lift_injective — Mathlib

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

Похожие утверждения