eqOnSourceSetoid — Mathlib

English

EqOnSource induces a setoid (an equivalence relation) on OpenPartialHomeomorph X Y, making it into a well-defined quotient by equivalence.

Русский

EqOnSource порождает множество-отношение на OpenPartialHomeomorph X Y, образуя эквивалентность и задавая корректный факторный объект.

LaTeX

$$$\text{eqOnSourceSetoid} : Setoid\bigl(OpenPartialHomeomorph X Y\bigr)$$$

Lean4

/-- `EqOnSource` is an equivalence relation. -/
instance eqOnSourceSetoid : Setoid (OpenPartialHomeomorph X Y) :=
  { PartialEquiv.eqOnSourceSetoid.comap toPartialEquiv with r := EqOnSource }

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