Documentation

Mathlib.Topology.ContinuousMap.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.

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 : α) :

Continuous maps #

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

Deprecated. Use map_continuousAt instead.

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_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology α] (f : C(α, β)) (a : α) :
@[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
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_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) :
                          @[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)) :
                          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_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
                                              @[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)
                                              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 IsQuotientMap.homeomorph_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} (hf : IsQuotientMap f) (b : Y) :
                                                hf.homeomorph.symm b = Quotient.mk'' (Function.surjInv b)
                                                @[simp]
                                                theorem IsQuotientMap.homeomorph_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} (hf : IsQuotientMap f) (a : Quotient (Setoid.ker f)) :
                                                hf.homeomorph a = a.liftOn' f
                                                noncomputable def IsQuotientMap.homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} (hf : IsQuotientMap 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 IsQuotientMap.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 : IsQuotientMap 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 IsQuotientMap.lift {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} (hf : IsQuotientMap 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 IsQuotientMap.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 : IsQuotientMap f) (g : C(X, Z)) (h : Function.FactorsThrough g f) :
                                                    (hf.lift g h).comp f = g

                                                    The obvious triangle induced by IsQuotientMap.lift commutes:

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

                                                    IsQuotientMap.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
                                                      Equations
                                                      • =
                                                      @[simp, deprecated ContinuousMap.coe_apply]
                                                      theorem Homeomorph.toContinuousMap_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ₜ β) (a : α) :
                                                      e.toContinuousMap a = e a
                                                      @[deprecated toContinuousMap]
                                                      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
                                                        @[simp]
                                                        theorem Homeomorph.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : α ≃ₜ β) (g : β ≃ₜ γ) :
                                                        (f.trans g) = (↑g).comp f
                                                        @[simp]
                                                        theorem Homeomorph.symm_comp_toContinuousMap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) :
                                                        (↑f.symm).comp f = 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).comp f.symm = ContinuousMap.id β

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