symm_eqOn_target — Mathlib

English

Two equivalent open partial homeomorphisms have the same source: if e ≈ e' then e.source = e'.source.

Русский

Два эквивалентных открытых частичных гомеоморфизма имеют одинаковый источник: e ≈ e' ⇒ e.source = e'.source.

LaTeX

$$$ e \approx e' \Rightarrow e.source = e'.source $$$

Lean4

/-- Two equivalent open partial homeomorphisms have coinciding `invFun` on the target -/
theorem symm_eqOn_target {e e' : OpenPartialHomeomorph X Y} (h : e ≈ e') : EqOn e.symm e'.symm e.target :=
  h.symm'.2

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