self_trans_symm — Mathlib

English

The composition of an open partial homeomorphism with its inverse is equivalent to the restriction of the identity to its source.

Русский

Состав открытого частичного гомеоморфизма с его обратным эквивалентен ограничению тождества на источнике.

LaTeX

$$$ e.trans e.symm \approx OpenPartialHomeomorph.ofSet e.source e.open_source $$$

Lean4

/-- Composition of an open partial homeomorphism and its inverse is equivalent to the restriction of
the identity to the source -/
theorem self_trans_symm : e.trans e.symm ≈ OpenPartialHomeomorph.ofSet e.source e.open_source :=
  PartialEquiv.self_trans_symm _

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