self_trans_symm

Mathlib.Topology.MetricSpace.DilationEquiv

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

English

A dilation is idempotent with its inverse: e.trans e.symm equals identity on X.

Русский

DilationEquiv между X и X удовлетворяет, что e.trans e.symm = refl X.

LaTeX

$$$\forall e : X \simeq^{\mathrm{d}} X,\ e \circ e^{-1} = \mathrm{refl}(X)$$$

Lean4

@[simp]
theorem self_trans_symm (e : X ≃ᵈ Y) : e.trans e.symm = refl X :=
  DilationEquiv.ext e.symm_apply_apply

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

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

Разделы

Аффилиация

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