eqOn — Mathlib

English

Two equivalent partial equivalences coincide on their source: for every x in the source, e(x) = e'(x).

Русский

Две эквивалентные частичные эквивалентности совпадают на своей области определения: для каждого x из области определения e, e(x) = e'(x).

LaTeX

$$$ \\forall x \\in e.source, \\ e(x) = e'(x) $$$

Lean4

/-- Two equivalent partial equivs coincide on the source. -/
theorem eqOn {e e' : PartialEquiv α β} (h : e ≈ e') : e.source.EqOn e e' :=
  h.2

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