symm

Mathlib.Topology.Algebra.Algebra.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousAlgEquiv.symm

← MathLib Explorer

English

Applying the inverse of e after e to an element a returns a.

Русский

Обратное применение e после применения e к элементу a возвращает a.

LaTeX

$$$ e^{-1} (e(a)) = a $$$

Lean4

/-- The inverse of a continuous algebra equivalence. -/
@[symm]
def symm (e : A ≃A[R] B) : B ≃A[R] A where
  __ := e.toAlgEquiv.symm
  continuous_toFun := e.continuous_invFun
  continuous_invFun := e.continuous_toFun

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru