symm_trans_self

Mathlib.Topology.Algebra.ContinuousAffineEquiv

URI: https://scilib.ai/kg/mathlib#ContinuousAffineEquiv.symm_trans_self

English

The symmetric of the trans of an equivalence with itself yields a reverse relation.

Русский

Симметрическое отношение пересечения с самим собой возвращает обратное отношение.

LaTeX

$$$e^{\mathrm{symm}} \circ e = \mathrm{refl}$$$

Lean4

@[simp]
theorem symm_trans_self (e : P₁ ≃ᴬ[k] P₂) : e.symm.trans e = refl k P₂ :=
  ext e.apply_symm_apply

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

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

Разделы

Аффилиация

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