Topological (sub)algebras #

This file contains an API for ContinuousAlgEquiv.

structure ContinuousAlgEquiv (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] extends A ≃ₐ[R] B :

Type (max u_2 u_3)

toFun : A → B
invFun : B → A
left_inv : Function.LeftInverse self.invFun self.toFun
right_inv : Function.RightInverse self.invFun self.toFun
map_mul' : ∀ (x y : A), self.toFun (x * y) = self.toFun x * self.toFun y
map_add' : ∀ (x y : A), self.toFun (x + y) = self.toFun x + self.toFun y
commutes' : ∀ (r : R), self.toFun ((algebraMap R A) r) = (algebraMap R B) r
continuous_toFun : Continuous self.toFun
continuous_invFun : Continuous self.invFun

Instances For

source

def «term_≃A[_]_» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

class ContinuousAlgEquivClass (F : Type u_1) (R : outParam (Type u_2)) (A : outParam (Type u_3)) (B : outParam (Type u_4)) [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] [EquivLike F A B] extends AlgEquivClass F R A B :

Prop

map_mul : ∀ (f : F) (a b : A), f (a * b) = f a * f b
map_add : ∀ (f : F) (a b : A), f (a + b) = f a + f b
commutes : ∀ (f : F) (r : R), f ((algebraMap R A) r) = (algebraMap R B) r
map_continuous : ∀ (f : F), Continuous ⇑f
inv_continuous : ∀ (f : F), Continuous (EquivLike.inv f)

Instances

source

def ContinuousAlgEquiv.toContinuousAlgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) :

A →A[R] B

Equations

↑e = { toAlgHom := ↑e.toAlgEquiv, cont := ⋯ }

Instances For

source

instance ContinuousAlgEquiv.coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] :

Coe (A ≃A[R]B) (A →A[R] B)

Equations

ContinuousAlgEquiv.coe = { coe := ContinuousAlgEquiv.toContinuousAlgHom }

source

instance ContinuousAlgEquiv.equivLike {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] :

EquivLike (A ≃A[R]B) A B

Equations

ContinuousAlgEquiv.equivLike = { coe := fun (f : A ≃A[R]B) => f.toFun, inv := fun (f : A ≃A[R]B) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

source

theorem ContinuousAlgEquiv.continuousAlgEquivClass {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] :

ContinuousAlgEquivClass (A ≃A[R]B) R A B

source

theorem ContinuousAlgEquiv.coe_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) (a : A) :

↑e a = e a

source

@[simp]

theorem ContinuousAlgEquiv.coe_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) :

⇑↑e = ⇑e

source

theorem ContinuousAlgEquiv.toAlgEquiv_injective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] :

Function.Injective ContinuousAlgEquiv.toAlgEquiv

source

theorem ContinuousAlgEquiv.ext {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {f g : A ≃A[R]B} (h : ⇑f = ⇑g) :

f = g

source

theorem ContinuousAlgEquiv.coe_injective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] :

Function.Injective ContinuousAlgEquiv.toContinuousAlgHom

source

@[simp]

theorem ContinuousAlgEquiv.coe_inj {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {f g : A ≃A[R]B} :

↑f = ↑g ↔ f = g

source

def ContinuousAlgEquiv.toHomeomorph {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) :

A ≃ₜ B

Equations

e.toHomeomorph = { toEquiv := e.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source

@[simp]

theorem ContinuousAlgEquiv.coe_toHomeomorph {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) :

⇑e.toHomeomorph = ⇑e

source

theorem ContinuousAlgEquiv.isOpenMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) :

IsOpenMap ⇑e

source

theorem ContinuousAlgEquiv.image_closure {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) (S : Set A) :

⇑e '' closure S = closure (⇑e '' S)

source

theorem ContinuousAlgEquiv.preimage_closure {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) (S : Set B) :

⇑e ⁻¹' closure S = closure (⇑e ⁻¹' S)

source

@[simp]

theorem ContinuousAlgEquiv.isClosed_image {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) {S : Set A} :

IsClosed (⇑e '' S) ↔ IsClosed S

source

theorem ContinuousAlgEquiv.map_nhds_eq {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) (a : A) :

Filter.map (⇑e) (nhds a) = nhds (e a)

source

theorem ContinuousAlgEquiv.map_zero {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) :

e 0 = 0

source

theorem ContinuousAlgEquiv.map_add {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) (a₁ a₂ : A) :

e (a₁ + a₂) = e a₁ + e a₂

source

theorem ContinuousAlgEquiv.map_smul {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) (r : R) (a : A) :

e (r • a) = r • e a

source

theorem ContinuousAlgEquiv.map_eq_zero_iff {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) {a : A} :

e a = 0 ↔ a = 0

source

theorem ContinuousAlgEquiv.continuous {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) :

Continuous ⇑e

source

theorem ContinuousAlgEquiv.continuousOn {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) {S : Set A} :

ContinuousOn (⇑e) S

source

theorem ContinuousAlgEquiv.continuousAt {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) {a : A} :

ContinuousAt (⇑e) a

source

theorem ContinuousAlgEquiv.continuousWithinAt {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) {S : Set A} {a : A} :

ContinuousWithinAt (⇑e) S a

source

theorem ContinuousAlgEquiv.comp_continuous_iff {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {α : Type u_5} [TopologicalSpace α] (e : A ≃A[R]B) {f : α → A} :

Continuous (⇑e ∘ f) ↔ Continuous f

source

def ContinuousAlgEquiv.refl (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [TopologicalSpace A] [Algebra R A] :

A ≃A[R]A

Equations

ContinuousAlgEquiv.refl R A = { toAlgEquiv := AlgEquiv.refl, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source

@[simp]

theorem ContinuousAlgEquiv.refl_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [TopologicalSpace A] [Algebra R A] (a : A) :

(ContinuousAlgEquiv.refl R A) a = a

source

@[simp]

theorem ContinuousAlgEquiv.coe_refl (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [TopologicalSpace A] [Algebra R A] :

↑(ContinuousAlgEquiv.refl R A) = ContinuousAlgHom.id R A

source

@[simp]

theorem ContinuousAlgEquiv.coe_refl' (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [TopologicalSpace A] [Algebra R A] :

⇑(ContinuousAlgEquiv.refl R A) = id

source

def ContinuousAlgEquiv.symm {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) :

B ≃A[R]A

Equations

e.symm = { toAlgEquiv := e.symm, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source

@[simp]

theorem ContinuousAlgEquiv.apply_symm_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) (b : B) :

e (e.symm b) = b

source

@[simp]

theorem ContinuousAlgEquiv.symm_apply_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) (a : A) :

e.symm (e a) = a

source

@[simp]

theorem ContinuousAlgEquiv.symm_image_image {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) (S : Set A) :

⇑e.symm '' (⇑e '' S) = S

source

@[simp]

theorem ContinuousAlgEquiv.image_symm_image {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) (S : Set B) :

⇑e '' (⇑e.symm '' S) = S

source

@[simp]

theorem ContinuousAlgEquiv.symm_toAlgEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) :

e.symm.toAlgEquiv = e.symm

source

@[simp]

theorem ContinuousAlgEquiv.symm_toHomeomorph {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) :

e.symm.toHomeomorph = e.toHomeomorph.symm

source

theorem ContinuousAlgEquiv.symm_map_nhds_eq {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) (a : A) :

Filter.map (⇑e.symm) (nhds (e a)) = nhds a

source

def ContinuousAlgEquiv.trans {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Semiring C] [TopologicalSpace C] [Algebra R A] [Algebra R B] [Algebra R C] (e₁ : A ≃A[R]B) (e₂ : B ≃A[R]C) :

A ≃A[R]C

Equations

e₁.trans e₂ = { toAlgEquiv := e₁.trans e₂.toAlgEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source

@[simp]

theorem ContinuousAlgEquiv.trans_toAlgEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Semiring C] [TopologicalSpace C] [Algebra R A] [Algebra R B] [Algebra R C] (e₁ : A ≃A[R]B) (e₂ : B ≃A[R]C) :

(e₁.trans e₂).toAlgEquiv = e₁.trans e₂.toAlgEquiv

source

@[simp]

theorem ContinuousAlgEquiv.trans_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Semiring C] [TopologicalSpace C] [Algebra R A] [Algebra R B] [Algebra R C] (e₁ : A ≃A[R]B) (e₂ : B ≃A[R]C) (a : A) :

(e₁.trans e₂) a = e₂ (e₁ a)

source

@[simp]

theorem ContinuousAlgEquiv.symm_trans_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Semiring C] [TopologicalSpace C] [Algebra R A] [Algebra R B] [Algebra R C] (e₁ : B ≃A[R]A) (e₂ : C ≃A[R]B) (a : A) :

(e₂.trans e₁).symm a = e₂.symm (e₁.symm a)

source

@[simp]

theorem ContinuousAlgEquiv.comp_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Semiring C] [TopologicalSpace C] [Algebra R A] [Algebra R B] [Algebra R C] (e₁ : A ≃A[R]B) (e₂ : B ≃A[R]C) :

(↑e₂.toAlgEquiv).comp ↑e₁.toAlgEquiv = ↑(e₁.trans e₂)

source

@[simp]

theorem ContinuousAlgEquiv.coe_comp_coe_symm {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) :

(↑e).comp ↑e.symm = ContinuousAlgHom.id R B

source

@[simp]

theorem ContinuousAlgEquiv.coe_symm_comp_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) :

(↑e.symm).comp ↑e = ContinuousAlgHom.id R A

source

@[simp]

theorem ContinuousAlgEquiv.symm_comp_self {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) :

e.symm.toFun ∘ e.toFun = id

source

@[simp]

theorem ContinuousAlgEquiv.self_comp_symm {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) :

e.toFun ∘ e.symm.toFun = id

source

@[simp]

theorem ContinuousAlgEquiv.symm_symm {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) :

e.symm.symm = e

source

@[simp]

theorem ContinuousAlgEquiv.refl_symm {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Algebra R A] :

(ContinuousAlgEquiv.refl R A).symm = ContinuousAlgEquiv.refl R A

source

theorem ContinuousAlgEquiv.symm_symm_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) (a : A) :

e.symm.symm a = e a

source

theorem ContinuousAlgEquiv.symm_apply_eq {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) {a : A} {b : B} :

e.symm b = a ↔ b = e a

source

theorem ContinuousAlgEquiv.eq_symm_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) {a : A} {b : B} :

a = e.symm b ↔ e a = b

source

theorem ContinuousAlgEquiv.image_eq_preimage {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) (S : Set A) :

⇑e '' S = ⇑e.symm ⁻¹' S

source

theorem ContinuousAlgEquiv.image_symm_eq_preimage {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) (S : Set B) :

⇑e.symm '' S = ⇑e ⁻¹' S

source

@[simp]

theorem ContinuousAlgEquiv.symm_preimage_preimage {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) (S : Set B) :

⇑e.symm ⁻¹' (⇑e ⁻¹' S) = S

source

@[simp]

theorem ContinuousAlgEquiv.preimage_symm_preimage {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R]B) (S : Set A) :

⇑e ⁻¹' (⇑e.symm ⁻¹' S) = S

source

theorem ContinuousAlgEquiv.isUniformEmbedding {R : Type u_1} [CommSemiring R] {E₁ : Type u_5} {E₂ : Type u_6} [UniformSpace E₁] [UniformSpace E₂] [Ring E₁] [UniformAddGroup E₁] [Algebra R E₁] [Ring E₂] [UniformAddGroup E₂] [Algebra R E₂] (e : E₁ ≃A[R]E₂) :

IsUniformEmbedding ⇑e

source

theorem AlgEquiv.isUniformEmbedding {R : Type u_1} [CommSemiring R] {E₁ : Type u_5} {E₂ : Type u_6} [UniformSpace E₁] [UniformSpace E₂] [Ring E₁] [UniformAddGroup E₁] [Algebra R E₁] [Ring E₂] [UniformAddGroup E₂] [Algebra R E₂] (e : E₁ ≃ₐ[R] E₂) (h₁ : Continuous ⇑e) (h₂ : Continuous ⇑e.symm) :

IsUniformEmbedding ⇑e

Documentation

FLT.ForMathlib.Topology.Algebra.Algebra

Topological (sub)algebras #