Documentation

Mathlib.Topology.ContinuousFunction.Basic

Continuous bundled maps #

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

We use the FunLike 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)
  • toFun : αβ

    The function α → β

  • continuous_toFun : Continuous s.toFun

    Proposition that toFun is continuous

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.

Instances For

    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) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [TopologicalSpace α] [TopologicalSpace β] extends FunLike :
      Type (max (max u_1 u_2) u_3)

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

      You should extend this class when you extend ContinuousMap.

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

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

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

          Continuous maps #

          Equations
          @[simp]
          theorem ContinuousMap.toFun_eq_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : C(α, β)} :
          f.toFun = f
          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} [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
            Instances For
              @[simp]
              theorem ContinuousMap.coe_copy {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (f' : αβ) (h : f' = f) :
              ↑(ContinuousMap.copy f f' h) = f'
              theorem ContinuousMap.copy_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (f' : αβ) (h : f' = 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 FunLike.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 FunLike.congr_arg instead.

              @[simp]
              theorem ContinuousMap.coe_mk {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : αβ) (h : Continuous 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_apply (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology α] (f : C(α, β)) (a : α) :
              ↑(ContinuousMap.equivFnOfDiscrete α β) f a = f 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
              • One or more equations did not get rendered due to their size.
              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
                      @[simp]
                      theorem ContinuousMap.id_apply {α : Type u_1} [TopologicalSpace α] (a : α) :
                      ↑(ContinuousMap.id α) a = a
                      @[simp]
                      theorem ContinuousMap.const_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (b : β) (a : α) :
                      ↑(ContinuousMap.const α b) a = b
                      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
                      Instances For
                        @[simp]
                        theorem ContinuousMap.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : C(β, γ)) (g : C(α, β)) :
                        ↑(ContinuousMap.comp f 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 : α) :
                        ↑(ContinuousMap.comp f 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(α, β)) :
                        @[simp]
                        theorem ContinuousMap.id_comp {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) :
                        @[simp]
                        theorem ContinuousMap.comp_id {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) :
                        @[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) :
                        ContinuousMap.comp f₁ g = ContinuousMap.comp f₂ 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) :
                        ContinuousMap.comp f g₁ = ContinuousMap.comp f g₂ g₁ = g₂
                        @[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
                        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
                          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
                            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 : α₁ × β₁), ↑(ContinuousMap.prodMap f 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
                              Instances For
                                @[simp]
                                theorem ContinuousMap.prod_eval {α : Type u_1} [TopologicalSpace α] {β₁ : Type u_7} {β₂ : Type u_8} [TopologicalSpace β₁] [TopologicalSpace β₂] (f : C(α, β₁)) (g : C(α, β₂)) (a : α) :
                                ↑(ContinuousMap.prodMk f g) a = (f a, g a)
                                @[simp]
                                theorem ContinuousMap.prodSwap_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (x : α × β) :
                                ContinuousMap.prodSwap x = (x.snd, x.fst)
                                def ContinuousMap.prodSwap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] :
                                C(α × β, β × α)

                                Prod.swap bundled as a ContinuousMap.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem ContinuousMap.sigmaMk_apply {ι : Type u_5} {Y : ιType u_6} [(i : ι) → TopologicalSpace (Y i)] (i : ι) (snd : Y i) :
                                  ↑(ContinuousMap.sigmaMk i) snd = { fst := i, snd := snd }
                                  def ContinuousMap.sigmaMk {ι : Type u_5} {Y : ιType u_6} [(i : ι) → TopologicalSpace (Y i)] (i : ι) :
                                  C(Y i, (i : ι) × Y i)

                                  Sigma.mk i as a bundled continuous map.

                                  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
                                    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 => ↑(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.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.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) { val := x, property := hx } = f x
                                            @[simp]
                                            theorem ContinuousMap.restrictPreimage_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (s : Set β) :
                                            ∀ (a : ↑(f ⁻¹' s)), ↑(ContinuousMap.restrictPreimage f s) a = Set.restrictPreimage s (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
                                            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) { val := x, property := hxi } = ↑(φ j) { val := x, property := 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) { val := x, property := hxi } = ↑(φ j) { val := x, property := 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) { val := x, property := hxi } = ↑(φ j) { val := x, property := 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) { val := x, property := hxi } = ↑(F t ht) { val := x, property := hxj }) (hA : ∀ (x : α), i, i A 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
                                                • One or more equations did not get rendered due to their size.
                                                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) { val := x, property := hxi } = ↑(F t ht) { val := x, property := hxj }} {hA : ∀ (x : α), i, i A 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) { val := x, property := hxi } = ↑(F t ht) { val := x, property := hxj }} {hA : ∀ (x : α), i, i A i nhds x} {s : Set α} {hs : s A} :
                                                  @[simp]
                                                  theorem Homeomorph.toContinuousMap_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (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
                                                  Instances For

                                                    Homeomorph.toContinuousMap as a coercion.

                                                    Equations
                                                    • Homeomorph.instCoeHomeomorphContinuousMap = { coe := Homeomorph.toContinuousMap }
                                                    @[simp]

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

                                                    @[simp]

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