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) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] extends A →+ B, C(A, B) : Type (max u_7 u_8)

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

• toFun : A → B
• 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

structure ContinuousMonoidHom (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] extends A →* B, C(A, B) : 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*) [FunLike F A B] [ContinuousMapClass F A B] [MonoidHomClass F A B] (f : F).

When you extend this structure, make sure to extend ContinuousMapClass and/or MonoidHomClass, if needed.

• toFun : A → B
• 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

@[deprecated "Use `[MonoidHomClass F A B] [ContinuousMapClass F A B]` instead." (since := "2024-10-08")]

structure ContinuousAddMonoidHomClass (F : Type u_1) (A : outParam (Type u_7)) (B : outParam (Type u_8)) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] [FunLike F A B] extends AddMonoidHomClass F A B, ContinuousMapClass F A B : Prop

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

Deprecated and changed from a class to a structure. Use [AddMonoidHomClass F A B] [ContinuousMapClass F A B] instead.

• 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

@[deprecated "Use `[MonoidHomClass F A B] [ContinuousMapClass F A B]` instead." (since := "2024-10-08")]

structure 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 F A B, ContinuousMapClass F A B : Prop

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

Deprecated and changed from a class to a structure. Use [MonoidHomClass F A B] [ContinuousMapClass F A B] instead.

• 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

instance ContinuousMonoidHom.instFunLike {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : FunLike (ContinuousMonoidHom A B) A B

Equations

• ContinuousMonoidHom.instFunLike = { coe := fun (f : ContinuousMonoidHom A B) => (↑f.toMonoidHom).toFun, coe_injective' := ⋯ }

instance ContinuousAddMonoidHom.instFunLike {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : FunLike (ContinuousAddMonoidHom A B) A B

Equations

• ContinuousAddMonoidHom.instFunLike = { coe := fun (f : ContinuousAddMonoidHom A B) => (↑f.toAddMonoidHom).toFun, coe_injective' := ⋯ }

instance ContinuousMonoidHom.instMonoidHomClass {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : MonoidHomClass (ContinuousMonoidHom A B) A B

instance ContinuousAddMonoidHom.instAddMonoidHomClass {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : AddMonoidHomClass (ContinuousAddMonoidHom A B) A B

instance ContinuousMonoidHom.instContinuousMapClass {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousMapClass (ContinuousMonoidHom A B) A B

instance ContinuousAddMonoidHom.instContinuousMapClass {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousMapClass (ContinuousAddMonoidHom A B) A B

theorem ContinuousAddMonoidHom.ext {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] {f 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 g : ContinuousMonoidHom A B} (h : ∀ (x : A), f x = g x) : f = g

theorem ContinuousMonoidHom.toContinuousMap_injective {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : Function.Injective ContinuousMonoidHom.toContinuousMap

theorem ContinuousAddMonoidHom.toContinuousMap_injective {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : Function.Injective ContinuousAddMonoidHom.toContinuousMap

@[deprecated ContinuousMonoidHom.mk (since := "2024-10-08")]

def ContinuousMonoidHom.mk' {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (toMonoidHom : A →* B) (continuous_toFun : Continuous (↑toMonoidHom).toFun := by continuity) : ContinuousMonoidHom A B

Alias of ContinuousMonoidHom.mk.

Equations

• @ContinuousMonoidHom.mk' = @ContinuousMonoidHom.mk

@[deprecated ContinuousAddMonoidHom.mk (since := "2024-10-08")]

def ContinuousAddMonoidHom.mk' {A : Type u_7} {B : Type u_8} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (toAddMonoidHom : A →+ B) (continuous_toFun : Continuous (↑toAddMonoidHom).toFun := by continuity) : ContinuousAddMonoidHom A B

Alias of ContinuousAddMonoidHom.mk.

Equations

• @ContinuousAddMonoidHom.mk' = @ContinuousAddMonoidHom.mk

def ContinuousMonoidHom.comp {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) : ContinuousMonoidHom A C

Composition of two continuous homomorphisms.

Equations

• g.comp f = { toMonoidHom := g.comp f.toMonoidHom, continuous_toFun := ⋯ }

def ContinuousAddMonoidHom.comp {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) : ContinuousAddMonoidHom A C

Composition of two continuous homomorphisms.

Equations

• g.comp f = { toAddMonoidHom := g.comp f.toAddMonoidHom, continuous_toFun := ⋯ }

@[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✝)

def ContinuousMonoidHom.prod {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) : ContinuousMonoidHom A (B × C)

Product of two continuous homomorphisms on the same space.

Equations

• f.prod g = { toMonoidHom := f.prod g.toMonoidHom, continuous_toFun := ⋯ }

def ContinuousAddMonoidHom.prod {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) : ContinuousAddMonoidHom A (B × C)

Product of two continuous homomorphisms on the same space.

Equations

• f.prod g = { toAddMonoidHom := f.prod g.toAddMonoidHom, continuous_toFun := ⋯ }

@[simp]

theorem ContinuousAddMonoidHom.prod_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.prod 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)

def ContinuousMonoidHom.prodMap {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) : ContinuousMonoidHom (A × B) (C × D)

Product of two continuous homomorphisms on different spaces.

Equations

• f.prodMap g = { toMonoidHom := f.prodMap g.toMonoidHom, continuous_toFun := ⋯ }

def ContinuousAddMonoidHom.prodMap {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) : ContinuousAddMonoidHom (A × B) (C × D)

Product of two continuous homomorphisms on different spaces.

Equations

• f.prodMap g = { toAddMonoidHom := f.prodMap g.toAddMonoidHom, continuous_toFun := ⋯ }

@[simp]

theorem ContinuousAddMonoidHom.prodMap_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.prodMap g) i = (f.toAddMonoidHom i.1, g.toAddMonoidHom i.2)

@[simp]

theorem ContinuousMonoidHom.prodMap_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.prodMap g) i = (f.toMonoidHom i.1, g.toMonoidHom i.2)

@[deprecated ContinuousMonoidHom.prodMap (since := "2024-10-05")]

def ContinuousMonoidHom.prod_map {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) : ContinuousMonoidHom (A × B) (C × D)

Alias of ContinuousMonoidHom.prodMap.

---

Product of two continuous homomorphisms on different spaces.

Equations

• @ContinuousMonoidHom.prod_map = @ContinuousMonoidHom.prodMap

@[deprecated ContinuousAddMonoidHom.prodMap (since := "2024-10-05")]

def ContinuousAddMonoidHom.sum_map {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) : ContinuousAddMonoidHom (A × B) (C × D)

Alias of ContinuousAddMonoidHom.prodMap.

---

Product of two continuous homomorphisms on different spaces.

Equations

• @ContinuousAddMonoidHom.sum_map = @ContinuousAddMonoidHom.prodMap

def ContinuousMonoidHom.one (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousMonoidHom A B

The trivial continuous homomorphism.

Equations

• ContinuousMonoidHom.one A B = { toMonoidHom := 1, continuous_toFun := ⋯ }

def ContinuousAddMonoidHom.zero (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousAddMonoidHom A B

The trivial continuous homomorphism.

Equations

• ContinuousAddMonoidHom.zero A B = { toAddMonoidHom := 0, continuous_toFun := ⋯ }

@[simp]

theorem ContinuousAddMonoidHom.zero_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (x✝ : A) : (ContinuousAddMonoidHom.zero A B) x✝ = 0

@[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

instance ContinuousMonoidHom.instInhabited (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : Inhabited (ContinuousMonoidHom A B)

Equations

• ContinuousMonoidHom.instInhabited A B = { default := ContinuousMonoidHom.one A B }

instance ContinuousAddMonoidHom.instInhabited (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : Inhabited (ContinuousAddMonoidHom A B)

Equations

• ContinuousAddMonoidHom.instInhabited A B = { default := ContinuousAddMonoidHom.zero A B }

def ContinuousMonoidHom.id (A : Type u_2) [Monoid A] [TopologicalSpace A] : ContinuousMonoidHom A A

The identity continuous homomorphism.

Equations

• ContinuousMonoidHom.id A = { toMonoidHom := MonoidHom.id A, continuous_toFun := ⋯ }

def ContinuousAddMonoidHom.id (A : Type u_2) [AddMonoid A] [TopologicalSpace A] : ContinuousAddMonoidHom A A

The identity continuous homomorphism.

Equations

• ContinuousAddMonoidHom.id A = { toAddMonoidHom := AddMonoidHom.id A, continuous_toFun := ⋯ }

@[simp]

theorem ContinuousMonoidHom.id_toFun (A : Type u_2) [Monoid A] [TopologicalSpace A] (x : A) : (ContinuousMonoidHom.id A) x = x

@[simp]

theorem ContinuousAddMonoidHom.id_toFun (A : Type u_2) [AddMonoid A] [TopologicalSpace A] (x : A) : (ContinuousAddMonoidHom.id A) x = x

def ContinuousMonoidHom.fst (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousMonoidHom (A × B) A

The continuous homomorphism given by projection onto the first factor.

Equations

• ContinuousMonoidHom.fst A B = { toMonoidHom := MonoidHom.fst A B, continuous_toFun := ⋯ }

def ContinuousAddMonoidHom.fst (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousAddMonoidHom (A × B) A

The continuous homomorphism given by projection onto the first factor.

Equations

• ContinuousAddMonoidHom.fst A B = { toAddMonoidHom := AddMonoidHom.fst A B, continuous_toFun := ⋯ }

@[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

@[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

def ContinuousMonoidHom.snd (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousMonoidHom (A × B) B

The continuous homomorphism given by projection onto the second factor.

Equations

• ContinuousMonoidHom.snd A B = { toMonoidHom := MonoidHom.snd A B, continuous_toFun := ⋯ }

def ContinuousAddMonoidHom.snd (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousAddMonoidHom (A × B) B

The continuous homomorphism given by projection onto the second factor.

Equations

• ContinuousAddMonoidHom.snd A B = { toAddMonoidHom := AddMonoidHom.snd A B, continuous_toFun := ⋯ }

@[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

@[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

def ContinuousMonoidHom.inl (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousMonoidHom A (A × B)

The continuous homomorphism given by inclusion of the first factor.

Equations

• ContinuousMonoidHom.inl A B = (ContinuousMonoidHom.id A).prod (ContinuousMonoidHom.one A B)

def ContinuousAddMonoidHom.inl (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousAddMonoidHom A (A × B)

The continuous homomorphism given by inclusion of the first factor.

Equations

• ContinuousAddMonoidHom.inl A B = (ContinuousAddMonoidHom.id A).prod (ContinuousAddMonoidHom.zero A B)

@[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)

@[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)

def ContinuousMonoidHom.inr (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousMonoidHom B (A × B)

The continuous homomorphism given by inclusion of the second factor.

Equations

• ContinuousMonoidHom.inr A B = (ContinuousMonoidHom.one B A).prod (ContinuousMonoidHom.id B)

def ContinuousAddMonoidHom.inr (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousAddMonoidHom B (A × B)

The continuous homomorphism given by inclusion of the second factor.

Equations

• ContinuousAddMonoidHom.inr A B = (ContinuousAddMonoidHom.zero B A).prod (ContinuousAddMonoidHom.id B)

@[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)

@[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)

def ContinuousMonoidHom.diag (A : Type u_2) [Monoid A] [TopologicalSpace A] : ContinuousMonoidHom A (A × A)

The continuous homomorphism given by the diagonal embedding.

Equations

• ContinuousMonoidHom.diag A = (ContinuousMonoidHom.id A).prod (ContinuousMonoidHom.id A)

def ContinuousAddMonoidHom.diag (A : Type u_2) [AddMonoid A] [TopologicalSpace A] : ContinuousAddMonoidHom A (A × A)

The continuous homomorphism given by the diagonal embedding.

Equations

• ContinuousAddMonoidHom.diag A = (ContinuousAddMonoidHom.id A).prod (ContinuousAddMonoidHom.id A)

@[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]

theorem ContinuousAddMonoidHom.diag_toFun (A : Type u_2) [AddMonoid A] [TopologicalSpace A] (i : A) : (ContinuousAddMonoidHom.diag A) i = ((ContinuousAddMonoidHom.id A).toAddMonoidHom i, (ContinuousAddMonoidHom.id A).toAddMonoidHom i)

def ContinuousMonoidHom.swap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousMonoidHom (A × B) (B × A)

The continuous homomorphism given by swapping components.

Equations

• ContinuousMonoidHom.swap A B = (ContinuousMonoidHom.snd A B).prod (ContinuousMonoidHom.fst A B)

def ContinuousAddMonoidHom.swap (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousAddMonoidHom (A × B) (B × A)

The continuous homomorphism given by swapping components.

Equations

• ContinuousAddMonoidHom.swap A B = (ContinuousAddMonoidHom.snd A B).prod (ContinuousAddMonoidHom.fst A B)

@[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)

def ContinuousMonoidHom.mul (E : Type u_6) [CommGroup E] [TopologicalSpace E] [TopologicalGroup E] : ContinuousMonoidHom (E × E) E

The continuous homomorphism given by multiplication.

Equations

• ContinuousMonoidHom.mul E = { toMonoidHom := mulMonoidHom, continuous_toFun := ⋯ }

def ContinuousAddMonoidHom.add (E : Type u_6) [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] : ContinuousAddMonoidHom (E × E) E

The continuous homomorphism given by addition.

Equations

• ContinuousAddMonoidHom.add E = { toAddMonoidHom := addAddMonoidHom, continuous_toFun := ⋯ }

@[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

@[simp]

theorem ContinuousAddMonoidHom.add_toFun (E : Type u_6) [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] (a✝ : E × E) : (ContinuousAddMonoidHom.add E) a✝ = a✝.1 + a✝.2

def ContinuousMonoidHom.inv (E : Type u_6) [CommGroup E] [TopologicalSpace E] [TopologicalGroup E] : ContinuousMonoidHom E E

The continuous homomorphism given by inversion.

Equations

• ContinuousMonoidHom.inv E = { toMonoidHom := invMonoidHom, continuous_toFun := ⋯ }

def ContinuousAddMonoidHom.neg (E : Type u_6) [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] : ContinuousAddMonoidHom E E

The continuous homomorphism given by negation.

Equations

• ContinuousAddMonoidHom.neg E = { toAddMonoidHom := negAddMonoidHom, continuous_toFun := ⋯ }

@[simp]

theorem ContinuousMonoidHom.inv_toFun (E : Type u_6) [CommGroup E] [TopologicalSpace E] [TopologicalGroup E] (a✝ : E) : (ContinuousMonoidHom.inv E) a✝ = a✝⁻¹

@[simp]

theorem ContinuousAddMonoidHom.neg_toFun (E : Type u_6) [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] (a✝ : E) : (ContinuousAddMonoidHom.neg E) a✝ = -a✝

def ContinuousMonoidHom.coprod {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) : ContinuousMonoidHom (A × B) E

Coproduct of two continuous homomorphisms to the same space.

Equations

• f.coprod g = (ContinuousMonoidHom.mul E).comp (f.prodMap g)

def ContinuousAddMonoidHom.coprod {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) : ContinuousAddMonoidHom (A × B) E

Coproduct of two continuous homomorphisms to the same space.

Equations

• f.coprod g = (ContinuousAddMonoidHom.add E).comp (f.prodMap g)

@[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.prodMap 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.prodMap g).toMonoidHom a✝)

instance ContinuousMonoidHom.instCommGroup {A : Type u_2} {E : Type u_6} [Monoid A] [CommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalGroup E] : CommGroup (ContinuousMonoidHom A E)

Equations

• ContinuousMonoidHom.instCommGroup = CommGroup.mk ⋯

instance ContinuousAddMonoidHom.instAddCommGroup {A : Type u_2} {E : Type u_6} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] : AddCommGroup (ContinuousAddMonoidHom A E)

Equations

• ContinuousAddMonoidHom.instAddCommGroup = AddCommGroup.mk ⋯

instance ContinuousMonoidHom.instTopologicalSpace {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : TopologicalSpace (ContinuousMonoidHom A B)

Equations

• ContinuousMonoidHom.instTopologicalSpace = TopologicalSpace.induced ContinuousMonoidHom.toContinuousMap ContinuousMap.compactOpen

instance ContinuousAddMonoidHom.instTopologicalSpace {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : TopologicalSpace (ContinuousAddMonoidHom A B)

Equations

• ContinuousAddMonoidHom.instTopologicalSpace = TopologicalSpace.induced ContinuousAddMonoidHom.toContinuousMap ContinuousMap.compactOpen

theorem ContinuousMonoidHom.isInducing_toContinuousMap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : Topology.IsInducing ContinuousMonoidHom.toContinuousMap

theorem ContinuousAddMonoidHom.isInducing_toContinuousMap (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : Topology.IsInducing ContinuousAddMonoidHom.toContinuousMap

@[deprecated ContinuousMonoidHom.isInducing_toContinuousMap (since := "2024-10-28")]

theorem ContinuousMonoidHom.inducing_toContinuousMap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : Topology.IsInducing ContinuousMonoidHom.toContinuousMap

Alias of ContinuousMonoidHom.isInducing_toContinuousMap.

theorem ContinuousMonoidHom.isEmbedding_toContinuousMap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : Topology.IsEmbedding ContinuousMonoidHom.toContinuousMap

theorem ContinuousAddMonoidHom.isEmbedding_toContinuousMap (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : Topology.IsEmbedding ContinuousAddMonoidHom.toContinuousMap

@[deprecated ContinuousMonoidHom.isEmbedding_toContinuousMap (since := "2024-10-26")]

theorem ContinuousMonoidHom.embedding_toContinuousMap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : Topology.IsEmbedding ContinuousMonoidHom.toContinuousMap

Alias of ContinuousMonoidHom.isEmbedding_toContinuousMap.

instance ContinuousMonoidHom.instContinuousEvalConst (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousEvalConst (ContinuousMonoidHom A B) A B

instance ContinuousAddMonoidHom.instContinuousEvalConst (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousEvalConst (ContinuousAddMonoidHom A B) A B

instance ContinuousMonoidHom.instContinuousEval (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [LocallyCompactPair A B] : ContinuousEval (ContinuousMonoidHom A B) A B

instance ContinuousAddMonoidHom.instContinuousEval (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] [LocallyCompactPair A B] : ContinuousEval (ContinuousAddMonoidHom A B) A B

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 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.isClosedEmbedding_toContinuousMap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [ContinuousMul B] [T2Space B] : Topology.IsClosedEmbedding ContinuousMonoidHom.toContinuousMap

theorem ContinuousAddMonoidHom.isClosedEmbedding_toContinuousMap (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] [ContinuousAdd B] [T2Space B] : Topology.IsClosedEmbedding ContinuousAddMonoidHom.toContinuousMap

@[deprecated ContinuousMonoidHom.isClosedEmbedding_toContinuousMap (since := "2024-10-20")]

theorem ContinuousMonoidHom.closedEmbedding_toContinuousMap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [ContinuousMul B] [T2Space B] : Topology.IsClosedEmbedding ContinuousMonoidHom.toContinuousMap

Alias of ContinuousMonoidHom.isClosedEmbedding_toContinuousMap.

instance ContinuousMonoidHom.instT2Space {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [T2Space B] : T2Space (ContinuousMonoidHom A B)

instance ContinuousAddMonoidHom.instT2Space {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] [T2Space B] : T2Space (ContinuousAddMonoidHom A B)

instance ContinuousMonoidHom.instTopologicalGroup {A : Type u_2} {E : Type u_6} [Monoid A] [CommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalGroup E] : TopologicalGroup (ContinuousMonoidHom A E)

instance ContinuousAddMonoidHom.instTopologicalAddGroup {A : Type u_2} {E : Type u_6} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] : TopologicalAddGroup (ContinuousAddMonoidHom A E)

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 : A → ContinuousMonoidHom B C) (h : Continuous (Function.uncurry fun (x : A) (y : B) => (f x) y)) : Continuous f

theorem ContinuousAddMonoidHom.continuous_of_continuous_uncurry {B : Type u_3} {C : Type u_4} [AddMonoid B] [AddMonoid C] [TopologicalSpace B] [TopologicalSpace C] {A : Type u_7} [TopologicalSpace A] (f : A → ContinuousAddMonoidHom B C) (h : Continuous (Function.uncurry fun (x : A) (y : B) => (f x) y)) : Continuous f

theorem ContinuousMonoidHom.continuous_comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid A] [Monoid B] [Monoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [LocallyCompactSpace B] : Continuous fun (f : ContinuousMonoidHom A B × ContinuousMonoidHom B C) => f.2.comp f.1

theorem ContinuousAddMonoidHom.continuous_comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [LocallyCompactSpace B] : Continuous fun (f : ContinuousAddMonoidHom A B × ContinuousAddMonoidHom B C) => f.2.comp f.1

theorem ContinuousMonoidHom.continuous_comp_left {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) : Continuous fun (g : ContinuousMonoidHom B C) => g.comp f

theorem ContinuousAddMonoidHom.continuous_comp_left {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) : Continuous fun (g : ContinuousAddMonoidHom B C) => g.comp f

theorem ContinuousMonoidHom.continuous_comp_right {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 B C) : Continuous fun (g : ContinuousMonoidHom A B) => f.comp g

theorem ContinuousAddMonoidHom.continuous_comp_right {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 B C) : Continuous fun (g : ContinuousAddMonoidHom A B) => f.comp g

def ContinuousMonoidHom.compLeft {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 B) : ContinuousMonoidHom (ContinuousMonoidHom B E) (ContinuousMonoidHom A E)

ContinuousMonoidHom _ f is a functor.

Equations

• ContinuousMonoidHom.compLeft E f = { toFun := fun (g : ContinuousMonoidHom B E) => g.comp f, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }

def ContinuousAddMonoidHom.compLeft {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 B) : ContinuousAddMonoidHom (ContinuousAddMonoidHom B E) (ContinuousAddMonoidHom A E)

ContinuousAddMonoidHom _ f is a functor.

Equations

• ContinuousAddMonoidHom.compLeft E f = { toFun := fun (g : ContinuousAddMonoidHom B E) => g.comp f, map_zero' := ⋯, map_add' := ⋯, continuous_toFun := ⋯ }

def ContinuousMonoidHom.compRight (A : Type u_2) {E : Type u_6} [Monoid A] [CommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalGroup E] {B : Type u_7} [CommGroup B] [TopologicalSpace B] [TopologicalGroup B] (f : ContinuousMonoidHom B E) : ContinuousMonoidHom (ContinuousMonoidHom A B) (ContinuousMonoidHom A E)

ContinuousMonoidHom f _ is a functor.

Equations

• ContinuousMonoidHom.compRight A f = { toFun := fun (g : ContinuousMonoidHom A B) => f.comp g, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }

def ContinuousAddMonoidHom.compRight (A : Type u_2) {E : Type u_6} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] {B : Type u_7} [AddCommGroup B] [TopologicalSpace B] [TopologicalAddGroup B] (f : ContinuousAddMonoidHom B E) : ContinuousAddMonoidHom (ContinuousAddMonoidHom A B) (ContinuousAddMonoidHom A E)

ContinuousAddMonoidHom f _ is a functor.

Equations

• ContinuousAddMonoidHom.compRight A f = { toFun := fun (g : ContinuousAddMonoidHom A B) => f.comp g, map_zero' := ⋯, map_add' := ⋯, continuous_toFun := ⋯ }

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) : LocallyCompactSpace (ContinuousMonoidHom X Y)

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) : LocallyCompactSpace (ContinuousAddMonoidHom X Y)

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 n → x * x ∈ V n → x ∈ V (n + 1)) (hVo : (nhds 1).HasBasis (fun (x : ℕ) => True) V) : LocallyCompactSpace (ContinuousMonoidHom X Y)

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 n → x + x ∈ V n → x ∈ V (n + 1)) (hVo : (nhds 0).HasBasis (fun (x : ℕ) => True) V) : LocallyCompactSpace (ContinuousAddMonoidHom X Y)

Continuous MulEquiv

This section defines the space of continuous isomorphisms between two topological groups.

Main definitions

structure ContinuousAddEquiv (G : Type u) [TopologicalSpace G] (H : Type v) [TopologicalSpace H] [Add G] [Add H] extends G ≃+ H, G ≃ₜ H : Type (max u v)

The structure of two-sided continuous isomorphisms between additive groups. Note that both the map and its inverse have to be continuous.

• toFun : G → H
• invFun : H → G
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• map_add' (x y : G) : self.toFun (x + y) = self.toFun x + self.toFun y
• continuous_toFun : Continuous self.toFun
• continuous_invFun : Continuous self.invFun

structure ContinuousMulEquiv (G : Type u) [TopologicalSpace G] (H : Type v) [TopologicalSpace H] [Mul G] [Mul H] extends G ≃* H, G ≃ₜ H : Type (max u v)

The structure of two-sided continuous isomorphisms between groups. Note that both the map and its inverse have to be continuous.

• toFun : G → H
• invFun : H → G
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• map_mul' (x y : G) : self.toFun (x * y) = self.toFun x * self.toFun y
• continuous_toFun : Continuous self.toFun
• continuous_invFun : Continuous self.invFun

def «term_≃ₜ*_» : Lean.TrailingParserDescr

The structure of two-sided continuous isomorphisms between groups. Note that both the map and its inverse have to be continuous.

Equations

• «term_≃ₜ*_» = Lean.ParserDescr.trailingNode `«term_≃ₜ*_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ₜ* ") (Lean.ParserDescr.cat `term 26))

def «term_≃ₜ+_» : Lean.TrailingParserDescr

The structure of two-sided continuous isomorphisms between additive groups. Note that both the map and its inverse have to be continuous.

Equations

• «term_≃ₜ+_» = Lean.ParserDescr.trailingNode `«term_≃ₜ+_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ₜ+ ") (Lean.ParserDescr.cat `term 26))

instance ContinuousMulEquiv.instEquivLike {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] : EquivLike (M ≃ₜ* N) M N

Equations

• ContinuousMulEquiv.instEquivLike = { coe := fun (f : M ≃ₜ* N) => f.toFun, inv := fun (f : M ≃ₜ* N) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

instance ContinuousAddEquiv.instEquivLike {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] : EquivLike (M ≃ₜ+ N) M N

Equations

• ContinuousAddEquiv.instEquivLike = { coe := fun (f : M ≃ₜ+ N) => f.toFun, inv := fun (f : M ≃ₜ+ N) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

instance ContinuousMulEquiv.instMulEquivClass {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] : MulEquivClass (M ≃ₜ* N) M N

instance ContinuousAddEquiv.instAddEquivClass {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] : AddEquivClass (M ≃ₜ+ N) M N

instance ContinuousMulEquiv.instHomeomorphClass {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] : HomeomorphClass (M ≃ₜ* N) M N

instance ContinuousAddEquiv.instHomeomorphClass {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] : HomeomorphClass (M ≃ₜ+ N) M N

theorem ContinuousAddEquiv.ext {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {f g : M ≃ₜ+ N} (h : ∀ (x : M), f x = g x) : f = g

Two continuous additive isomorphisms agree if they are defined by the same underlying function.

theorem ContinuousMulEquiv.ext {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] {f g : M ≃ₜ* N} (h : ∀ (x : M), f x = g x) : f = g

Two continuous multiplicative isomorphisms agree if they are defined by the same underlying function.

@[simp]

theorem ContinuousMulEquiv.coe_mk {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (f : M ≃* N) (hf1 : Continuous f.toFun) (hf2 : Continuous f.invFun) : ⇑{ toMulEquiv := f, continuous_toFun := hf1, continuous_invFun := hf2 } = ⇑f

@[simp]

theorem ContinuousAddEquiv.coe_mk {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (f : M ≃+ N) (hf1 : Continuous f.toFun) (hf2 : Continuous f.invFun) : ⇑{ toAddEquiv := f, continuous_toFun := hf1, continuous_invFun := hf2 } = ⇑f

theorem ContinuousMulEquiv.toEquiv_eq_coe {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (f : M ≃ₜ* N) : f.toEquiv = ↑f

theorem ContinuousAddEquiv.toEquiv_eq_coe {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (f : M ≃ₜ+ N) : f.toEquiv = ↑f

@[simp]

theorem ContinuousMulEquiv.toMulEquiv_eq_coe {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (f : M ≃ₜ* N) : f.toMulEquiv = ↑f

@[simp]

theorem ContinuousAddEquiv.toAddEquiv_eq_coe {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (f : M ≃ₜ+ N) : f.toAddEquiv = ↑f

theorem ContinuousMulEquiv.toHomeomorph_eq_coe {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (f : M ≃ₜ* N) : f.toHomeomorph = ↑f

theorem ContinuousAddEquiv.toHomeomorph_eq_coe {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (f : M ≃ₜ+ N) : f.toHomeomorph = ↑f

def ContinuousMulEquiv.mk' {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (f : M ≃ₜ N) (h : ∀ (x y : M), f (x * y) = f x * f y) : M ≃ₜ* N

Makes a continuous multiplicative isomorphism from a homeomorphism which preserves multiplication.

Equations

• ContinuousMulEquiv.mk' f h = { toEquiv := f.toEquiv, map_mul' := h, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def ContinuousAddEquiv.mk' {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (f : M ≃ₜ N) (h : ∀ (x y : M), f (x + y) = f x + f y) : M ≃ₜ+ N

Makes an continuous additive isomorphism from a homeomorphism which preserves addition.

Equations

• ContinuousAddEquiv.mk' f h = { toEquiv := f.toEquiv, map_add' := h, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousMulEquiv.coe_mk' {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (f : M ≃ₜ N) (h : ∀ (x y : M), f (x * y) = f x * f y) : ⇑(ContinuousMulEquiv.mk' f h) = ⇑f

theorem ContinuousMulEquiv.bijective {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) : Function.Bijective ⇑e

theorem ContinuousAddEquiv.bijective {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) : Function.Bijective ⇑e

theorem ContinuousMulEquiv.injective {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) : Function.Injective ⇑e

theorem ContinuousAddEquiv.injective {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) : Function.Injective ⇑e

theorem ContinuousMulEquiv.surjective {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) : Function.Surjective ⇑e

theorem ContinuousAddEquiv.surjective {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) : Function.Surjective ⇑e

theorem ContinuousMulEquiv.apply_eq_iff_eq {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) {x y : M} : e x = e y ↔ x = y

theorem ContinuousAddEquiv.apply_eq_iff_eq {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) {x y : M} : e x = e y ↔ x = y

def ContinuousMulEquiv.refl (M : Type u_1) [TopologicalSpace M] [Mul M] : M ≃ₜ* M

The identity map is a continuous multiplicative isomorphism.

Equations

• ContinuousMulEquiv.refl M = { toMulEquiv := MulEquiv.refl M, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def ContinuousAddEquiv.refl (M : Type u_1) [TopologicalSpace M] [Add M] : M ≃ₜ+ M

The identity map is a continuous additive isomorphism.

Equations

• ContinuousAddEquiv.refl M = { toAddEquiv := AddEquiv.refl M, continuous_toFun := ⋯, continuous_invFun := ⋯ }

instance ContinuousMulEquiv.instInhabited (M : Type u_1) [TopologicalSpace M] [Mul M] : Inhabited (M ≃ₜ* M)

Equations

• ContinuousMulEquiv.instInhabited M = { default := ContinuousMulEquiv.refl M }

instance ContinuousAddEquiv.instInhabited (M : Type u_1) [TopologicalSpace M] [Add M] : Inhabited (M ≃ₜ+ M)

Equations

• ContinuousAddEquiv.instInhabited M = { default := ContinuousAddEquiv.refl M }

@[simp]

theorem ContinuousMulEquiv.coe_refl (M : Type u_1) [TopologicalSpace M] [Mul M] : ⇑(ContinuousMulEquiv.refl M) = id

@[simp]

theorem ContinuousAddEquiv.coe_refl (M : Type u_1) [TopologicalSpace M] [Add M] : ⇑(ContinuousAddEquiv.refl M) = id

@[simp]

theorem ContinuousMulEquiv.refl_apply (M : Type u_1) [TopologicalSpace M] [Mul M] (m : M) : (ContinuousMulEquiv.refl M) m = m

@[simp]

theorem ContinuousAddEquiv.refl_apply (M : Type u_1) [TopologicalSpace M] [Add M] (m : M) : (ContinuousAddEquiv.refl M) m = m

def ContinuousMulEquiv.symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (cme : M ≃ₜ* N) : N ≃ₜ* M

The inverse of a ContinuousMulEquiv.

Equations

• cme.symm = { toMulEquiv := cme.symm, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def ContinuousAddEquiv.symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (cme : M ≃ₜ+ N) : N ≃ₜ+ M

The inverse of a ContinuousAddEquiv.

Equations

• cme.symm = { toAddEquiv := cme.symm, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem ContinuousMulEquiv.invFun_eq_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] {f : M ≃ₜ* N} : f.invFun = ⇑f.symm

theorem ContinuousAddEquiv.invFun_eq_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {f : M ≃ₜ+ N} : f.invFun = ⇑f.symm

@[simp]

theorem ContinuousMulEquiv.coe_toHomeomorph_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (f : M ≃ₜ* N) : (↑f).symm = ↑f.symm

@[simp]

theorem ContinuousAddEquiv.coe_toHomeomorph_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (f : M ≃ₜ+ N) : (↑f).symm = ↑f.symm

@[simp]

theorem ContinuousMulEquiv.equivLike_inv_eq_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (f : M ≃ₜ* N) : EquivLike.inv f = ⇑f.symm

@[simp]

theorem ContinuousAddEquiv.equivLike_neg_eq_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (f : M ≃ₜ+ N) : EquivLike.inv f = ⇑f.symm

@[simp]

theorem ContinuousMulEquiv.symm_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (f : M ≃ₜ* N) : f.symm.symm = f

@[simp]

theorem ContinuousAddEquiv.symm_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (f : M ≃ₜ+ N) : f.symm.symm = f

@[simp]

theorem ContinuousMulEquiv.apply_symm_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) (y : N) : e (e.symm y) = y

e.symm is a right inverse of e, written as e (e.symm y) = y.

@[simp]

theorem ContinuousAddEquiv.apply_symm_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) (y : N) : e (e.symm y) = y

e.symm is a right inverse of e, written as e (e.symm y) = y.

@[simp]

theorem ContinuousMulEquiv.symm_apply_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) (x : M) : e.symm (e x) = x

e.symm is a left inverse of e, written as e.symm (e y) = y.

@[simp]

theorem ContinuousAddEquiv.symm_apply_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) (x : M) : e.symm (e x) = x

e.symm is a left inverse of e, written as e.symm (e y) = y.

@[simp]

theorem ContinuousMulEquiv.symm_comp_self {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) : ⇑e.symm ∘ ⇑e = id

@[simp]

theorem ContinuousAddEquiv.symm_comp_self {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) : ⇑e.symm ∘ ⇑e = id

@[simp]

theorem ContinuousMulEquiv.self_comp_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) : ⇑e ∘ ⇑e.symm = id

@[simp]

theorem ContinuousAddEquiv.self_comp_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) : ⇑e ∘ ⇑e.symm = id

theorem ContinuousMulEquiv.apply_eq_iff_symm_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) {x : M} {y : N} : e x = y ↔ x = e.symm y

theorem ContinuousAddEquiv.apply_eq_iff_symm_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) {x : M} {y : N} : e x = y ↔ x = e.symm y

theorem ContinuousMulEquiv.symm_apply_eq {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) {x : N} {y : M} : e.symm x = y ↔ x = e y

theorem ContinuousAddEquiv.symm_apply_eq {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) {x : N} {y : M} : e.symm x = y ↔ x = e y

theorem ContinuousMulEquiv.eq_symm_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) {x : N} {y : M} : y = e.symm x ↔ e y = x

theorem ContinuousAddEquiv.eq_symm_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) {x : N} {y : M} : y = e.symm x ↔ e y = x

theorem ContinuousMulEquiv.eq_comp_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] {α : Type u_3} (e : M ≃ₜ* N) (f : N → α) (g : M → α) : f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g

theorem ContinuousAddEquiv.eq_comp_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {α : Type u_3} (e : M ≃ₜ+ N) (f : N → α) (g : M → α) : f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g

theorem ContinuousMulEquiv.comp_symm_eq {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] {α : Type u_3} (e : M ≃ₜ* N) (f : N → α) (g : M → α) : g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e

theorem ContinuousAddEquiv.comp_symm_eq {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {α : Type u_3} (e : M ≃ₜ+ N) (f : N → α) (g : M → α) : g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e

theorem ContinuousMulEquiv.eq_symm_comp {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] {α : Type u_3} (e : M ≃ₜ* N) (f : α → M) (g : α → N) : f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g

theorem ContinuousAddEquiv.eq_symm_comp {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {α : Type u_3} (e : M ≃ₜ+ N) (f : α → M) (g : α → N) : f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g

theorem ContinuousMulEquiv.symm_comp_eq {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] {α : Type u_3} (e : M ≃ₜ* N) (f : α → M) (g : α → N) : ⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f

theorem ContinuousAddEquiv.symm_comp_eq {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {α : Type u_3} (e : M ≃ₜ+ N) (f : α → M) (g : α → N) : ⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f

def ContinuousMulEquiv.trans {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] {L : Type u_3} [Mul L] [TopologicalSpace L] (cme1 : M ≃ₜ* N) (cme2 : N ≃ₜ* L) : M ≃ₜ* L

The composition of two ContinuousMulEquiv.

Equations

• cme1.trans cme2 = { toMulEquiv := cme1.trans cme2.toMulEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def ContinuousAddEquiv.trans {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {L : Type u_3} [Add L] [TopologicalSpace L] (cme1 : M ≃ₜ+ N) (cme2 : N ≃ₜ+ L) : M ≃ₜ+ L

The composition of two ContinuousAddEquiv.

Equations

• cme1.trans cme2 = { toAddEquiv := cme1.trans cme2.toAddEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousMulEquiv.coe_trans {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] {L : Type u_3} [Mul L] [TopologicalSpace L] (e₁ : M ≃ₜ* N) (e₂ : N ≃ₜ* L) : ⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁

@[simp]

theorem ContinuousAddEquiv.coe_trans {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {L : Type u_3} [Add L] [TopologicalSpace L] (e₁ : M ≃ₜ+ N) (e₂ : N ≃ₜ+ L) : ⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁

@[simp]

theorem ContinuousMulEquiv.trans_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] {L : Type u_3} [Mul L] [TopologicalSpace L] (e₁ : M ≃ₜ* N) (e₂ : N ≃ₜ* L) (m : M) : (e₁.trans e₂) m = e₂ (e₁ m)

@[simp]

theorem ContinuousAddEquiv.trans_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {L : Type u_3} [Add L] [TopologicalSpace L] (e₁ : M ≃ₜ+ N) (e₂ : N ≃ₜ+ L) (m : M) : (e₁.trans e₂) m = e₂ (e₁ m)

@[simp]

theorem ContinuousMulEquiv.symm_trans_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] {L : Type u_3} [Mul L] [TopologicalSpace L] (e₁ : M ≃ₜ* N) (e₂ : N ≃ₜ* L) (l : L) : (e₁.trans e₂).symm l = e₁.symm (e₂.symm l)

@[simp]

theorem ContinuousAddEquiv.symm_trans_apply {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {L : Type u_3} [Add L] [TopologicalSpace L] (e₁ : M ≃ₜ+ N) (e₂ : N ≃ₜ+ L) (l : L) : (e₁.trans e₂).symm l = e₁.symm (e₂.symm l)

@[simp]

theorem ContinuousMulEquiv.symm_trans_self {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) : e.symm.trans e = ContinuousMulEquiv.refl N

@[simp]

theorem ContinuousAddEquiv.symm_trans_self {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) : e.symm.trans e = ContinuousAddEquiv.refl N

@[simp]

theorem ContinuousMulEquiv.self_trans_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) : e.trans e.symm = ContinuousMulEquiv.refl M

@[simp]

theorem ContinuousAddEquiv.self_trans_symm {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) : e.trans e.symm = ContinuousAddEquiv.refl M

def ContinuousMulEquiv.ofUnique {M : Type u_3} {N : Type u_4} [Unique M] [Unique N] [Mul M] [Mul N] [TopologicalSpace M] [TopologicalSpace N] : M ≃ₜ* N

The MulEquiv between two monoids with a unique element.

Equations

• ContinuousMulEquiv.ofUnique = { toMulEquiv := MulEquiv.ofUnique, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def ContinuousAddEquiv.ofUnique {M : Type u_3} {N : Type u_4} [Unique M] [Unique N] [Add M] [Add N] [TopologicalSpace M] [TopologicalSpace N] : M ≃ₜ+ N

The AddEquiv between two AddMonoids with a unique element.

Equations

• ContinuousAddEquiv.ofUnique = { toAddEquiv := AddEquiv.ofUnique, continuous_toFun := ⋯, continuous_invFun := ⋯ }

instance ContinuousMulEquiv.instUnique {M : Type u_3} {N : Type u_4} [Unique M] [Unique N] [Mul M] [Mul N] [TopologicalSpace M] [TopologicalSpace N] : Unique (M ≃ₜ* N)

There is a unique monoid homomorphism between two monoids with a unique element.

Equations

• ContinuousMulEquiv.instUnique = { default := ContinuousMulEquiv.ofUnique, uniq := ⋯ }

instance ContinuousAddEquiv.instUnique {M : Type u_3} {N : Type u_4} [Unique M] [Unique N] [Add M] [Add N] [TopologicalSpace M] [TopologicalSpace N] : Unique (M ≃ₜ+ N)

There is a unique additive monoid homomorphism between two additive monoids with a unique element.

Equations

• ContinuousAddEquiv.instUnique = { default := ContinuousAddEquiv.ofUnique, uniq := ⋯ }