symm_trans_apply

Mathlib.Topology.MetricSpace.Isometry

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

English

Bijective IsometryEquiv.symm

Русский

Биективность симм отображения IsometryEquiv.symm

LaTeX

$$$\mathrm{Bijective}(\mathrm{IsometryEquiv.symm})$$$

Lean4

@[simp]
theorem symm_trans_apply (h₁ : α ≃ᵢ β) (h₂ : β ≃ᵢ γ) (x : γ) : (h₁.trans h₂).symm x = h₁.symm (h₂.symm x) :=
  rfl

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

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

Разделы

Аффилиация

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