target_eq — Mathlib

English

Two equivalent open partial homeomorphisms have the same target: e ≈ e' implies e.target = e'.target.

Русский

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

LaTeX

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

Lean4

/-- Two equivalent open partial homeomorphisms have the same target. -/
theorem target_eq {e e' : OpenPartialHomeomorph X Y} (h : e ≈ e') : e.target = e'.target :=
  h.symm'.1

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