eq_of_eqOnSource_univ — Mathlib

English

If two open partial homeomorphisms are equivalent and both have full source and target (univ), then they are equal.

Русский

Если два открытых частичных гомеоморфизма эквивалентны и имеют полный источник и мишень (univ), то они равны.

LaTeX

$$$ \text{eq_of_eqOnSource_univ} : (e \approx e') \;\land\; e.source = \mathrm{univ} \;\land\; e.target = \mathrm{univ} \Rightarrow e = e' $$$

Lean4

theorem eq_of_eqOnSource_univ {e e' : OpenPartialHomeomorph X Y} (h : e ≈ e') (s : e.source = univ)
    (t : e.target = univ) : e = e' :=
  toPartialEquiv_injective <| PartialEquiv.eq_of_eqOnSource_univ _ _ h s t

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