English
If e and e' are partial equivalences with the same image on s, i.e., e.IsImage s t and e'.IsImage s t, and if e and e' agree on e.source ∩ s, then e.target ∩ t = e'.target ∩ t.
Русский
Если два частичных эквивилизма совпадают на пересечении источников с s и имеют одинаковые образы, то их целевые части на t совпадают.
LaTeX
$$$\\forall e,e':\\mathrm{PartialEquiv}(\\alpha,\\beta),\\; s,t\\subseteq \\alpha,\\; (h:\\ e.IsImage\\,s\\,t)\\, (h':\\ e'.IsImage\\,s\\,t)\\; (hs:\\ e.source \\cap s = e'.source \\cap s)\\; (heq:\\EqOn e e' (e.source \\cap s))\\Rightarrow e.target \\cap t = e'.target \\cap t$$$
Lean4
theorem inter_eq_of_inter_eq_of_eqOn {e' : PartialEquiv α β} (h : e.IsImage s t) (h' : e'.IsImage s t)
(hs : e.source ∩ s = e'.source ∩ s) (heq : EqOn e e' (e.source ∩ s)) : e.target ∩ t = e'.target ∩ t := by
rw [← h.image_eq, ← h'.image_eq, ← hs, heq.image_eq]
