symm_image_target_eq_source — Mathlib

English

Two partial equivalences that agree on all points and have the same source are equal.

Русский

Два частичных эквивалента, совпадающие на всей области определения и имеющие одинаковый источник, совпадают.

LaTeX

$$$\\forall e,e' : \\mathrm{PartialEquiv}(\\alpha,\\beta),\\; (\\forall x, e(x)=e'(x)) \\land (\\forall x, e.Symm(x)=e'.Symm(x)) \\land (e.source = e'.source) \\Rightarrow e=e'$$$

Lean4

theorem symm_image_target_eq_source : e.symm '' e.target = e.source :=
  e.symm.image_source_eq_target

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