symm_trans_self

Mathlib.Topology.Homeomorph.Defs

URI: https://scilib.ai/kg/mathlib#Homeomorph.symm_trans_self

English

Let h be a homeomorphism X → Y. Then h^{-1} ∘ h = id_Y.

Русский

Пусть h—гомеоморфизм X → Y. Тогда h^{-1} ∘ h = id_Y.

LaTeX

$$$h^{-1} \\circ h = \\mathrm{id}_Y$$$

Lean4

@[simp]
theorem symm_trans_self (h : X ≃ₜ Y) : h.symm.trans h = Homeomorph.refl Y :=
  by
  ext
  apply apply_symm_apply

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

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

Разделы

Аффилиация

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