English
The restruced partial equivalence has the same function as the original on its domain.
Русский
Ограничённый частичный эквивалент имеет ту же функцию на своей области определения.
LaTeX
$$$\\text{restr_coe}: (e.restr s : \\alpha \\to \\beta) = e.toFun$$$
Lean4
/-- Two partial equivs that have the same `source`, same `toFun` and same `invFun`, coincide. -/
@[ext]
protected theorem ext {e e' : PartialEquiv α β} (h : ∀ x, e x = e' x) (hsymm : ∀ x, e.symm x = e'.symm x)
(hs : e.source = e'.source) : e = e' :=
by
have A : (e : α → β) = e' := by
ext x
exact h x
have B : (e.symm : β → α) = e'.symm := by
ext x
exact hsymm x
have I : e '' e.source = e.target := e.image_source_eq_target
have I' : e' '' e'.source = e'.target := e'.image_source_eq_target
rw [A, hs, I'] at I
cases e; cases e'
simp_all
