Documentation

Mathlib.Topology.ContinuousFunction.Basic

Continuous bundled maps #

In this file we define the type ContinuousMap of continuous bundled maps.

We use the DFunLike design, so each type of morphisms has a companion typeclass which is meant to be satisfied by itself and all stricter types.

structure ContinuousMap (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] :
Type (max u_1 u_2)

The type of continuous maps from α to β.

When possible, instead of parametrizing results over (f : C(α, β)), you should parametrize over {F : Type*} [ContinuousMapClass F α β] (f : F).

When you extend this structure, make sure to extend ContinuousMapClass.

  • toFun : αβ

    The function α → β

  • continuous_toFun : Continuous self.toFun

    Proposition that toFun is continuous

Instances For
    theorem ContinuousMap.continuous_toFun {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (self : C(α, β)) :
    Continuous self.toFun

    Proposition that toFun is continuous

    The type of continuous maps from α to β.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      class ContinuousMapClass (F : Type u_1) (α : Type u_2) (β : Type u_3) [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] :

      ContinuousMapClass F α β states that F is a type of continuous maps.

      You should extend this class when you extend ContinuousMap.

      • map_continuous : ∀ (f : F), Continuous f

        Continuity

      Instances
        theorem ContinuousMapClass.map_continuous {F : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] [self : ContinuousMapClass F α β] (f : F) :

        Continuity

        theorem map_continuousAt {F : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] [ContinuousMapClass F α β] (f : F) (a : α) :
        ContinuousAt (f) a
        theorem map_continuousWithinAt {F : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] [ContinuousMapClass F α β] (f : F) (s : Set α) (a : α) :
        def toContinuousMap {F : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] [ContinuousMapClass F α β] (f : F) :
        C(α, β)

        Coerce a bundled morphism with a ContinuousMapClass instance to a ContinuousMap.

        Equations
        • f = { toFun := f, continuous_toFun := }
        Instances For
          instance instCoeTCContinuousMap {F : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] [ContinuousMapClass F α β] :
          CoeTC F C(α, β)
          Equations
          • instCoeTCContinuousMap = { coe := toContinuousMap }

          Continuous maps #

          instance ContinuousMap.funLike {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] :
          FunLike C(α, β) α β
          Equations
          • ContinuousMap.funLike = { coe := ContinuousMap.toFun, coe_injective' := }
          Equations
          • =
          @[simp]
          theorem ContinuousMap.toFun_eq_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : C(α, β)} :
          f.toFun = f
          instance ContinuousMap.instCanLiftForallCoeContinuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] :
          CanLift (αβ) C(α, β) DFunLike.coe Continuous
          Equations
          • =
          def ContinuousMap.Simps.apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) :
          αβ

          See note [custom simps projection].

          Equations
          Instances For
            @[simp]
            theorem ContinuousMap.coe_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {F : Type u_5} [FunLike F α β] [ContinuousMapClass F α β] (f : F) :
            f = f
            theorem ContinuousMap.ext {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : C(α, β)} {g : C(α, β)} (h : ∀ (a : α), f a = g a) :
            f = g
            def ContinuousMap.copy {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (f' : αβ) (h : f' = f) :
            C(α, β)

            Copy of a ContinuousMap with a new toFun equal to the old one. Useful to fix definitional equalities.

            Equations
            • f.copy f' h = { toFun := f', continuous_toFun := }
            Instances For
              @[simp]
              theorem ContinuousMap.coe_copy {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (f' : αβ) (h : f' = f) :
              (f.copy f' h) = f'
              theorem ContinuousMap.copy_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (f' : αβ) (h : f' = f) :
              f.copy f' h = f
              theorem ContinuousMap.continuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) :

              Deprecated. Use map_continuous instead.

              theorem ContinuousMap.continuous_set_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (s : Set C(α, β)) (f : s) :
              Continuous f
              theorem ContinuousMap.continuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (x : α) :
              ContinuousAt (f) x

              Deprecated. Use map_continuousAt instead.

              theorem ContinuousMap.congr_fun {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : C(α, β)} {g : C(α, β)} (H : f = g) (x : α) :
              f x = g x

              Deprecated. Use DFunLike.congr_fun instead.

              theorem ContinuousMap.congr_arg {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) {x : α} {y : α} (h : x = y) :
              f x = f y

              Deprecated. Use DFunLike.congr_arg instead.

              @[simp]
              theorem ContinuousMap.coe_mk {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : αβ) (h : Continuous f) :
              { toFun := f, continuous_toFun := h } = f
              theorem ContinuousMap.map_specializes {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) {x : α} {y : α} (h : x y) :
              f x f y
              @[simp]
              theorem ContinuousMap.equivFnOfDiscrete_symm_apply_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology α] (f : αβ) :
              ∀ (a : α), ((ContinuousMap.equivFnOfDiscrete α β).symm f) a = f a
              @[simp]
              theorem ContinuousMap.equivFnOfDiscrete_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology α] (f : C(α, β)) (a : α) :
              def ContinuousMap.equivFnOfDiscrete (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology α] :
              C(α, β) (αβ)

              The continuous functions from α to β are the same as the plain functions when α is discrete.

              Equations
              • ContinuousMap.equivFnOfDiscrete α β = { toFun := fun (f : C(α, β)) => f, invFun := fun (f : αβ) => { toFun := f, continuous_toFun := }, left_inv := , right_inv := }
              Instances For
                def ContinuousMap.id (α : Type u_1) [TopologicalSpace α] :
                C(α, α)

                The identity as a continuous map.

                Equations
                Instances For
                  @[simp]
                  theorem ContinuousMap.coe_id (α : Type u_1) [TopologicalSpace α] :
                  (ContinuousMap.id α) = id
                  def ContinuousMap.const (α : Type u_1) {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (b : β) :
                  C(α, β)

                  The constant map as a continuous map.

                  Equations
                  Instances For
                    @[simp]
                    theorem ContinuousMap.coe_const (α : Type u_1) {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (b : β) :
                    @[simp]
                    theorem ContinuousMap.constPi_apply (α : Type u_1) {β : Type u_2} [TopologicalSpace β] :
                    (ContinuousMap.constPi α) = fun (b : β) => Function.const α b
                    def ContinuousMap.constPi (α : Type u_1) {β : Type u_2} [TopologicalSpace β] :
                    C(β, αβ)

                    Function.const α b as a bundled continuous function of b.

                    Equations
                    Instances For
                      Equations
                      @[simp]
                      theorem ContinuousMap.id_apply {α : Type u_1} [TopologicalSpace α] (a : α) :
                      @[simp]
                      theorem ContinuousMap.const_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (b : β) (a : α) :
                      def ContinuousMap.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : C(β, γ)) (g : C(α, β)) :
                      C(α, γ)

                      The composition of continuous maps, as a continuous map.

                      Equations
                      • f.comp g = { toFun := f g, continuous_toFun := }
                      Instances For
                        @[simp]
                        theorem ContinuousMap.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : C(β, γ)) (g : C(α, β)) :
                        (f.comp g) = f g
                        @[simp]
                        theorem ContinuousMap.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : C(β, γ)) (g : C(α, β)) (a : α) :
                        (f.comp g) a = f (g a)
                        @[simp]
                        theorem ContinuousMap.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (f : C(γ, δ)) (g : C(β, γ)) (h : C(α, β)) :
                        (f.comp g).comp h = f.comp (g.comp h)
                        @[simp]
                        theorem ContinuousMap.id_comp {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) :
                        (ContinuousMap.id β).comp f = f
                        @[simp]
                        theorem ContinuousMap.comp_id {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) :
                        f.comp (ContinuousMap.id α) = f
                        @[simp]
                        theorem ContinuousMap.const_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (c : γ) (f : C(α, β)) :
                        @[simp]
                        theorem ContinuousMap.comp_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : C(β, γ)) (b : β) :
                        @[simp]
                        theorem ContinuousMap.cancel_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f₁ : C(β, γ)} {f₂ : C(β, γ)} {g : C(α, β)} (hg : Function.Surjective g) :
                        f₁.comp g = f₂.comp g f₁ = f₂
                        @[simp]
                        theorem ContinuousMap.cancel_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : C(β, γ)} {g₁ : C(α, β)} {g₂ : C(α, β)} (hf : Function.Injective f) :
                        f.comp g₁ = f.comp g₂ g₁ = g₂
                        Equations
                        • =
                        @[simp]
                        theorem ContinuousMap.fst_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] :
                        ContinuousMap.fst = Prod.fst
                        def ContinuousMap.fst {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] :
                        C(α × β, α)

                        Prod.fst : (x, y) ↦ x as a bundled continuous map.

                        Equations
                        • ContinuousMap.fst = { toFun := Prod.fst, continuous_toFun := }
                        Instances For
                          @[simp]
                          theorem ContinuousMap.snd_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] :
                          ContinuousMap.snd = Prod.snd
                          def ContinuousMap.snd {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] :
                          C(α × β, β)

                          Prod.snd : (x, y) ↦ y as a bundled continuous map.

                          Equations
                          • ContinuousMap.snd = { toFun := Prod.snd, continuous_toFun := }
                          Instances For
                            def ContinuousMap.prodMk {α : Type u_1} [TopologicalSpace α] {β₁ : Type u_7} {β₂ : Type u_8} [TopologicalSpace β₁] [TopologicalSpace β₂] (f : C(α, β₁)) (g : C(α, β₂)) :
                            C(α, β₁ × β₂)

                            Given two continuous maps f and g, this is the continuous map x ↦ (f x, g x).

                            Equations
                            • f.prodMk g = { toFun := fun (x : α) => (f x, g x), continuous_toFun := }
                            Instances For
                              @[simp]
                              theorem ContinuousMap.prodMap_apply {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} [TopologicalSpace α₁] [TopologicalSpace α₂] [TopologicalSpace β₁] [TopologicalSpace β₂] (f : C(α₁, α₂)) (g : C(β₁, β₂)) :
                              ∀ (a : α₁ × β₁), (f.prodMap g) a = Prod.map (f) (g) a
                              def ContinuousMap.prodMap {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} [TopologicalSpace α₁] [TopologicalSpace α₂] [TopologicalSpace β₁] [TopologicalSpace β₂] (f : C(α₁, α₂)) (g : C(β₁, β₂)) :
                              C(α₁ × β₁, α₂ × β₂)

                              Given two continuous maps f and g, this is the continuous map (x, y) ↦ (f x, g y).

                              Equations
                              • f.prodMap g = { toFun := Prod.map f g, continuous_toFun := }
                              Instances For
                                @[simp]
                                theorem ContinuousMap.prod_eval {α : Type u_1} [TopologicalSpace α] {β₁ : Type u_7} {β₂ : Type u_8} [TopologicalSpace β₁] [TopologicalSpace β₂] (f : C(α, β₁)) (g : C(α, β₂)) (a : α) :
                                (f.prodMk g) a = (f a, g a)
                                @[simp]
                                theorem ContinuousMap.prodSwap_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (x : α × β) :
                                ContinuousMap.prodSwap x = (x.2, x.1)
                                def ContinuousMap.prodSwap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] :
                                C(α × β, β × α)

                                Prod.swap bundled as a ContinuousMap.

                                Equations
                                • ContinuousMap.prodSwap = ContinuousMap.snd.prodMk ContinuousMap.fst
                                Instances For
                                  @[simp]
                                  theorem ContinuousMap.sigmaMk_apply {I : Type u_5} {X : IType u_7} [(i : I) → TopologicalSpace (X i)] (i : I) (snd : X i) :
                                  (ContinuousMap.sigmaMk i) snd = i, snd
                                  def ContinuousMap.sigmaMk {I : Type u_5} {X : IType u_7} [(i : I) → TopologicalSpace (X i)] (i : I) :
                                  C(X i, (i : I) × X i)

                                  Sigma.mk i as a bundled continuous map.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem ContinuousMap.sigma_apply {I : Type u_5} {A : Type u_6} {X : IType u_7} [TopologicalSpace A] [(i : I) → TopologicalSpace (X i)] (f : (i : I) → C(X i, A)) (ig : (i : I) × X i) :
                                    (ContinuousMap.sigma f) ig = (f ig.fst) ig.snd
                                    def ContinuousMap.sigma {I : Type u_5} {A : Type u_6} {X : IType u_7} [TopologicalSpace A] [(i : I) → TopologicalSpace (X i)] (f : (i : I) → C(X i, A)) :
                                    C((i : I) × X i, A)

                                    To give a continuous map out of a disjoint union, it suffices to give a continuous map out of each term. This is Sigma.uncurry for continuous maps.

                                    Equations
                                    • ContinuousMap.sigma f = { toFun := fun (ig : (i : I) × X i) => (f ig.fst) ig.snd, continuous_toFun := }
                                    Instances For
                                      @[simp]
                                      theorem ContinuousMap.sigmaEquiv_apply {I : Type u_5} (A : Type u_6) (X : IType u_7) [TopologicalSpace A] [(i : I) → TopologicalSpace (X i)] (f : (i : I) → C(X i, A)) :
                                      @[simp]
                                      theorem ContinuousMap.sigmaEquiv_symm_apply {I : Type u_5} (A : Type u_6) (X : IType u_7) [TopologicalSpace A] [(i : I) → TopologicalSpace (X i)] (f : C((i : I) × X i, A)) (i : I) :
                                      def ContinuousMap.sigmaEquiv {I : Type u_5} (A : Type u_6) (X : IType u_7) [TopologicalSpace A] [(i : I) → TopologicalSpace (X i)] :
                                      ((i : I) → C(X i, A)) C((i : I) × X i, A)

                                      Giving a continuous map out of a disjoint union is the same as giving a continuous map out of each term. This is a version of Equiv.piCurry for continuous maps.

                                      Equations
                                      Instances For
                                        def ContinuousMap.pi {I : Type u_5} {A : Type u_6} {X : IType u_7} [TopologicalSpace A] [(i : I) → TopologicalSpace (X i)] (f : (i : I) → C(A, X i)) :
                                        C(A, (i : I) → X i)

                                        Abbreviation for product of continuous maps, which is continuous

                                        Equations
                                        • ContinuousMap.pi f = { toFun := fun (a : A) (i : I) => (f i) a, continuous_toFun := }
                                        Instances For
                                          @[simp]
                                          theorem ContinuousMap.pi_eval {I : Type u_5} {A : Type u_6} {X : IType u_7} [TopologicalSpace A] [(i : I) → TopologicalSpace (X i)] (f : (i : I) → C(A, X i)) (a : A) :
                                          (ContinuousMap.pi f) a = fun (i : I) => (f i) a
                                          @[simp]
                                          theorem ContinuousMap.eval_apply {I : Type u_5} {X : IType u_7} [(i : I) → TopologicalSpace (X i)] (i : I) :
                                          def ContinuousMap.eval {I : Type u_5} {X : IType u_7} [(i : I) → TopologicalSpace (X i)] (i : I) :
                                          C((j : I) → X j, X i)

                                          Evaluation at point as a bundled continuous map.

                                          Equations
                                          Instances For
                                            @[simp]
                                            theorem ContinuousMap.piEquiv_apply {I : Type u_5} (A : Type u_6) (X : IType u_7) [TopologicalSpace A] [(i : I) → TopologicalSpace (X i)] (f : (i : I) → C(A, X i)) :
                                            @[simp]
                                            theorem ContinuousMap.piEquiv_symm_apply {I : Type u_5} (A : Type u_6) (X : IType u_7) [TopologicalSpace A] [(i : I) → TopologicalSpace (X i)] (f : C(A, (i : I) → X i)) (i : I) :
                                            (ContinuousMap.piEquiv A X).symm f i = (ContinuousMap.eval i).comp f
                                            def ContinuousMap.piEquiv {I : Type u_5} (A : Type u_6) (X : IType u_7) [TopologicalSpace A] [(i : I) → TopologicalSpace (X i)] :
                                            ((i : I) → C(A, X i)) C(A, (i : I) → X i)

                                            Giving a continuous map out of a disjoint union is the same as giving a continuous map out of each term

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem ContinuousMap.piMap_apply {I : Type u_5} {X : IType u_7} {Y : IType u_8} [(i : I) → TopologicalSpace (X i)] [(i : I) → TopologicalSpace (Y i)] (f : (i : I) → C(X i, Y i)) (a : (i : I) → X i) (i : I) :
                                              (ContinuousMap.piMap f) a i = (f i) (a i)
                                              def ContinuousMap.piMap {I : Type u_5} {X : IType u_7} {Y : IType u_8} [(i : I) → TopologicalSpace (X i)] [(i : I) → TopologicalSpace (Y i)] (f : (i : I) → C(X i, Y i)) :
                                              C((i : I) → X i, (i : I) → Y i)

                                              Combine a collection of bundled continuous maps C(X i, Y i) into a bundled continuous map C(∀ i, X i, ∀ i, Y i).

                                              Equations
                                              Instances For
                                                def ContinuousMap.precomp {I : Type u_5} {X : IType u_7} [(i : I) → TopologicalSpace (X i)] {ι : Type u_9} (φ : ιI) :
                                                C((i : I) → X i, (i : ι) → X (φ i))

                                                "Precomposition" as a continuous map between dependent types.

                                                Equations
                                                • ContinuousMap.precomp φ = { toFun := fun (f : (i : I) → X i) (j : ι) => f (φ j), continuous_toFun := }
                                                Instances For
                                                  def ContinuousMap.restrict {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (s : Set α) (f : C(α, β)) :
                                                  C(s, β)

                                                  The restriction of a continuous function α → β to a subset s of α.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem ContinuousMap.coe_restrict {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (s : Set α) (f : C(α, β)) :
                                                    (ContinuousMap.restrict s f) = f Subtype.val
                                                    @[simp]
                                                    theorem ContinuousMap.restrict_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (s : Set α) (x : s) :
                                                    (ContinuousMap.restrict s f) x = f x
                                                    @[simp]
                                                    theorem ContinuousMap.restrict_apply_mk {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (s : Set α) (x : α) (hx : x s) :
                                                    (ContinuousMap.restrict s f) x, hx = f x
                                                    @[simp]
                                                    theorem ContinuousMap.restrictPreimage_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (s : Set β) :
                                                    ∀ (a : (f ⁻¹' s)), (f.restrictPreimage s) a = s.restrictPreimage (f) a
                                                    def ContinuousMap.restrictPreimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (s : Set β) :
                                                    C((f ⁻¹' s), s)

                                                    The restriction of a continuous map to the preimage of a set.

                                                    Equations
                                                    • f.restrictPreimage s = { toFun := s.restrictPreimage f, continuous_toFun := }
                                                    Instances For
                                                      noncomputable def ContinuousMap.liftCover {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {ι : Type u_5} (S : ιSet α) (φ : (i : ι) → C((S i), β)) (hφ : ∀ (i j : ι) (x : α) (hxi : x S i) (hxj : x S j), (φ i) x, hxi = (φ j) x, hxj) (hS : ∀ (x : α), ∃ (i : ι), S i nhds x) :
                                                      C(α, β)

                                                      A family φ i of continuous maps C(S i, β), where the domains S i contain a neighbourhood of each point in α and the functions φ i agree pairwise on intersections, can be glued to construct a continuous map in C(α, β).

                                                      Equations
                                                      Instances For
                                                        @[simp]
                                                        theorem ContinuousMap.liftCover_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {ι : Type u_5} {S : ιSet α} {φ : (i : ι) → C((S i), β)} {hφ : ∀ (i j : ι) (x : α) (hxi : x S i) (hxj : x S j), (φ i) x, hxi = (φ j) x, hxj} {hS : ∀ (x : α), ∃ (i : ι), S i nhds x} {i : ι} (x : (S i)) :
                                                        (ContinuousMap.liftCover S φ hS) x = (φ i) x
                                                        theorem ContinuousMap.liftCover_restrict {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {ι : Type u_5} {S : ιSet α} {φ : (i : ι) → C((S i), β)} {hφ : ∀ (i j : ι) (x : α) (hxi : x S i) (hxj : x S j), (φ i) x, hxi = (φ j) x, hxj} {hS : ∀ (x : α), ∃ (i : ι), S i nhds x} {i : ι} :
                                                        noncomputable def ContinuousMap.liftCover' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (A : Set (Set α)) (F : (s : Set α) → s AC(s, β)) (hF : ∀ (s : Set α) (hs : s A) (t : Set α) (ht : t A) (x : α) (hxi : x s) (hxj : x t), (F s hs) x, hxi = (F t ht) x, hxj) (hA : ∀ (x : α), iA, i nhds x) :
                                                        C(α, β)

                                                        A family F s of continuous maps C(s, β), where (1) the domains s are taken from a set A of sets in α which contain a neighbourhood of each point in α and (2) the functions F s agree pairwise on intersections, can be glued to construct a continuous map in C(α, β).

                                                        Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem ContinuousMap.liftCover_coe' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {A : Set (Set α)} {F : (s : Set α) → s AC(s, β)} {hF : ∀ (s : Set α) (hs : s A) (t : Set α) (ht : t A) (x : α) (hxi : x s) (hxj : x t), (F s hs) x, hxi = (F t ht) x, hxj} {hA : ∀ (x : α), iA, i nhds x} {s : Set α} {hs : s A} (x : s) :
                                                          (ContinuousMap.liftCover' A F hF hA) x = (F s hs) x
                                                          @[simp]
                                                          theorem ContinuousMap.liftCover_restrict' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {A : Set (Set α)} {F : (s : Set α) → s AC(s, β)} {hF : ∀ (s : Set α) (hs : s A) (t : Set α) (ht : t A) (x : α) (hxi : x s) (hxj : x t), (F s hs) x, hxi = (F t ht) x, hxj} {hA : ∀ (x : α), iA, i nhds x} {s : Set α} {hs : s A} :
                                                          @[simp]
                                                          theorem Function.RightInverse.homeomorph_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {f' : C(Y, X)} (hf : Function.RightInverse f' f) (b : Y) :
                                                          hf.homeomorph.symm b = Quotient.mk'' (f' b)
                                                          @[simp]
                                                          theorem Function.RightInverse.homeomorph_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {f' : C(Y, X)} (hf : Function.RightInverse f' f) (a : Quotient (Setoid.ker f)) :
                                                          hf.homeomorph a = a.liftOn' f
                                                          def Function.RightInverse.homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {f' : C(Y, X)} (hf : Function.RightInverse f' f) :

                                                          Setoid.quotientKerEquivOfRightInverse as a homeomorphism.

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem QuotientMap.homeomorph_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} (hf : QuotientMap f) (b : Y) :
                                                            hf.homeomorph.symm b = Quotient.mk'' (Function.surjInv b)
                                                            @[simp]
                                                            theorem QuotientMap.homeomorph_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} (hf : QuotientMap f) (a : Quotient (Setoid.ker f)) :
                                                            hf.homeomorph a = a.liftOn' f
                                                            noncomputable def QuotientMap.homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} (hf : QuotientMap f) :

                                                            The homeomorphism from the quotient of a quotient map to its codomain. This is Setoid.quotientKerEquivOfSurjective as a homeomorphism.

                                                            Equations
                                                            Instances For
                                                              @[simp]
                                                              theorem QuotientMap.lift_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} (hf : QuotientMap f) (g : C(X, Z)) (h : Function.FactorsThrough g f) :
                                                              ∀ (a : Y), (hf.lift g h) a = ((fun (i : Quotient (Setoid.ker f)) => i.liftOn' g ) hf.homeomorph.symm) a
                                                              noncomputable def QuotientMap.lift {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} (hf : QuotientMap f) (g : C(X, Z)) (h : Function.FactorsThrough g f) :
                                                              C(Y, Z)

                                                              Descend a continuous map, which is constant on the fibres, along a quotient map.

                                                              Equations
                                                              • hf.lift g h = { toFun := (fun (i : Quotient (Setoid.ker f)) => i.liftOn' g ) hf.homeomorph.symm, continuous_toFun := }
                                                              Instances For
                                                                @[simp]
                                                                theorem QuotientMap.lift_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} (hf : QuotientMap f) (g : C(X, Z)) (h : Function.FactorsThrough g f) :
                                                                (hf.lift g h).comp f = g

                                                                The obvious triangle induced by QuotientMap.lift commutes:

                                                                     g
                                                                  X --→ Z
                                                                  |   ↗
                                                                f |  / hf.lift g h
                                                                  v /
                                                                  Y
                                                                
                                                                @[simp]
                                                                theorem QuotientMap.liftEquiv_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} (hf : QuotientMap f) (g : { g : C(X, Z) // Function.FactorsThrough g f }) :
                                                                hf.liftEquiv g = hf.lift g
                                                                @[simp]
                                                                theorem QuotientMap.liftEquiv_symm_apply_coe {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} (hf : QuotientMap f) (g : C(Y, Z)) :
                                                                (hf.liftEquiv.symm g) = g.comp f
                                                                noncomputable def QuotientMap.liftEquiv {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} (hf : QuotientMap f) :
                                                                { g : C(X, Z) // Function.FactorsThrough g f } C(Y, Z)

                                                                QuotientMap.lift as an equivalence.

                                                                Equations
                                                                • hf.liftEquiv = { toFun := fun (g : { g : C(X, Z) // Function.FactorsThrough g f }) => hf.lift g , invFun := fun (g : C(Y, Z)) => g.comp f, , left_inv := , right_inv := }
                                                                Instances For
                                                                  @[simp]
                                                                  theorem Homeomorph.toContinuousMap_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ₜ β) (a : α) :
                                                                  e.toContinuousMap a = e a
                                                                  def Homeomorph.toContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ₜ β) :
                                                                  C(α, β)

                                                                  The forward direction of a homeomorphism, as a bundled continuous map.

                                                                  Equations
                                                                  • e.toContinuousMap = { toFun := e, continuous_toFun := }
                                                                  Instances For
                                                                    instance Homeomorph.instCoeContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] :
                                                                    Coe (α ≃ₜ β) C(α, β)

                                                                    Homeomorph.toContinuousMap as a coercion.

                                                                    Equations
                                                                    • Homeomorph.instCoeContinuousMap = { coe := Homeomorph.toContinuousMap }
                                                                    @[simp]
                                                                    theorem Homeomorph.coe_refl {α : Type u_1} [TopologicalSpace α] :
                                                                    (Homeomorph.refl α).toContinuousMap = ContinuousMap.id α
                                                                    @[simp]
                                                                    theorem Homeomorph.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : α ≃ₜ β) (g : β ≃ₜ γ) :
                                                                    (f.trans g).toContinuousMap = g.toContinuousMap.comp f.toContinuousMap
                                                                    @[simp]
                                                                    theorem Homeomorph.symm_comp_toContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) :
                                                                    f.symm.toContinuousMap.comp f.toContinuousMap = ContinuousMap.id α

                                                                    Left inverse to a continuous map from a homeomorphism, mirroring Equiv.symm_comp_self.

                                                                    @[simp]
                                                                    theorem Homeomorph.toContinuousMap_comp_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) :
                                                                    f.toContinuousMap.comp f.symm.toContinuousMap = ContinuousMap.id β

                                                                    Right inverse to a continuous map from a homeomorphism, mirroring Equiv.self_comp_symm.