apply_symm_apply

Mathlib.Topology.Homeomorph.Defs

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

English

For h, h.symm, and y, h(h.symm(y)) = y.

Русский

Для h, h.symm и y верно h(h.symm(y)) = y.

LaTeX

$$$$ \forall h:\, X \simeq_t Y,\; \forall y:\, Y,\; h(h^{\mathrm{symm}}(y)) = y. $$$$

Lean4

@[simp]
theorem apply_symm_apply (h : X ≃ₜ Y) (y : Y) : h (h.symm y) = y :=
  h.toEquiv.apply_symm_apply y

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

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

Разделы

Аффилиация

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