English
If h: e.IsImage s t and hs: e.source ∩ s = e'.source ∩ s and heq: EqOn e e' (e.source ∩ s), then EqOn e.symm e'.symm (e.target ∩ t).
Русский
Если два частичных эквививалента совпадают на пересечении источника с s и имеют одинаковые значения на этом пересечении, то их оборотные отображения совпадают на пересечении целевой части с t.
LaTeX
$$$\\forall e,e':\\mathrm{PartialEquiv}(\\alpha,\\beta),\\; s,t\\subseteq \\alpha,\\; (h:\\ e.IsImage\\,s\\,t)\\, (hs:\\ e.source \\cap s = e'.source \\cap s)\\, (heq:\\EqOn e e' (e.source \\cap s))\\Rightarrow EqOn e.symm e'.symm (e.target \\cap t)$$$
Lean4
theorem symm_eq_on_of_inter_eq_of_eqOn {e' : PartialEquiv α β} (h : e.IsImage s t) (hs : e.source ∩ s = e'.source ∩ s)
(heq : EqOn e e' (e.source ∩ s)) : EqOn e.symm e'.symm (e.target ∩ t) :=
by
rw [← h.image_eq]
rintro y ⟨x, hx, rfl⟩
have hx' := hx; rw [hs] at hx'
rw [e.left_inv hx.1, heq hx, e'.left_inv hx'.1]
