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.

Equations

• One or more equations did not get rendered due to their size.

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

The type of continuous monoid homomorphisms from A to B.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ContinuousMonoidHom.instFunLike = { coe := fun (f : 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 (A →ₜ+ B) A B

Equations

• ContinuousAddMonoidHom.instFunLike = { coe := fun (f : 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 (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 aContinuousMonoidHom. This is declared as the default coercion from F to (A →ₜ* B).

Equations

• ↑f = { toMonoidHom := ↑f, continuous_toFun := ⋯ }

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 aContinuousAddMonoidHom. This is declared as the default coercion from F to ContinuousAddMonoidHom A B.

Equations

• ↑f = { toAddMonoidHom := ↑f, continuous_toFun := ⋯ }

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.

Equations

• ContinuousMonoidHom.instCoeOutOfMonoidHomClassOfContinuousMapClass = { coe := ContinuousMonoidHom.toContinuousMonoidHom }

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.

Equations

• ContinuousAddMonoidHom.instCoeOutOfAddMonoidHomClassOfContinuousMapClass = { coe := 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

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.

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

Composition of two continuous homomorphisms.

Equations

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

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

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

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

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.

Equations

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

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.

Equations

• ContinuousAddMonoidHom.instZero A B = { zero := { 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) : 0 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) : 1 x✝ = 1

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

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

Equations

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

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

Equations

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

def ContinuousMonoidHom.id (A : Type u_2) [Monoid A] [TopologicalSpace A] : 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] : A →ₜ+ A

The identity continuous homomorphism.

Equations

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

@[simp]

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

@[simp]

theorem ContinuousMonoidHom.id_toFun (A : Type u_2) [Monoid 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.

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] : 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) : (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.

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] : 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 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

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

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.

Equations

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

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.

Equations

• ContinuousAddMonoidHom.inl A B = (ContinuousAddMonoidHom.id A).prod 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)

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

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.

Equations

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

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.

Equations

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

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

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

def ContinuousMonoidHom.diag (A : Type u_2) [Monoid A] [TopologicalSpace A] : 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] : A →ₜ+ A × A

The continuous homomorphism given by the diagonal embedding.

Equations

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

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

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] : 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) : (swap A B) i = (i.2, i.1)

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

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

The continuous homomorphism given by multiplication.

Equations

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

def ContinuousAddMonoidHom.add (E : Type u_6) [AddCommMonoid E] [TopologicalSpace E] [ContinuousAdd E] : 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) [CommMonoid E] [TopologicalSpace E] [ContinuousMul E] (a✝ : E × E) : (mul E) a✝ = a✝.1 * a✝.2

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

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

Equations

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

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

Equations

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

def ContinuousAddMonoidHom.neg (E : Type u_6) [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] : 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] [IsTopologicalGroup E] (a✝ : E) : (inv E) a✝ = a✝⁻¹

@[simp]

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• ContinuousMonoidHom.ofClass A B F f = ↑f

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.

Equations

• ContinuousAddMonoidHom.ofClass A B F f = ↑f

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

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

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

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

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.

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

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 := ⋯ }