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

def ContinuousMonoidHom.«term_→ₜ+_» : Lean.TrailingParserDescr

The type of continuous monoid homomorphisms from A to B.

def ContinuousMonoidHom.«term_→ₜ*_» : Lean.TrailingParserDescr

The type of continuous monoid homomorphisms from A to B.

@[implicit_reducible]

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

@[implicit_reducible]

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

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

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

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

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

@[simp]

theorem ContinuousMonoidHom.coe_toMonoidHom {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (f : A →ₜ* B) : f.toMonoidHom = ↑f

@[simp]

theorem ContinuousAddMonoidHom.coe_toAddMonoidHom {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (f : A →ₜ+ B) : f.toAddMonoidHom = ↑f

@[simp]

theorem ContinuousMonoidHom.coe_toContinuousMap {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (f : A →ₜ* B) : f.toContinuousMap = ↑f

@[simp]

theorem ContinuousAddMonoidHom.coe_toContinuousMap {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (f : A →ₜ+ B) : f.toContinuousMap = ↑f

def ContinuousMonoidHom.toContinuousMonoidHom {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] {F : Type u_7} [FunLike F A B] [MonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) : A →ₜ* B

Turn an element of a type F satisfying MonoidHomClass F A B and ContinuousMapClass F A B into a ContinuousMonoidHom. This is declared as the default coercion from F to (A →ₜ* B).

def ContinuousAddMonoidHom.toContinuousAddMonoidHom {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] {F : Type u_7} [FunLike F A B] [AddMonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) : A →ₜ+ B

Turn an element of a type F satisfying AddMonoidHomClass F A B and ContinuousMapClass F A B into a ContinuousAddMonoidHom. This is declared as the default coercion from F to ContinuousAddMonoidHom A B.

@[implicit_reducible]

instance ContinuousMonoidHom.instCoeOutOfMonoidHomClassOfContinuousMapClass {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] {F : Type u_7} [FunLike F A B] [MonoidHomClass F A B] [ContinuousMapClass F A B] : CoeOut F (A →ₜ* B)

Any type satisfying MonoidHomClass and ContinuousMapClass can be cast into ContinuousMonoidHom via ContinuousMonoidHom.toContinuousMonoidHom.

@[implicit_reducible]

instance ContinuousAddMonoidHom.instCoeOutOfAddMonoidHomClassOfContinuousMapClass {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] {F : Type u_7} [FunLike F A B] [AddMonoidHomClass F A B] [ContinuousMapClass F A B] : CoeOut F (A →ₜ+ B)

Any type satisfying AddMonoidHomClass and ContinuousMapClass can be cast into ContinuousAddMonoidHom via ContinuousAddMonoidHom.toContinuousAddMonoidHom.

@[simp]

theorem ContinuousMonoidHom.coe_coe {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] {F : Type u_7} [FunLike F A B] [MonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) : ⇑↑f = ⇑f

@[simp]

theorem ContinuousAddMonoidHom.coe_coe {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] {F : Type u_7} [FunLike F A B] [AddMonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) : ⇑↑f = ⇑f

@[simp]

theorem ContinuousMonoidHom.toMonoidHom_toContinuousMonoidHom {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] {F : Type u_7} [FunLike F A B] [MonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) : ↑↑f = ↑f

@[simp]

theorem ContinuousAddMonoidHom.toAddMonoidHom_toContinuousAddMonoidHom {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] {F : Type u_7} [FunLike F A B] [AddMonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) : ↑↑f = ↑f

@[simp]

theorem ContinuousMonoidHom.toContinuousMap_toContinuousMonoidHom {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] {F : Type u_7} [FunLike F A B] [MonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) : ↑↑f = ↑f

@[simp]

theorem ContinuousAddMonoidHom.toContinuousMap_toContinuousAddMonoidHom {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] {F : Type u_7} [FunLike F A B] [AddMonoidHomClass F A B] [ContinuousMapClass F A B] (f : F) : ↑↑f = ↑f

theorem ContinuousMonoidHom.ext {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] {f g : A →ₜ* B} (h : ∀ (x : A), f x = g x) : f = g

theorem ContinuousAddMonoidHom.ext {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] {f g : A →ₜ+ B} (h : ∀ (x : A), f x = g x) : f = g

theorem ContinuousAddMonoidHom.ext_iff {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] {f g : A →ₜ+ B} : f = g ↔ ∀ (x : A), f x = g x

theorem ContinuousMonoidHom.ext_iff {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] {f g : A →ₜ* B} : f = g ↔ ∀ (x : A), f x = g x

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

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

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

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

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 : B →ₜ* C) (f : A →ₜ* B) : A →ₜ* C

Composition of two continuous homomorphisms.

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 : B →ₜ+ C) (f : A →ₜ+ B) : A →ₜ+ C

Composition of two continuous homomorphisms.

@[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 : B →ₜ* C) (f : A →ₜ* B) (a✝ : A) : (g.comp f) a✝ = g (f a✝)

@[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 : B →ₜ+ C) (f : A →ₜ+ B) (a✝ : A) : (g.comp f) a✝ = g (f a✝)

@[simp]

theorem ContinuousMonoidHom.coe_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 : B →ₜ* C) (f : A →ₜ* B) : ⇑(g.comp f) = ⇑g ∘ ⇑f

@[simp]

theorem ContinuousAddMonoidHom.coe_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 : B →ₜ+ C) (f : A →ₜ+ B) : ⇑(g.comp f) = ⇑g ∘ ⇑f

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 : A →ₜ* B) (g : A →ₜ* C) : A →ₜ* B × C

Product of two continuous homomorphisms on the same space.

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 : A →ₜ+ B) (g : A →ₜ+ C) : A →ₜ+ B × C

Product of two continuous homomorphisms on the same space.

@[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 : A →ₜ+ B) (g : A →ₜ+ C) (i : A) : (f.prod g) i = (f i, g 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 : A →ₜ* B) (g : A →ₜ* C) (i : A) : (f.prod g) i = (f i, g 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 : A →ₜ* C) (g : B →ₜ* D) : A × B →ₜ* C × D

Product of two continuous homomorphisms on different spaces.

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 : A →ₜ+ C) (g : B →ₜ+ D) : A × B →ₜ+ C × D

Product of two continuous homomorphisms on different spaces.

@[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 : A →ₜ* C) (g : B →ₜ* D) (i : A × B) : (f.prodMap g) i = (f i.1, g i.2)

@[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 : A →ₜ+ C) (g : B →ₜ+ D) (i : A × B) : (f.prodMap g) i = (f i.1, g i.2)

@[implicit_reducible]

instance ContinuousMonoidHom.instOne (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : One (A →ₜ* B)

The trivial continuous homomorphism.

@[implicit_reducible]

instance ContinuousAddMonoidHom.instZero (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : Zero (A →ₜ+ B)

The trivial continuous homomorphism.

@[simp]

theorem ContinuousMonoidHom.one_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (x✝ : A) : 1 x✝ = 1

@[simp]

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

@[simp]

theorem ContinuousMonoidHom.coe_one (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : ⇑1 = 1

@[simp]

theorem ContinuousAddMonoidHom.coe_zero (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : ⇑0 = 0

@[implicit_reducible]

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

@[implicit_reducible]

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

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

The identity continuous homomorphism.

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

The identity continuous homomorphism.

@[simp]

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

@[simp]

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

@[simp]

theorem ContinuousMonoidHom.coe_id (A : Type u_2) [Monoid A] [TopologicalSpace A] : ⇑(id A) = _root_.id

@[simp]

theorem ContinuousAddMonoidHom.coe_id (A : Type u_2) [AddMonoid A] [TopologicalSpace A] : ⇑(id A) = _root_.id

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

The continuous homomorphism given by projection onto the first factor.

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

The continuous homomorphism given by projection onto the first factor.

@[simp]

theorem ContinuousMonoidHom.fst_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (self : A × B) : (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) : (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] : A × B →ₜ* B

The continuous homomorphism given by projection onto the second factor.

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

The continuous homomorphism given by projection onto the second factor.

@[simp]

theorem ContinuousMonoidHom.snd_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (self : A × B) : (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) : (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] : A →ₜ* A × B

The continuous homomorphism given by inclusion of the first factor.

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

The continuous homomorphism given by inclusion of the first factor.

@[simp]

theorem ContinuousAddMonoidHom.inl_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (i : A) : (inl A B) i = (i, 0)

@[simp]

theorem ContinuousMonoidHom.inl_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (i : A) : (inl A B) i = (i, 1)

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

The continuous homomorphism given by inclusion of the second factor.

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

The continuous homomorphism given by inclusion of the second factor.

@[simp]

theorem ContinuousAddMonoidHom.inr_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (i : B) : (inr A B) i = (0, i)

@[simp]

theorem ContinuousMonoidHom.inr_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (i : B) : (inr A B) i = (1, i)

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

The continuous homomorphism given by the diagonal embedding.

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

The continuous homomorphism given by the diagonal embedding.

@[simp]

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

@[simp]

theorem ContinuousMonoidHom.diag_toFun (A : Type u_2) [Monoid A] [TopologicalSpace A] (i : A) : (diag A) i = (i, i)

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

The continuous homomorphism given by swapping components.

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

The continuous homomorphism given by swapping components.

@[simp]

theorem ContinuousMonoidHom.swap_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (i : A × B) : (swap A B) i = (i.2, i.1)

@[simp]

theorem ContinuousAddMonoidHom.swap_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (i : A × B) : (swap A B) i = (i.2, i.1)

def ContinuousMonoidHom.mul (E : Type u_6) [CommMonoid E] [TopologicalSpace E] [ContinuousMul E] : E × E →ₜ* E

The continuous homomorphism given by multiplication.

def ContinuousAddMonoidHom.add (E : Type u_6) [AddCommMonoid E] [TopologicalSpace E] [ContinuousAdd E] : E × E →ₜ+ E

The continuous homomorphism given by addition.

@[simp]

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

@[simp]

theorem ContinuousMonoidHom.mul_toFun (E : Type u_6) [CommMonoid E] [TopologicalSpace E] [ContinuousMul E] (a✝ : E × E) : (mul E) a✝ = a✝.1 * a✝.2

@[implicit_reducible]

instance ContinuousMonoidHom.instCommMonoid {A : Type u_2} {E : Type u_6} [Monoid A] [TopologicalSpace A] [CommMonoid E] [TopologicalSpace E] [ContinuousMul E] : CommMonoid (A →ₜ* E)

@[implicit_reducible]

instance ContinuousAddMonoidHom.instAddCommMonoid {A : Type u_2} {E : Type u_6} [AddMonoid A] [TopologicalSpace A] [AddCommMonoid E] [TopologicalSpace E] [ContinuousAdd E] : AddCommMonoid (A →ₜ+ E)

@[simp]

theorem ContinuousMonoidHom.mul_apply {A : Type u_2} {E : Type u_6} [Monoid A] [TopologicalSpace A] [CommMonoid E] [TopologicalSpace E] [ContinuousMul E] (f g : A →ₜ* E) (a : A) : (f * g) a = f a * g a

@[simp]

theorem ContinuousAddMonoidHom.add_apply {A : Type u_2} {E : Type u_6} [AddMonoid A] [TopologicalSpace A] [AddCommMonoid E] [TopologicalSpace E] [ContinuousAdd E] (f g : A →ₜ+ E) (a : A) : (f + g) a = f a + g a

@[simp]

theorem ContinuousMonoidHom.pow_apply {A : Type u_2} {E : Type u_6} [Monoid A] [TopologicalSpace A] [CommMonoid E] [TopologicalSpace E] [ContinuousMul E] (f : A →ₜ* E) (n : ℕ) (a : A) : (f ^ n) a = f a ^ n

@[simp]

theorem ContinuousAddMonoidHom.nsmul_apply {A : Type u_2} {E : Type u_6} [AddMonoid A] [TopologicalSpace A] [AddCommMonoid E] [TopologicalSpace E] [ContinuousAdd E] (f : A →ₜ+ E) (n : ℕ) (a : A) : (n • f) a = n • f a

def ContinuousMonoidHom.coprod {A : Type u_2} {B : Type u_3} {E : Type u_6} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [CommMonoid E] [TopologicalSpace E] [ContinuousMul E] (f : A →ₜ* E) (g : B →ₜ* E) : A × B →ₜ* E

Coproduct of two continuous homomorphisms to the same space.

def ContinuousAddMonoidHom.coprod {A : Type u_2} {B : Type u_3} {E : Type u_6} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] [AddCommMonoid E] [TopologicalSpace E] [ContinuousAdd E] (f : A →ₜ+ E) (g : B →ₜ+ E) : A × B →ₜ+ E

Coproduct of two continuous homomorphisms to the same space.

@[simp]

theorem ContinuousMonoidHom.coprod_toFun {A : Type u_2} {B : Type u_3} {E : Type u_6} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [CommMonoid E] [TopologicalSpace E] [ContinuousMul E] (f : A →ₜ* E) (g : B →ₜ* E) (a✝ : A × B) : (f.coprod g) a✝ = f a✝.1 * g a✝.2

@[simp]

theorem ContinuousAddMonoidHom.coprod_toFun {A : Type u_2} {B : Type u_3} {E : Type u_6} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] [AddCommMonoid E] [TopologicalSpace E] [ContinuousAdd E] (f : A →ₜ+ E) (g : B →ₜ+ E) (a✝ : A × B) : (f.coprod g) a✝ = f a✝.1 + g a✝.2

def ContinuousMonoidHom.inv (E : Type u_6) [CommGroup E] [TopologicalSpace E] [IsTopologicalGroup E] : E →ₜ* E

The continuous homomorphism given by inversion.

def ContinuousAddMonoidHom.neg (E : Type u_6) [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] : E →ₜ+ E

The continuous homomorphism given by negation.

@[simp]

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

@[simp]

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

@[implicit_reducible]

instance ContinuousMonoidHom.instCommGroup (A : Type u_2) (E : Type u_6) [Monoid A] [TopologicalSpace A] [CommGroup E] [TopologicalSpace E] [IsTopologicalGroup E] : CommGroup (A →ₜ* E)

@[implicit_reducible]

instance ContinuousAddMonoidHom.instAddCommGroup (A : Type u_2) (E : Type u_6) [AddMonoid A] [TopologicalSpace A] [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] : AddCommGroup (A →ₜ+ E)

def ContinuousMonoidHom.ofClass (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (F : Type u_7) [FunLike F A B] [ContinuousMapClass F A B] [MonoidHomClass F A B] (f : F) : A →ₜ* B

For f : F where F is a class of continuous monoid hom, this yields an element ContinuousMonoidHom A B.

def ContinuousAddMonoidHom.ofClass (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (F : Type u_7) [FunLike F A B] [ContinuousMapClass F A B] [AddMonoidHomClass F A B] (f : F) : A →ₜ+ B

For f : F where F is a class of continuous additive monoid hom, this yields an element ContinuousAddMonoidHom A B.

Continuous MulEquiv

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

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.

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.

@[implicit_reducible]

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

@[implicit_reducible]

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

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 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.

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 ContinuousAddEquiv.ext_iff {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] {f g : M ≃ₜ+ N} : f = g ↔ ∀ (x : M), f x = g x

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

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

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 a continuous additive isomorphism from a homeomorphism which preserves addition.

@[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) : ⇑(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.

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

The identity map is a continuous additive isomorphism.

@[implicit_reducible]

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

@[implicit_reducible]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem ContinuousAddEquiv.refl_apply (M : Type u_1) [TopologicalSpace M] [Add M] (m : M) : (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.

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.

def ContinuousMulEquiv.Simps.symm_apply (G : Type u) [TopologicalSpace G] (H : Type v) [TopologicalSpace H] [Mul G] [Mul H] (e : G ≃ₜ* H) : H → G

See Note [custom simps projection]

def ContinuousAddEquiv.Simps.symm_apply (G : Type u) [TopologicalSpace G] (H : Type v) [TopologicalSpace H] [Add G] [Add H] (e : G ≃ₜ+ H) : H → G

See Note [custom simps projection]

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

theorem ContinuousMulEquiv.symm_bijective {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] : Function.Bijective symm

theorem ContinuousAddEquiv.symm_bijective {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] : Function.Bijective symm

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

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.

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

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.

@[implicit_reducible]

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.

@[implicit_reducible]

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.

def MulEquiv.toContinuousMulEquiv {G : Type u} [TopologicalSpace G] {H : Type v} [TopologicalSpace H] [Mul G] [Mul H] (e : G ≃* H) (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) : G ≃ₜ* H

A MulEquiv that respects open sets is a ContinuousMulEquiv.

def AddEquiv.toContinuousAddEquiv {G : Type u} [TopologicalSpace G] {H : Type v} [TopologicalSpace H] [Add G] [Add H] (e : G ≃+ H) (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) : G ≃ₜ+ H

An AddEquiv that respects open sets is a ContinuousAddEquiv.

@[simp]

theorem AddEquiv.toContinuousAddEquiv_symm_apply {G : Type u} [TopologicalSpace G] {H : Type v} [TopologicalSpace H] [Add G] [Add H] (e : G ≃+ H) (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) (a : H) : (e.toContinuousAddEquiv he).symm a = e.symm a

@[simp]

theorem AddEquiv.toContinuousAddEquiv_apply {G : Type u} [TopologicalSpace G] {H : Type v} [TopologicalSpace H] [Add G] [Add H] (e : G ≃+ H) (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) (a : G) : (e.toContinuousAddEquiv he) a = e a

@[simp]

theorem MulEquiv.toContinuousMulEquiv_symm_apply {G : Type u} [TopologicalSpace G] {H : Type v} [TopologicalSpace H] [Mul G] [Mul H] (e : G ≃* H) (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) (a : H) : (e.toContinuousMulEquiv he).symm a = e.symm a

@[simp]

theorem MulEquiv.toContinuousMulEquiv_apply {G : Type u} [TopologicalSpace G] {H : Type v} [TopologicalSpace H] [Mul G] [Mul H] (e : G ≃* H) (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) (a : G) : (e.toContinuousMulEquiv he) a = e a

@[simp]

theorem MulEquiv.toMulEquiv_toContinuousMulEquiv {G : Type u} [TopologicalSpace G] {H : Type v} [TopologicalSpace H] [Mul G] [Mul H] {e : G ≃* H} (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) : ↑(e.toContinuousMulEquiv he) = e

theorem AddEquiv.toAddEquiv_toContinuousAddEquiv {G : Type u} [TopologicalSpace G] {H : Type v} [TopologicalSpace H] [Add G] [Add H] {e : G ≃+ H} (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) : ↑(e.toContinuousAddEquiv he) = e

@[simp]

theorem MulEquiv.toHomeomorph_toContinuousMulEquiv {G : Type u} [TopologicalSpace G] {H : Type v} [TopologicalSpace H] [Mul G] [Mul H] {e : G ≃* H} (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) : ↑(e.toContinuousMulEquiv he) = e.toHomeomorph he

theorem AddEquiv.toHomeomorph_toContinuousAddEquiv {G : Type u} [TopologicalSpace G] {H : Type v} [TopologicalSpace H] [Add G] [Add H] {e : G ≃+ H} (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) : ↑(e.toContinuousAddEquiv he) = e.toHomeomorph he

theorem MulEquiv.symm_toContinuousMulEquiv {G : Type u} [TopologicalSpace G] {H : Type v} [TopologicalSpace H] [Mul G] [Mul H] {e : G ≃* H} (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) : (e.toContinuousMulEquiv he).symm = e.symm.toContinuousMulEquiv ⋯

theorem AddEquiv.symm_toContinuousAddEquiv {G : Type u} [TopologicalSpace G] {H : Type v} [TopologicalSpace H] [Add G] [Add H] {e : G ≃+ H} (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) : (e.toContinuousAddEquiv he).symm = e.symm.toContinuousAddEquiv ⋯