symm_trans_self — Mathlib

English

Composition of the inverse with the original partial equivalence is equivalent to the restriction of the identity to the target.

Русский

Сложение обратной связи с самой частичной эквивалентностью эквивалентно ограничению единицы на целевую область.

LaTeX

$$$ e^{\\mathrm{symm}} \\trans e \\approx \\mathrm{ofSet}(e.target) $$$

Lean4

/-- Composition of the inverse of a partial equivalence and this partial equivalence is equivalent
to the restriction of the identity to the target. -/
theorem symm_trans_self : e.symm.trans e ≈ ofSet e.target :=
  self_trans_symm e.symm

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