eqOn — Mathlib

English

Two equivalent open partial homeomorphisms have coinciding toFun on the source: e ≈ e' implies EqOn e e' e.source.

Русский

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

LaTeX

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

Lean4

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

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