graphOn_univ_injective — Mathlib

English

There exists a function f such that s equals the graph of f on the projection Prod.fst '' s iff Prod.fst is injective on s.

Русский

Существует функция f такая, что s является графом f над проекцией Prod.fst '' s тогда и только тогда, когда Prod.fst инъективна на s.

LaTeX

$$$(\\exists f : α \\to β)(s = \\mathrm{graphOn} f (\\mathrm{Prod.fst}'' s)) \\iff \\mathrm{InjOn}(\\mathrm{Prod.fst}, s).$$$

Lean4

theorem graphOn_univ_injective : Injective (univ.graphOn : (α → β) → Set (α × β)) := fun _f _g ↦ graphOn_univ_inj.1

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