symm_comp_self

Mathlib.Topology.Homeomorph.Defs

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

English

The composition of a homeomorphism with its inverse yields the identity on the domain.

Русский

Композиция гомеоморфизма с его обратной картой дает тождество на области определения.

LaTeX

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

Lean4

@[simp]
theorem symm_comp_self (h : X ≃ₜ Y) : h.symm ∘ h = id :=
  funext h.symm_apply_apply

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

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

Разделы

Аффилиация

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