Documentation

Mathlib.Topology.Algebra.ContinuousMonoidHom

Continuous Monoid Homs #

This file defines the space of continuous homomorphisms between two topological groups.

Main definitions #

structure ContinuousAddMonoidHom (A : Type u_7) (B : Type u_8) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] extends AddMonoidHom :
Type (max u_7 u_8)

The type of continuous additive monoid homomorphisms from A to B.

  • toFun : AB
  • map_zero' : (self.toAddMonoidHom).toFun 0 = 0
  • map_add' : ∀ (x y : A), (self.toAddMonoidHom).toFun (x + y) = (self.toAddMonoidHom).toFun x + (self.toAddMonoidHom).toFun y
  • continuous_toFun : Continuous (self.toAddMonoidHom).toFun

    Proof of continuity of the Hom.

Instances For
    theorem ContinuousAddMonoidHom.continuous_toFun {A : Type u_7} {B : Type u_8} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (self : ContinuousAddMonoidHom A B) :
    Continuous (self.toAddMonoidHom).toFun

    Proof of continuity of the Hom.

    structure ContinuousMonoidHom (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] extends MonoidHom :
    Type (max u_2 u_3)

    The type of continuous monoid homomorphisms from A to B.

    When possible, instead of parametrizing results over (f : ContinuousMonoidHom A B), you should parametrize over (F : Type*) [ContinuousMonoidHomClass F A B] (f : F).

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

    • toFun : AB
    • map_one' : (self.toMonoidHom).toFun 1 = 1
    • map_mul' : ∀ (x y : A), (self.toMonoidHom).toFun (x * y) = (self.toMonoidHom).toFun x * (self.toMonoidHom).toFun y
    • continuous_toFun : Continuous (self.toMonoidHom).toFun

      Proof of continuity of the Hom.

    Instances For
      theorem ContinuousMonoidHom.continuous_toFun {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (self : ContinuousMonoidHom A B) :
      Continuous (self.toMonoidHom).toFun

      Proof of continuity of the Hom.

      ContinuousAddMonoidHomClass F A B states that F is a type of continuous additive monoid homomorphisms.

      You should also extend this typeclass when you extend ContinuousAddMonoidHom.

      • map_add : ∀ (f : F) (x y : A), f (x + y) = f x + f y
      • map_zero : ∀ (f : F), f 0 = 0
      • map_continuous : ∀ (f : F), Continuous f

        Proof of the continuity of the map.

      Instances

        Proof of the continuity of the map.

        class ContinuousMonoidHomClass (F : Type u_1) (A : outParam (Type u_7)) (B : outParam (Type u_8)) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [FunLike F A B] extends MonoidHomClass :

        ContinuousMonoidHomClass F A B states that F is a type of continuous monoid homomorphisms.

        You should also extend this typeclass when you extend ContinuousMonoidHom.

        • map_mul : ∀ (f : F) (x y : A), f (x * y) = f x * f y
        • map_one : ∀ (f : F), f 1 = 1
        • map_continuous : ∀ (f : F), Continuous f

          Proof of the continuity of the map.

        Instances
          theorem ContinuousMonoidHomClass.map_continuous {F : Type u_1} {A : outParam (Type u_7)} {B : outParam (Type u_8)} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [FunLike F A B] [self : ContinuousMonoidHomClass F A B] (f : F) :

          Proof of the continuity of the map.

          @[instance 100]
          Equations
          • =
          @[instance 100]
          Equations
          • =
          Equations
          • ContinuousAddMonoidHom.funLike = { coe := fun (f : ContinuousAddMonoidHom A B) => (f.toAddMonoidHom).toFun, coe_injective' := }
          theorem ContinuousAddMonoidHom.funLike.proof_1 {A : Type u_1} {B : Type u_2} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (f : ContinuousAddMonoidHom A B) (g : ContinuousAddMonoidHom A B) (h : (fun (f : ContinuousAddMonoidHom A B) => (f.toAddMonoidHom).toFun) f = (fun (f : ContinuousAddMonoidHom A B) => (f.toAddMonoidHom).toFun) g) :
          f = g
          Equations
          • ContinuousMonoidHom.funLike = { coe := fun (f : ContinuousMonoidHom A B) => (f.toMonoidHom).toFun, coe_injective' := }
          theorem ContinuousAddMonoidHom.ext {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] {f : ContinuousAddMonoidHom A B} {g : ContinuousAddMonoidHom A B} (h : ∀ (x : A), f x = g x) :
          f = g
          theorem ContinuousMonoidHom.ext {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] {f : ContinuousMonoidHom A B} {g : ContinuousMonoidHom A B} (h : ∀ (x : A), f x = g x) :
          f = g

          Reinterpret a ContinuousAddMonoidHom as a ContinuousMap.

          Equations
          • f.toContinuousMap = { toFun := (f.toAddMonoidHom).toFun, continuous_toFun := }
          Instances For

            Reinterpret a ContinuousMonoidHom as a ContinuousMap.

            Equations
            • f.toContinuousMap = { toFun := (f.toMonoidHom).toFun, continuous_toFun := }
            Instances For
              theorem ContinuousAddMonoidHom.toContinuousMap_injective {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] :
              Function.Injective ContinuousAddMonoidHom.toContinuousMap
              theorem ContinuousMonoidHom.toContinuousMap_injective {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] :
              Function.Injective ContinuousMonoidHom.toContinuousMap

              Construct a ContinuousAddMonoidHom from a Continuous AddMonoidHom.

              Equations
              Instances For
                def ContinuousMonoidHom.mk' {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (f : A →* B) (hf : Continuous f) :

                Construct a ContinuousMonoidHom from a Continuous MonoidHom.

                Equations
                Instances For
                  theorem ContinuousAddMonoidHom.comp.proof_1 {A : Type u_1} {B : Type u_3} {C : Type u_2} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (g : ContinuousAddMonoidHom B C) (f : ContinuousAddMonoidHom A B) :
                  Continuous ((g.toAddMonoidHom).toFun f.toAddMonoidHom)

                  Composition of two continuous homomorphisms.

                  Equations
                  Instances For
                    @[simp]
                    theorem ContinuousAddMonoidHom.comp_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (g : ContinuousAddMonoidHom B C) (f : ContinuousAddMonoidHom A B) :
                    ∀ (a : A), (g.comp f) a = g.toAddMonoidHom (f.toAddMonoidHom a)
                    @[simp]
                    theorem ContinuousMonoidHom.comp_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid A] [Monoid B] [Monoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (g : ContinuousMonoidHom B C) (f : ContinuousMonoidHom A B) :
                    ∀ (a : A), (g.comp f) a = g.toMonoidHom (f.toMonoidHom a)

                    Composition of two continuous homomorphisms.

                    Equations
                    Instances For

                      Product of two continuous homomorphisms on the same space.

                      Equations
                      Instances For
                        theorem ContinuousAddMonoidHom.sum.proof_1 {A : Type u_1} {B : Type u_3} {C : Type u_2} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (f : ContinuousAddMonoidHom A B) (g : ContinuousAddMonoidHom A C) :
                        Continuous fun (x : A) => ((f.toAddMonoidHom).toFun x, g.toAddMonoidHom x)
                        @[simp]
                        theorem ContinuousAddMonoidHom.sum_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (f : ContinuousAddMonoidHom A B) (g : ContinuousAddMonoidHom A C) (i : A) :
                        (f.sum g) i = (f.toAddMonoidHom i, g.toAddMonoidHom i)
                        @[simp]
                        theorem ContinuousMonoidHom.prod_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid A] [Monoid B] [Monoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (f : ContinuousMonoidHom A B) (g : ContinuousMonoidHom A C) (i : A) :
                        (f.prod g) i = (f.toMonoidHom i, g.toMonoidHom i)

                        Product of two continuous homomorphisms on the same space.

                        Equations
                        Instances For

                          Product of two continuous homomorphisms on different spaces.

                          Equations
                          Instances For
                            theorem ContinuousAddMonoidHom.sum_map.proof_1 {A : Type u_1} {B : Type u_2} {C : Type u_4} {D : Type u_3} [AddMonoid A] [AddMonoid B] [AddMonoid C] [AddMonoid D] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [TopologicalSpace D] (f : ContinuousAddMonoidHom A C) (g : ContinuousAddMonoidHom B D) :
                            Continuous fun (p : A × B) => ((f.toAddMonoidHom).toFun p.1, (g.toAddMonoidHom).1 p.2)
                            @[simp]
                            theorem ContinuousAddMonoidHom.sum_map_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddMonoid A] [AddMonoid B] [AddMonoid C] [AddMonoid D] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [TopologicalSpace D] (f : ContinuousAddMonoidHom A C) (g : ContinuousAddMonoidHom B D) (i : A × B) :
                            (f.sum_map g) i = (f.toAddMonoidHom i.1, g.toAddMonoidHom i.2)
                            @[simp]
                            theorem ContinuousMonoidHom.prod_map_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [Monoid A] [Monoid B] [Monoid C] [Monoid D] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [TopologicalSpace D] (f : ContinuousMonoidHom A C) (g : ContinuousMonoidHom B D) (i : A × B) :
                            (f.prod_map g) i = (f.toMonoidHom i.1, g.toMonoidHom i.2)

                            Product of two continuous homomorphisms on different spaces.

                            Equations
                            Instances For

                              The trivial continuous homomorphism.

                              Equations
                              Instances For
                                theorem ContinuousAddMonoidHom.zero.proof_1 (A : Type u_1) (B : Type u_2) [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] :
                                Continuous fun (x : A) => AddZeroClass.toZero.1
                                @[simp]
                                theorem ContinuousMonoidHom.one_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] :
                                ∀ (x : A), (ContinuousMonoidHom.one A B) x = 1
                                @[simp]

                                The trivial continuous homomorphism.

                                Equations
                                Instances For

                                  The identity continuous homomorphism.

                                  Equations
                                  Instances For
                                    @[simp]

                                    The identity continuous homomorphism.

                                    Equations
                                    Instances For

                                      The continuous homomorphism given by projection onto the first factor.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem ContinuousAddMonoidHom.fst_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (self : A × B) :
                                        (ContinuousAddMonoidHom.fst A B) self = self.1
                                        @[simp]
                                        theorem ContinuousMonoidHom.fst_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (self : A × B) :
                                        (ContinuousMonoidHom.fst A B) self = self.1

                                        The continuous homomorphism given by projection onto the first factor.

                                        Equations
                                        Instances For

                                          The continuous homomorphism given by projection onto the second factor.

                                          Equations
                                          Instances For
                                            @[simp]
                                            theorem ContinuousAddMonoidHom.snd_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (self : A × B) :
                                            (ContinuousAddMonoidHom.snd A B) self = self.2
                                            @[simp]
                                            theorem ContinuousMonoidHom.snd_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (self : A × B) :
                                            (ContinuousMonoidHom.snd A B) self = self.2

                                            The continuous homomorphism given by projection onto the second factor.

                                            Equations
                                            Instances For

                                              The continuous homomorphism given by inclusion of the first factor.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem ContinuousMonoidHom.inl_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (i : A) :
                                                (ContinuousMonoidHom.inl A B) i = ((ContinuousMonoidHom.id A).toMonoidHom i, (ContinuousMonoidHom.one A B).toMonoidHom i)
                                                @[simp]
                                                theorem ContinuousAddMonoidHom.inl_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (i : A) :
                                                (ContinuousAddMonoidHom.inl A B) i = ((ContinuousAddMonoidHom.id A).toAddMonoidHom i, (ContinuousAddMonoidHom.zero A B).toAddMonoidHom i)

                                                The continuous homomorphism given by inclusion of the first factor.

                                                Equations
                                                Instances For

                                                  The continuous homomorphism given by inclusion of the second factor.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem ContinuousMonoidHom.inr_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (i : B) :
                                                    (ContinuousMonoidHom.inr A B) i = ((ContinuousMonoidHom.one B A).toMonoidHom i, (ContinuousMonoidHom.id B).toMonoidHom i)
                                                    @[simp]
                                                    theorem ContinuousAddMonoidHom.inr_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (i : B) :
                                                    (ContinuousAddMonoidHom.inr A B) i = ((ContinuousAddMonoidHom.zero B A).toAddMonoidHom i, (ContinuousAddMonoidHom.id B).toAddMonoidHom i)

                                                    The continuous homomorphism given by inclusion of the second factor.

                                                    Equations
                                                    Instances For

                                                      The continuous homomorphism given by the diagonal embedding.

                                                      Equations
                                                      Instances For
                                                        @[simp]
                                                        theorem ContinuousMonoidHom.diag_toFun (A : Type u_2) [Monoid A] [TopologicalSpace A] (i : A) :
                                                        (ContinuousMonoidHom.diag A) i = ((ContinuousMonoidHom.id A).toMonoidHom i, (ContinuousMonoidHom.id A).toMonoidHom i)
                                                        @[simp]

                                                        The continuous homomorphism given by the diagonal embedding.

                                                        Equations
                                                        Instances For

                                                          The continuous homomorphism given by swapping components.

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem ContinuousAddMonoidHom.swap_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (i : A × B) :
                                                            (ContinuousAddMonoidHom.swap A B) i = ((ContinuousAddMonoidHom.snd A B).toAddMonoidHom i, (ContinuousAddMonoidHom.fst A B).toAddMonoidHom i)
                                                            @[simp]
                                                            theorem ContinuousMonoidHom.swap_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (i : A × B) :
                                                            (ContinuousMonoidHom.swap A B) i = ((ContinuousMonoidHom.snd A B).toMonoidHom i, (ContinuousMonoidHom.fst A B).toMonoidHom i)

                                                            The continuous homomorphism given by swapping components.

                                                            Equations
                                                            Instances For

                                                              The continuous homomorphism given by addition.

                                                              Equations
                                                              Instances For
                                                                @[simp]
                                                                theorem ContinuousMonoidHom.mul_toFun (E : Type u_6) [CommGroup E] [TopologicalSpace E] [TopologicalGroup E] :
                                                                ∀ (a : E × E), (ContinuousMonoidHom.mul E) a = a.1 * a.2

                                                                The continuous homomorphism given by multiplication.

                                                                Equations
                                                                Instances For

                                                                  The continuous homomorphism given by negation.

                                                                  Equations
                                                                  Instances For

                                                                    The continuous homomorphism given by inversion.

                                                                    Equations
                                                                    Instances For

                                                                      Coproduct of two continuous homomorphisms to the same space.

                                                                      Equations
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem ContinuousAddMonoidHom.coprod_toFun {A : Type u_2} {B : Type u_3} {E : Type u_6} [AddMonoid A] [AddMonoid B] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace E] [TopologicalAddGroup E] (f : ContinuousAddMonoidHom A E) (g : ContinuousAddMonoidHom B E) :
                                                                        ∀ (a : A × B), (f.coprod g) a = (ContinuousAddMonoidHom.add E).toAddMonoidHom ((f.sum_map g).toAddMonoidHom a)
                                                                        @[simp]
                                                                        theorem ContinuousMonoidHom.coprod_toFun {A : Type u_2} {B : Type u_3} {E : Type u_6} [Monoid A] [Monoid B] [CommGroup E] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace E] [TopologicalGroup E] (f : ContinuousMonoidHom A E) (g : ContinuousMonoidHom B E) :
                                                                        ∀ (a : A × B), (f.coprod g) a = (ContinuousMonoidHom.mul E).toMonoidHom ((f.prod_map g).toMonoidHom a)

                                                                        Coproduct of two continuous homomorphisms to the same space.

                                                                        Equations
                                                                        Instances For
                                                                          theorem ContinuousAddMonoidHom.instAddCommGroup.proof_5 {A : Type u_1} {E : Type u_2} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] :
                                                                          ∀ (n : ) (x : ContinuousAddMonoidHom A E), nsmulRec (n + 1) x = nsmulRec (n + 1) x
                                                                          theorem ContinuousAddMonoidHom.instAddCommGroup.proof_11 {A : Type u_1} {E : Type u_2} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] :
                                                                          ∀ (n : ) (a : ContinuousAddMonoidHom A E), zsmulRec (Int.ofNat n.succ) a = zsmulRec (Int.ofNat n.succ) a
                                                                          Equations
                                                                          Equations
                                                                          Equations
                                                                          • ContinuousAddMonoidHom.instTopologicalSpace = TopologicalSpace.induced ContinuousAddMonoidHom.toContinuousMap ContinuousMap.compactOpen
                                                                          Equations
                                                                          • ContinuousMonoidHom.instTopologicalSpace = TopologicalSpace.induced ContinuousMonoidHom.toContinuousMap ContinuousMap.compactOpen
                                                                          theorem ContinuousAddMonoidHom.inducing_toContinuousMap (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] :
                                                                          Inducing ContinuousAddMonoidHom.toContinuousMap
                                                                          theorem ContinuousMonoidHom.inducing_toContinuousMap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] :
                                                                          Inducing ContinuousMonoidHom.toContinuousMap
                                                                          theorem ContinuousAddMonoidHom.embedding_toContinuousMap (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] :
                                                                          Embedding ContinuousAddMonoidHom.toContinuousMap
                                                                          theorem ContinuousMonoidHom.embedding_toContinuousMap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] :
                                                                          Embedding ContinuousMonoidHom.toContinuousMap
                                                                          theorem ContinuousAddMonoidHom.range_toContinuousMap (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] :
                                                                          Set.range ContinuousAddMonoidHom.toContinuousMap = {f : C(A, B) | f 0 = 0 ∀ (x y : A), f (x + y) = f x + f y}
                                                                          theorem ContinuousMonoidHom.range_toContinuousMap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] :
                                                                          Set.range ContinuousMonoidHom.toContinuousMap = {f : C(A, B) | f 1 = 1 ∀ (x y : A), f (x * y) = f x * f y}
                                                                          theorem ContinuousMonoidHom.closedEmbedding_toContinuousMap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [ContinuousMul B] [T2Space B] :
                                                                          ClosedEmbedding ContinuousMonoidHom.toContinuousMap
                                                                          Equations
                                                                          • =
                                                                          theorem ContinuousMonoidHom.continuous_of_continuous_uncurry {B : Type u_3} {C : Type u_4} [Monoid B] [Monoid C] [TopologicalSpace B] [TopologicalSpace C] {A : Type u_7} [TopologicalSpace A] (f : AContinuousMonoidHom B C) (h : Continuous (Function.uncurry fun (x : A) (y : B) => (f x) y)) :
                                                                          theorem ContinuousAddMonoidHom.compLeft.proof_1 {A : Type u_1} {B : Type u_3} (E : Type u_2) [AddMonoid A] [AddMonoid B] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace E] [TopologicalAddGroup E] (f : ContinuousAddMonoidHom A B) :
                                                                          (fun (g : ContinuousAddMonoidHom B E) => g.comp f) 0 = (fun (g : ContinuousAddMonoidHom B E) => g.comp f) 0

                                                                          ContinuousAddMonoidHom _ f is a functor.

                                                                          Equations
                                                                          Instances For
                                                                            theorem ContinuousAddMonoidHom.compLeft.proof_2 {A : Type u_3} {B : Type u_1} (E : Type u_2) [AddMonoid A] [AddMonoid B] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace E] [TopologicalAddGroup E] (f : ContinuousAddMonoidHom A B) (_g : ContinuousAddMonoidHom B E) (_h : ContinuousAddMonoidHom B E) :
                                                                            { toFun := fun (g : ContinuousAddMonoidHom B E) => g.comp f, map_zero' := }.toFun (_g + _h) = { toFun := fun (g : ContinuousAddMonoidHom B E) => g.comp f, map_zero' := }.toFun (_g + _h)

                                                                            ContinuousMonoidHom _ f is a functor.

                                                                            Equations
                                                                            Instances For

                                                                              ContinuousAddMonoidHom f _ is a functor.

                                                                              Equations
                                                                              Instances For
                                                                                theorem ContinuousAddMonoidHom.compRight.proof_2 (A : Type u_1) {E : Type u_3} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] {B : Type u_2} [AddCommGroup B] [TopologicalSpace B] [TopologicalAddGroup B] (f : ContinuousAddMonoidHom B E) (g : ContinuousAddMonoidHom A B) (h : ContinuousAddMonoidHom A B) :
                                                                                { toFun := fun (g : ContinuousAddMonoidHom A B) => f.comp g, map_zero' := }.toFun (g + h) = { toFun := fun (g : ContinuousAddMonoidHom A B) => f.comp g, map_zero' := }.toFun g + { toFun := fun (g : ContinuousAddMonoidHom A B) => f.comp g, map_zero' := }.toFun h

                                                                                ContinuousMonoidHom f _ is a functor.

                                                                                Equations
                                                                                Instances For
                                                                                  abbrev ContinuousAddMonoidHom.locallyCompactSpace_of_equicontinuousAt.match_2 {X : Type u_1} {Y : Type u_2} [AddGroup X] [AddCommGroup Y] (U : Set X) (W : Set Y) (f : XY) (motive : f (U.pi fun (x : X) => W) Set.range DFunLike.coeProp) :
                                                                                  ∀ (x : f (U.pi fun (x : X) => W) Set.range DFunLike.coe), (∀ (hg : f U.pi fun (x : X) => W) (g : X →+ Y) (hf : g = f), motive )motive x
                                                                                  Equations
                                                                                  • =
                                                                                  Instances For
                                                                                    theorem ContinuousAddMonoidHom.locallyCompactSpace_of_equicontinuousAt {X : Type u_7} {Y : Type u_8} [TopologicalSpace X] [AddGroup X] [TopologicalAddGroup X] [UniformSpace Y] [AddCommGroup Y] [UniformAddGroup Y] [T0Space Y] [CompactSpace Y] (U : Set X) (V : Set Y) (hU : IsCompact U) (hV : V nhds 0) (h : EquicontinuousAt (fun (f : {f : X →+ Y | Set.MapsTo (f) U V}) => f) 0) :
                                                                                    abbrev ContinuousAddMonoidHom.locallyCompactSpace_of_equicontinuousAt.match_1 {X : Type u_1} {Y : Type u_2} [AddGroup X] [AddCommGroup Y] (U : Set X) (W : Set Y) (f : XY) (motive : (∃ (x : X →+ Y), Set.MapsTo (x) U W x = f)Prop) :
                                                                                    ∀ (x : ∃ (x : X →+ Y), Set.MapsTo (x) U W x = f), (∀ (g : X →+ Y) (hg : Set.MapsTo (g) U W) (hf : g = f), motive )motive x
                                                                                    Equations
                                                                                    • =
                                                                                    Instances For
                                                                                      theorem ContinuousMonoidHom.locallyCompactSpace_of_equicontinuousAt {X : Type u_7} {Y : Type u_8} [TopologicalSpace X] [Group X] [TopologicalGroup X] [UniformSpace Y] [CommGroup Y] [UniformGroup Y] [T0Space Y] [CompactSpace Y] (U : Set X) (V : Set Y) (hU : IsCompact U) (hV : V nhds 1) (h : EquicontinuousAt (fun (f : {f : X →* Y | Set.MapsTo (f) U V}) => f) 1) :
                                                                                      theorem ContinuousAddMonoidHom.locallyCompactSpace_of_hasBasis {X : Type u_7} {Y : Type u_8} [TopologicalSpace X] [AddGroup X] [TopologicalAddGroup X] [UniformSpace Y] [AddCommGroup Y] [UniformAddGroup Y] [T0Space Y] [CompactSpace Y] [LocallyCompactSpace X] (V : Set Y) (hV : ∀ {n : } {x : Y}, x V nx + x V nx V (n + 1)) (hVo : (nhds 0).HasBasis (fun (x : ) => True) V) :
                                                                                      abbrev ContinuousAddMonoidHom.locallyCompactSpace_of_hasBasis.match_1 {X : Type u_1} {Y : Type u_2} [AddGroup X] [AddCommGroup Y] (V : Set Y) (U : Set X) (motive : {f : X →+ Y | Set.MapsTo (f) (U 0) (V 0)}Prop) :
                                                                                      ∀ (x : {f : X →+ Y | Set.MapsTo (f) (U 0) (V 0)}), (∀ (f : X →+ Y) (hf : f {f : X →+ Y | Set.MapsTo (f) (U 0) (V 0)}), motive f, hf)motive x
                                                                                      Equations
                                                                                      • =
                                                                                      Instances For
                                                                                        theorem ContinuousMonoidHom.locallyCompactSpace_of_hasBasis {X : Type u_7} {Y : Type u_8} [TopologicalSpace X] [Group X] [TopologicalGroup X] [UniformSpace Y] [CommGroup Y] [UniformGroup Y] [T0Space Y] [CompactSpace Y] [LocallyCompactSpace X] (V : Set Y) (hV : ∀ {n : } {x : Y}, x V nx * x V nx V (n + 1)) (hVo : (nhds 1).HasBasis (fun (x : ) => True) V) :