apply_symm_apply

Mathlib.Topology.MetricSpace.Isometry

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

English

h(h.symm(y)) = y for all y in β.

Русский

h(h.symm(y)) = y для каждого y ∈ β.

LaTeX

$$$\forall y,\ h(h.symm(y)) = y$$$

Lean4

@[simp]
theorem apply_symm_apply (h : α ≃ᵢ β) (y : β) : h (h.symm y) = y :=
  h.toEquiv.apply_symm_apply y

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

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

Разделы

Аффилиация

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