Isomorphisms of topological algebras #

This file contains an API for ContinuousAlgEquiv R A B, the type of continuous R-algebra isomorphisms with continuous inverses. Here R is a commutative (semi)ring, and A and B are R-algebras with topologies.

Main definitions #

Let R be a commutative semiring and let A and B be R-algebras which are also topological spaces.

ContinuousAlgEquiv R A B: the type of continuous R-algebra isomorphisms from A to B with continuous inverses.

Notations #

A ≃A[R] B : notation for ContinuousAlgEquiv R A B.

Tags #

continuous, isomorphism, algebra

source

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, A ≃ₜ B :

Type (max u_2 u_3)

ContinuousAlgEquiv R A B, with notation A ≃A[R] B, is the type of bijections between the topological R-algebras A and B which are both homeomorphisms and R-algebra isomorphisms.

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

ContinuousAlgEquiv R A B, with notation A ≃A[R] B, is the type of bijections between the topological R-algebras A and B which are both homeomorphisms and R-algebra isomorphisms.

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, HomeomorphClass F A B :

Prop

ContinuousAlgEquivClass F R A B states that F is a type of topological algebra structure-preserving equivalences. You should extend this class when you extend ContinuousAlgEquiv.

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

The natural coercion from a continuous algebra isomorphism to a continuous algebra morphism.

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

instance 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 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.ext_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] {f g : A ≃A[R] B} :

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

@[simp]

theorem ContinuousAlgEquiv.coe_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.toAlgEquiv = ⇑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_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

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) {g : B → β} :

Continuous (g ∘ ⇑e) ↔ Continuous g

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

The identity isomorphism as a continuous R-algebra equivalence.

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

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

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

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

The inverse of a continuous algebra equivalence.

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

The composition of two continuous algebra equivalences.

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

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 ∘ ⇑e = 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 ∘ ⇑e.symm = 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

theorem ContinuousAlgEquiv.symm_bijective {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.Bijective symm

source

@[simp]

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

(refl R A).symm = 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₁] [IsUniformAddGroup E₁] [Algebra R E₁] [Ring E₂] [IsUniformAddGroup 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₁] [IsUniformAddGroup E₁] [Algebra R E₁] [Ring E₂] [IsUniformAddGroup E₂] [Algebra R E₂] (e : E₁ ≃ₐ[R] E₂) (h₁ : Continuous ⇑e) (h₂ : Continuous ⇑e.symm) :

IsUniformEmbedding ⇑e

Documentation

Mathlib.Topology.Algebra.Algebra.Equiv

Isomorphisms of topological algebras #

Main definitions #

Notations #

Tags #