# Continuous Monoid Homs #

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

## Main definitions #

• ContinuousMonoidHom A B: The continuous homomorphisms A →* B.
• ContinuousAddMonoidHom A B: The continuous additive homomorphisms A →+ B.
structure ContinuousAddMonoidHom (A : Type u_7) (B : Type u_8) [] [] [] [] extends :
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} [] [] [] [] (self : ) :
Continuous (self.toAddMonoidHom).toFun

Proof of continuity of the Hom.

structure ContinuousMonoidHom (A : Type u_2) (B : Type u_3) [] [] [] [] extends :
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} [] [] [] [] (self : ) :
Continuous (self.toMonoidHom).toFun

Proof of continuity of the Hom.

class ContinuousAddMonoidHomClass (F : Type u_1) (A : outParam (Type u_7)) (B : outParam (Type u_8)) [] [] [] [] [FunLike F A B] extends :

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),

Proof of the continuity of the map.

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

Proof of the continuity of the map.

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

ContinuousMonoidHomClass F A B states that F is a type of continuous additive 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),

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)} [] [] [] [] [FunLike F A B] [self : ] (f : F) :

Proof of the continuity of the map.

@[instance 100]
instance ContinuousAddMonoidHomClass.toContinuousMapClass (F : Type u_1) (A : Type u_2) (B : Type u_3) [] [] [] [] [FunLike F A B] [] :
Equations
• =
@[instance 100]
instance ContinuousMonoidHomClass.toContinuousMapClass (F : Type u_1) (A : Type u_2) (B : Type u_3) [] [] [] [] [FunLike F A B] [] :
Equations
• =
instance ContinuousAddMonoidHom.funLike {A : Type u_2} {B : Type u_3} [] [] [] [] :
FunLike () A B
Equations
• ContinuousAddMonoidHom.funLike = { coe := fun (f : ) => (f.toAddMonoidHom).toFun, coe_injective' := }
theorem ContinuousAddMonoidHom.funLike.proof_1 {A : Type u_2} {B : Type u_1} [] [] [] [] (f : ) (g : ) (h : (fun (f : ) => (f.toAddMonoidHom).toFun) f = (fun (f : ) => (f.toAddMonoidHom).toFun) g) :
f = g
instance ContinuousMonoidHom.funLike {A : Type u_2} {B : Type u_3} [] [] [] [] :
FunLike () A B
Equations
• ContinuousMonoidHom.funLike = { coe := fun (f : ) => (f.toMonoidHom).toFun, coe_injective' := }
instance ContinuousAddMonoidHom.ContinuousAddMonoidHomClass {A : Type u_2} {B : Type u_3} [] [] [] [] :
Equations
• =
instance ContinuousMonoidHom.ContinuousMonoidHomClass {A : Type u_2} {B : Type u_3} [] [] [] [] :
Equations
• =
theorem ContinuousAddMonoidHom.ext {A : Type u_2} {B : Type u_3} [] [] [] [] {f : } {g : } (h : ∀ (x : A), f x = g x) :
f = g
theorem ContinuousMonoidHom.ext {A : Type u_2} {B : Type u_3} [] [] [] [] {f : } {g : } (h : ∀ (x : A), f x = g x) :
f = g
def ContinuousAddMonoidHom.toContinuousMap {A : Type u_2} {B : Type u_3} [] [] [] [] (f : ) :
C(A, B)

Reinterpret a ContinuousAddMonoidHom as a ContinuousMap.

Equations
• f.toContinuousMap = { toFun := (f.toAddMonoidHom).toFun, continuous_toFun := }
Instances For
def ContinuousMonoidHom.toContinuousMap {A : Type u_2} {B : Type u_3} [] [] [] [] (f : ) :
C(A, B)

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} [] [] [] [] :
Function.Injective ContinuousAddMonoidHom.toContinuousMap
theorem ContinuousMonoidHom.toContinuousMap_injective {A : Type u_2} {B : Type u_3} [] [] [] [] :
Function.Injective ContinuousMonoidHom.toContinuousMap
def ContinuousAddMonoidHom.mk' {A : Type u_2} {B : Type u_3} [] [] [] [] (f : A →+ B) (hf : ) :

Construct a ContinuousAddMonoidHom from a Continuous AddMonoidHom.

Equations
• = { toAddMonoidHom := f, continuous_toFun := hf }
Instances For
def ContinuousMonoidHom.mk' {A : Type u_2} {B : Type u_3} [] [] [] [] (f : A →* B) (hf : ) :

Construct a ContinuousMonoidHom from a Continuous MonoidHom.

Equations
• = { toMonoidHom := f, continuous_toFun := hf }
Instances For
theorem ContinuousAddMonoidHom.comp.proof_1 {A : Type u_1} {B : Type u_3} {C : Type u_2} [] [] [] [] [] [] (g : ) (f : ) :
Continuous ((g.toAddMonoidHom).toFun fun (x : A) => f.toAddMonoidHom x)
def ContinuousAddMonoidHom.comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [] [] [] [] [] [] (g : ) (f : ) :

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} [] [] [] [] [] [] (g : ) (f : ) :
∀ (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} [] [] [] [] [] [] (g : ) (f : ) :
∀ (a : A), (g.comp f) a = g.toMonoidHom (f.toMonoidHom a)
def ContinuousMonoidHom.comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [] [] [] [] [] [] (g : ) (f : ) :

Composition of two continuous homomorphisms.

Equations
Instances For
def ContinuousAddMonoidHom.sum {A : Type u_2} {B : Type u_3} {C : Type u_4} [] [] [] [] [] [] (f : ) (g : ) :

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} [] [] [] [] [] [] (f : ) (g : ) :
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} [] [] [] [] [] [] (f : ) (g : ) (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} [] [] [] [] [] [] (f : ) (g : ) (i : A) :
(f.prod g) i = (f.toMonoidHom i, g.toMonoidHom i)
def ContinuousMonoidHom.prod {A : Type u_2} {B : Type u_3} {C : Type u_4} [] [] [] [] [] [] (f : ) (g : ) :

Product of two continuous homomorphisms on the same space.

Equations
Instances For
def ContinuousAddMonoidHom.sum_map {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [] [] [] [] [] [] [] [] (f : ) (g : ) :

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} [] [] [] [] [] [] [] [] (f : ) (g : ) :
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} [] [] [] [] [] [] [] [] (f : ) (g : ) (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} [] [] [] [] [] [] [] [] (f : ) (g : ) (i : A × B) :
(f.prod_map g) i = (f.toMonoidHom i.1, g.toMonoidHom i.2)
def ContinuousMonoidHom.prod_map {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [] [] [] [] [] [] [] [] (f : ) (g : ) :

Product of two continuous homomorphisms on different spaces.

Equations
Instances For
def ContinuousAddMonoidHom.zero (A : Type u_2) (B : Type u_3) [] [] [] [] :

The trivial continuous homomorphism.

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

The trivial continuous homomorphism.

Equations
Instances For
instance ContinuousAddMonoidHom.instInhabited (A : Type u_2) (B : Type u_3) [] [] [] [] :
Equations
• = { default := }
instance ContinuousMonoidHom.instInhabited (A : Type u_2) (B : Type u_3) [] [] [] [] :
Equations
• = { default := }
def ContinuousAddMonoidHom.id (A : Type u_2) [] [] :

The identity continuous homomorphism.

Equations
Instances For
@[simp]
theorem ContinuousMonoidHom.id_toFun (A : Type u_2) [] [] (x : A) :
= x
@[simp]
theorem ContinuousAddMonoidHom.id_toFun (A : Type u_2) [] [] (x : A) :
= x
def ContinuousMonoidHom.id (A : Type u_2) [] [] :

The identity continuous homomorphism.

Equations
Instances For
def ContinuousAddMonoidHom.fst (A : Type u_2) (B : Type u_3) [] [] [] [] :

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) [] [] [] [] (self : A × B) :
self = self.1
@[simp]
theorem ContinuousMonoidHom.fst_toFun (A : Type u_2) (B : Type u_3) [] [] [] [] (self : A × B) :
() self = self.1
def ContinuousMonoidHom.fst (A : Type u_2) (B : Type u_3) [] [] [] [] :

The continuous homomorphism given by projection onto the first factor.

Equations
Instances For
def ContinuousAddMonoidHom.snd (A : Type u_2) (B : Type u_3) [] [] [] [] :

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) [] [] [] [] (self : A × B) :
self = self.2
@[simp]
theorem ContinuousMonoidHom.snd_toFun (A : Type u_2) (B : Type u_3) [] [] [] [] (self : A × B) :
() self = self.2
def ContinuousMonoidHom.snd (A : Type u_2) (B : Type u_3) [] [] [] [] :

The continuous homomorphism given by projection onto the second factor.

Equations
Instances For
def ContinuousAddMonoidHom.inl (A : Type u_2) (B : Type u_3) [] [] [] [] :

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) [] [] [] [] (i : A) :
() i = (.toMonoidHom i, ().toMonoidHom i)
@[simp]
theorem ContinuousAddMonoidHom.inl_toFun (A : Type u_2) (B : Type u_3) [] [] [] [] (i : A) :
i = (.toAddMonoidHom i, .toAddMonoidHom i)
def ContinuousMonoidHom.inl (A : Type u_2) (B : Type u_3) [] [] [] [] :

The continuous homomorphism given by inclusion of the first factor.

Equations
• = .prod ()
Instances For
def ContinuousAddMonoidHom.inr (A : Type u_2) (B : Type u_3) [] [] [] [] :

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) [] [] [] [] (i : B) :
() i = (().toMonoidHom i, .toMonoidHom i)
@[simp]
theorem ContinuousAddMonoidHom.inr_toFun (A : Type u_2) (B : Type u_3) [] [] [] [] (i : B) :
i = (.toAddMonoidHom i, .toAddMonoidHom i)
def ContinuousMonoidHom.inr (A : Type u_2) (B : Type u_3) [] [] [] [] :

The continuous homomorphism given by inclusion of the second factor.

Equations
• = ().prod
Instances For

The continuous homomorphism given by the diagonal embedding.

Equations
Instances For
@[simp]
theorem ContinuousMonoidHom.diag_toFun (A : Type u_2) [] [] (i : A) :
= (.toMonoidHom i, .toMonoidHom i)
@[simp]
theorem ContinuousAddMonoidHom.diag_toFun (A : Type u_2) [] [] (i : A) :
= (.toAddMonoidHom i, .toAddMonoidHom i)

The continuous homomorphism given by the diagonal embedding.

Equations
Instances For
def ContinuousAddMonoidHom.swap (A : Type u_2) (B : Type u_3) [] [] [] [] :

The continuous homomorphism given by swapping components.

Equations
• = .sum
Instances For
@[simp]
theorem ContinuousAddMonoidHom.swap_toFun (A : Type u_2) (B : Type u_3) [] [] [] [] (i : A × B) :
i = (.toAddMonoidHom i, .toAddMonoidHom i)
@[simp]
theorem ContinuousMonoidHom.swap_toFun (A : Type u_2) (B : Type u_3) [] [] [] [] (i : A × B) :
() i = (().toMonoidHom i, ().toMonoidHom i)
def ContinuousMonoidHom.swap (A : Type u_2) (B : Type u_3) [] [] [] [] :

The continuous homomorphism given by swapping components.

Equations
• = ().prod ()
Instances For

The continuous homomorphism given by addition.

Equations
Instances For
theorem ContinuousAddMonoidHom.add.proof_1 (E : Type u_1) [] [] :
Continuous fun (p : E × E) => p.1 + p.2
@[simp]
theorem ContinuousAddMonoidHom.add_toFun (E : Type u_6) [] [] :
∀ (a : E × E), = a.1 + a.2
@[simp]
theorem ContinuousMonoidHom.mul_toFun (E : Type u_6) [] [] [] :
∀ (a : E × E), = a.1 * a.2
def ContinuousMonoidHom.mul (E : Type u_6) [] [] [] :

The continuous homomorphism given by multiplication.

Equations
Instances For
theorem ContinuousAddMonoidHom.neg.proof_1 (E : Type u_1) [] [] :
Continuous fun (a : E) => -a
def ContinuousAddMonoidHom.neg (E : Type u_6) [] [] :

The continuous homomorphism given by negation.

Equations
Instances For
@[simp]
theorem ContinuousAddMonoidHom.neg_toFun (E : Type u_6) [] [] :
∀ (a : E), = -a
@[simp]
theorem ContinuousMonoidHom.inv_toFun (E : Type u_6) [] [] [] :
∀ (a : E), = a⁻¹
def ContinuousMonoidHom.inv (E : Type u_6) [] [] [] :

The continuous homomorphism given by inversion.

Equations
Instances For
def ContinuousAddMonoidHom.coprod {A : Type u_2} {B : Type u_3} {E : Type u_6} [] [] [] [] [] [] (f : ) (g : ) :

Coproduct of two continuous homomorphisms to the same space.

Equations
• f.coprod g = .comp (f.sum_map g)
Instances For
@[simp]
theorem ContinuousMonoidHom.coprod_toFun {A : Type u_2} {B : Type u_3} {E : Type u_6} [] [] [] [] [] [] [] (f : ) (g : ) :
∀ (a : A × B), (f.coprod g) a = .toMonoidHom ((f.prod_map g).toMonoidHom a)
@[simp]
theorem ContinuousAddMonoidHom.coprod_toFun {A : Type u_2} {B : Type u_3} {E : Type u_6} [] [] [] [] [] [] (f : ) (g : ) :
∀ (a : A × B), (f.coprod g) a = .toAddMonoidHom ((f.sum_map g).toAddMonoidHom a)
def ContinuousMonoidHom.coprod {A : Type u_2} {B : Type u_3} {E : Type u_6} [] [] [] [] [] [] [] (f : ) (g : ) :

Coproduct of two continuous homomorphisms to the same space.

Equations
• f.coprod g = .comp (f.prod_map g)
Instances For
theorem ContinuousAddMonoidHom.instAddCommGroup.proof_1 {A : Type u_2} {E : Type u_1} [] [] [] [] (f : ) (g : ) (h : ) :
f + g + h = f + (g + h)
theorem ContinuousAddMonoidHom.instAddCommGroup.proof_10 {A : Type u_2} {E : Type u_1} [] [] [] [] :
∀ (a : ), zsmulRec 0 a = zsmulRec 0 a
theorem ContinuousAddMonoidHom.instAddCommGroup.proof_14 {A : Type u_2} {E : Type u_1} [] [] [] [] (f : ) (g : ) :
f + g = g + f
theorem ContinuousAddMonoidHom.instAddCommGroup.proof_5 {A : Type u_2} {E : Type u_1} [] [] [] [] :
∀ (n : ) (x : ), nsmulRec (n + 1) x = nsmulRec (n + 1) x
instance ContinuousAddMonoidHom.instAddCommGroup {A : Type u_2} {E : Type u_6} [] [] [] [] :
Equations
• ContinuousAddMonoidHom.instAddCommGroup =
theorem ContinuousAddMonoidHom.instAddCommGroup.proof_2 {A : Type u_2} {E : Type u_1} [] [] [] [] (f : ) :
0 + f = f
theorem ContinuousAddMonoidHom.instAddCommGroup.proof_4 {A : Type u_2} {E : Type u_1} [] [] [] [] :
∀ (x : ), nsmulRec 0 x = nsmulRec 0 x
theorem ContinuousAddMonoidHom.instAddCommGroup.proof_8 {A : Type u_2} {E : Type u_1} [] [] [] [] (f : ) :
f + 0 = f
theorem ContinuousAddMonoidHom.instAddCommGroup.proof_3 {A : Type u_2} {E : Type u_1} [] [] [] [] (f : ) :
f + 0 = f
theorem ContinuousAddMonoidHom.instAddCommGroup.proof_13 {A : Type u_2} {E : Type u_1} [] [] [] [] (f : ) :
-f + f = 0
theorem ContinuousAddMonoidHom.instAddCommGroup.proof_6 {A : Type u_2} {E : Type u_1} [] [] [] [] (f : ) (g : ) (h : ) :
f + g + h = f + (g + h)
theorem ContinuousAddMonoidHom.instAddCommGroup.proof_12 {A : Type u_2} {E : Type u_1} [] [] [] [] :
∀ (n : ) (a : ), zsmulRec () a = zsmulRec () a
theorem ContinuousAddMonoidHom.instAddCommGroup.proof_9 {A : Type u_2} {E : Type u_1} [] [] [] [] :
∀ (a b : ), a - b = a - b
theorem ContinuousAddMonoidHom.instAddCommGroup.proof_11 {A : Type u_2} {E : Type u_1} [] [] [] [] :
∀ (n : ) (a : ), zsmulRec (Int.ofNat n.succ) a = zsmulRec (Int.ofNat n.succ) a
theorem ContinuousAddMonoidHom.instAddCommGroup.proof_7 {A : Type u_2} {E : Type u_1} [] [] [] [] (f : ) :
0 + f = f
instance ContinuousMonoidHom.instCommGroup {A : Type u_2} {E : Type u_6} [] [] [] [] [] :
Equations
• ContinuousMonoidHom.instCommGroup =
instance ContinuousAddMonoidHom.instTopologicalSpace {A : Type u_2} {B : Type u_3} [] [] [] [] :
Equations
• ContinuousAddMonoidHom.instTopologicalSpace = TopologicalSpace.induced ContinuousAddMonoidHom.toContinuousMap ContinuousMap.compactOpen
instance ContinuousMonoidHom.instTopologicalSpace {A : Type u_2} {B : Type u_3} [] [] [] [] :
Equations
• ContinuousMonoidHom.instTopologicalSpace = TopologicalSpace.induced ContinuousMonoidHom.toContinuousMap ContinuousMap.compactOpen
theorem ContinuousAddMonoidHom.inducing_toContinuousMap (A : Type u_2) (B : Type u_3) [] [] [] [] :
Inducing ContinuousAddMonoidHom.toContinuousMap
theorem ContinuousMonoidHom.inducing_toContinuousMap (A : Type u_2) (B : Type u_3) [] [] [] [] :
Inducing ContinuousMonoidHom.toContinuousMap
theorem ContinuousAddMonoidHom.embedding_toContinuousMap (A : Type u_2) (B : Type u_3) [] [] [] [] :
Embedding ContinuousAddMonoidHom.toContinuousMap
theorem ContinuousMonoidHom.embedding_toContinuousMap (A : Type u_2) (B : Type u_3) [] [] [] [] :
Embedding ContinuousMonoidHom.toContinuousMap
theorem ContinuousAddMonoidHom.range_toContinuousMap (A : Type u_2) (B : Type u_3) [] [] [] [] :
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) [] [] [] [] :
Set.range ContinuousMonoidHom.toContinuousMap = {f : C(A, B) | f 1 = 1 ∀ (x y : A), f (x * y) = f x * f y}
theorem ContinuousAddMonoidHom.closedEmbedding_toContinuousMap (A : Type u_2) (B : Type u_3) [] [] [] [] [] [] :
ClosedEmbedding ContinuousAddMonoidHom.toContinuousMap
theorem ContinuousMonoidHom.closedEmbedding_toContinuousMap (A : Type u_2) (B : Type u_3) [] [] [] [] [] [] :
ClosedEmbedding ContinuousMonoidHom.toContinuousMap
instance ContinuousAddMonoidHom.instT2Space {A : Type u_2} {B : Type u_3} [] [] [] [] [] :
Equations
• =
instance ContinuousMonoidHom.instT2Space {A : Type u_2} {B : Type u_3} [] [] [] [] [] :
Equations
• =
instance ContinuousAddMonoidHom.instTopologicalAddGroup {A : Type u_2} {E : Type u_6} [] [] [] [] :
Equations
• =
instance ContinuousMonoidHom.instTopologicalGroup {A : Type u_2} {E : Type u_6} [] [] [] [] [] :
Equations
• =
theorem ContinuousAddMonoidHom.continuous_of_continuous_uncurry {B : Type u_3} {C : Type u_4} [] [] [] [] {A : Type u_7} [] (f : A) (h : Continuous (Function.uncurry fun (x : A) (y : B) => (f x) y)) :
theorem ContinuousMonoidHom.continuous_of_continuous_uncurry {B : Type u_3} {C : Type u_4} [] [] [] [] {A : Type u_7} [] (f : A) (h : Continuous (Function.uncurry fun (x : A) (y : B) => (f x) y)) :
theorem ContinuousAddMonoidHom.continuous_comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [] [] [] [] [] [] :
Continuous fun (f : ) => f.2.comp f.1
theorem ContinuousMonoidHom.continuous_comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [] [] [] [] [] [] :
Continuous fun (f : ) => f.2.comp f.1
theorem ContinuousAddMonoidHom.continuous_comp_left {A : Type u_2} {B : Type u_3} {C : Type u_4} [] [] [] [] [] [] (f : ) :
Continuous fun (g : ) => g.comp f
theorem ContinuousMonoidHom.continuous_comp_left {A : Type u_2} {B : Type u_3} {C : Type u_4} [] [] [] [] [] [] (f : ) :
Continuous fun (g : ) => g.comp f
theorem ContinuousAddMonoidHom.continuous_comp_right {A : Type u_2} {B : Type u_3} {C : Type u_4} [] [] [] [] [] [] (f : ) :
Continuous fun (g : ) => f.comp g
theorem ContinuousMonoidHom.continuous_comp_right {A : Type u_2} {B : Type u_3} {C : Type u_4} [] [] [] [] [] [] (f : ) :
Continuous fun (g : ) => f.comp g
theorem ContinuousAddMonoidHom.compLeft.proof_2 {A : Type u_3} {B : Type u_2} (E : Type u_1) [] [] [] [] [] [] (f : ) (_g : ) (_h : ) :
{ toFun := fun (g : ) => g.comp f, map_zero' := }.toFun (_g + _h) = { toFun := fun (g : ) => g.comp f, map_zero' := }.toFun (_g + _h)
theorem ContinuousAddMonoidHom.compLeft.proof_1 {A : Type u_1} {B : Type u_3} (E : Type u_2) [] [] [] [] [] [] (f : ) :
(fun (g : ) => g.comp f) 0 = (fun (g : ) => g.comp f) 0
theorem ContinuousAddMonoidHom.compLeft.proof_3 {A : Type u_3} {B : Type u_1} (E : Type u_2) [] [] [] [] [] [] (f : ) :
Continuous fun (g : ) => g.comp f
def ContinuousAddMonoidHom.compLeft {A : Type u_2} {B : Type u_3} (E : Type u_6) [] [] [] [] [] [] (f : ) :

ContinuousAddMonoidHom _ f is a functor.

Equations
• = { toFun := fun (g : ) => g.comp f, map_zero' := , map_add' := , continuous_toFun := }
Instances For
def ContinuousMonoidHom.compLeft {A : Type u_2} {B : Type u_3} (E : Type u_6) [] [] [] [] [] [] [] (f : ) :

ContinuousMonoidHom _ f is a functor.

Equations
• = { toFun := fun (g : ) => g.comp f, map_one' := , map_mul' := , continuous_toFun := }
Instances For
theorem ContinuousAddMonoidHom.compRight.proof_1 (A : Type u_1) {E : Type u_2} [] [] [] [] {B : Type u_3} [] [] (f : ) :
(fun (g : ) => f.comp g) 0 = 0
def ContinuousAddMonoidHom.compRight (A : Type u_2) {E : Type u_6} [] [] [] [] {B : Type u_7} [] [] (f : ) :

ContinuousAddMonoidHom f _ is a functor.

Equations
• = { toFun := fun (g : ) => f.comp g, map_zero' := , map_add' := , continuous_toFun := }
Instances For
theorem ContinuousAddMonoidHom.compRight.proof_2 (A : Type u_2) {E : Type u_3} [] [] [] [] {B : Type u_1} [] [] (f : ) (g : ) (h : ) :
{ toFun := fun (g : ) => f.comp g, map_zero' := }.toFun (g + h) = { toFun := fun (g : ) => f.comp g, map_zero' := }.toFun g + { toFun := fun (g : ) => f.comp g, map_zero' := }.toFun h
theorem ContinuousAddMonoidHom.compRight.proof_3 (A : Type u_1) {E : Type u_3} [] [] [] [] {B : Type u_2} [] [] (f : ) :
Continuous fun (g : ) => f.comp g
def ContinuousMonoidHom.compRight (A : Type u_2) {E : Type u_6} [] [] [] [] [] {B : Type u_7} [] [] [] (f : ) :

ContinuousMonoidHom f _ is a functor.

Equations
• = { toFun := fun (g : ) => f.comp g, map_one' := , map_mul' := , continuous_toFun := }
Instances For