English
If two partial functions f and g have the same domain membership for every input and agree on all values whenever they are defined, then f = g.
Русский
Если две частичные функции f и g имеют одинаковую принадлежность к области определения для каждого аргумента и совпадают на всех значениях, когда определены, то f = g.
LaTeX
$$$\\big( \\forall a,\; a \\in \\mathrm{Dom}(f) \\leftrightarrow a \\in \\mathrm{Dom}(g) \\big) \\land \\big( \\forall a\\ p\\ q,\; f(a,p) = g(a,q) \\big) \\Rightarrow f = g$$$
Lean4
/-- Partial function extensionality -/
theorem ext' {f g : α →. β} (H1 : ∀ a, a ∈ Dom f ↔ a ∈ Dom g) (H2 : ∀ a p q, f.fn a p = g.fn a q) : f = g :=
funext fun a => Part.ext' (H1 a) (H2 a)
