symm_toHomeomorph

Mathlib.Topology.Algebra.Algebra.Equiv

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

English

The symmetric of a continuous algebraic equivalence equals the symmetric homeomorphism of the same.

Русский

Обратное к непрерывному алгебраическому эквиваленту равно обратному гомоморфизму.

LaTeX

$$$ e^{-1}.toHomeomorph = e.toHomeomorph^{-1} $$$

Lean4

@[simp]
theorem symm_toHomeomorph (e : A ≃A[R] B) : e.symm.toHomeomorph = e.toHomeomorph.symm :=
  rfl

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

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

Разделы

Аффилиация

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