English
The map that sends a total function f: α → β to its corresponding partial function PFun.lift f is injective.
Русский
Отображение, переводящее пределенную функцию f: α → β в частичную функцию PFun.lift f, инъективно.
LaTeX
$$$\\text{Injective}(\\mathrm{PFun.lift})$$$
Lean4
theorem lift_injective : Injective (PFun.lift : (α → β) → α →. β) := fun _ _ h =>
funext fun a => Part.some_injective <| congr_fun h a