symm_apply_apply

Mathlib.Topology.MetricSpace.DilationEquiv

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

English

The inverse image under e of its image on x returns x.

Русский

Обратное приложение e к изображению e на x возвращает x.

LaTeX

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

Lean4

@[simp]
theorem symm_apply_apply (e : X ≃ᵈ Y) (x : X) : e.symm (e x) = x :=
  e.left_inv x

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

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

Разделы

Аффилиация

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