graph_injective — Mathlib

English

The map sending a function to its graph is injective: different functions have different graphs.

Русский

Отображение функций в их графы инъективно: разные функции имеют разные графы.

LaTeX

$$$\text{Injective } (\text{graph} : (\alpha \to \beta) \to \text{SetRel } \alpha \beta)$$$

Lean4

theorem graph_injective : Injective (graph : (α → β) → SetRel α β) := by aesop (add simp [Injective, Set.ext_iff])

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