English
Two Part objects are equal if they have the same domain and their values agree pointwise on corresponding domains.
Русский
Два объекта Part равны, если у них совпадает область определения и значения совпадают по каждому элементу области определения.
LaTeX
$$$$\forall o,p: \mathrm{Part}\,\alpha,\; (o.\Dom \leftrightarrow p.\Dom) \to (\forall h_1,h_2,\; o.get h_1 = p.get h_2) \Rightarrow o = p.$$$$
Lean4
/-- `Part` extensionality -/
theorem ext' : ∀ {o p : Part α}, (o.Dom ↔ p.Dom) → (∀ h₁ h₂, o.get h₁ = p.get h₂) → o = p
| ⟨od, o⟩, ⟨pd, p⟩, H1, H2 => by
have t : od = pd := propext H1
cases t; rw [show o = p from funext fun p => H2 p p]
