English
There is a natural equivalence between partial functions α →. β and pairs (p : α → Prop, f : Subtype p → β).
Русский
Существует естественное эквивалентное соответствие между частичными функциями α →. β и парами (p : α → Prop, f : Subtype p → β).
LaTeX
$$$ (\\alpha \\to^. \\beta) \\simeq \\Sigma p: \\alpha \\to \\mathrm{Prop},\\; (\\mathrm{Subtype}\\ p \\to \\beta) $$$
Lean4
/-- The type of partial functions `α →. β` is equivalent to
the type of pairs `(p : α → Prop, f : Subtype p → β)`. -/
def equivSubtype : (α →. β) ≃ Σ p : α → Prop, Subtype p → β :=
⟨fun f => ⟨fun a => (f a).Dom, asSubtype f⟩, fun f x => ⟨f.1 x, fun h => f.2 ⟨x, h⟩⟩, fun _ =>
funext fun _ => Part.eta _, fun ⟨p, f⟩ => by dsimp; congr⟩
