toContinuousAlgHom — Mathlib

English

The type of continuous algebra isomorphisms forms a class that respects addition, multiplication, and continuity of the map and its inverse.

Русский

Тип непрерывных алгебраических эквивалент образует класс, сохраняющий сложение, умножение и непрерывность отображения и его обратного.

LaTeX

$$ContinuousAlgEquivClass(ContinuousAlgEquiv R A B) R A B$$

Lean4

/-- The natural coercion from a continuous algebra isomorphism to a continuous
algebra morphism. -/
@[coe]
def toContinuousAlgHom (e : A ≃A[R] B) : A →A[R] B
    where
  __ := e.toAlgHom
  cont := e.continuous_toFun

Похожие утверждения