self_trans_symm

Mathlib.Geometry.Manifold.Diffeomorph

URI: https://scilib.ai/kg/mathlib#Diffeomorph.self_trans_symm

English

The trans operation respects identity on both sides and yields a coherent composition.

Русский

Операция trans сохраняет тождественный элемент и дает связную композицию.

LaTeX

$$$\text{trans}(\mathrm{refl}, h) = h$ and $\mathrm{refl}.trans(h) = h.$$$

Lean4

@[simp]
theorem self_trans_symm (h : M ≃ₘ^n⟮I, J⟯ N) : h.trans h.symm = Diffeomorph.refl I M n :=
  ext h.symm_apply_apply

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

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

Разделы

Аффилиация

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