EqOnSource — Mathlib

English

Two open partial homeomorphisms are related by EqOnSource exactly when their underlying partial equivalences have EqOn-source equality.

Русский

Два открытых частичных гомеоморфа равны по EqOnSource тогда и только тогда, когда соответствующие им частичные эквиваленты имеют равенство на источнике.

LaTeX

$$$ EqOnSource\left(e,e'\right) \iff PartialEquiv.EqOnSource\left(e.toPartialEquiv, e'.toPartialEquiv\right) $$$

Lean4

/-- `EqOnSource e e'` means that `e` and `e'` have the same source, and coincide there. They
should really be considered the same partial equivalence. -/
def EqOnSource (e e' : OpenPartialHomeomorph X Y) : Prop :=
  e.source = e'.source ∧ EqOn e e' e.source

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