eqOnSource_iff — Mathlib

English

Two open partial homeomorphisms e and e' satisfy EqOnSource exactly when their toPartialEquiv representations have the corresponding EqOnSource relation.

Русский

Два открытых частичных гомеоморфизма e и e' удовлетворяют EqOnSource тогда и только тогда, когда их представления в виде toPartialEquiv удовлетворяют соответствующему relation EqOnSource.

LaTeX

$$$ \text{eqOnSource_iff} : \; (e,e') : OpenPartialHomeomorph X Y \quad \Rightarrow\quad (e \approx e') \;\iff\; (e.toPartialEquiv, e'.toPartialEquiv) \text{ удовлетворяют } PartialEquiv.EqOnSource$$$

Lean4

theorem eqOnSource_iff (e e' : OpenPartialHomeomorph X Y) :
    EqOnSource e e' ↔ PartialEquiv.EqOnSource e.toPartialEquiv e'.toPartialEquiv :=
  Iff.rfl

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