symm_trans_self — Mathlib

English

The inverse composition is equivalent to the restriction of the inverse target to the image of the source.

Русский

Обратная композиция эквивалентна ограничению обратной мишени на изображение источника.

LaTeX

$$$ e.symm.trans e \approx OpenPartialHomeomorph.ofSet e.target e.open_target $$$

Lean4

theorem symm_trans_self : e.symm.trans e ≈ OpenPartialHomeomorph.ofSet e.target e.open_target :=
  e.symm.self_trans_symm

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