injective_iff_ker_bot — Mathlib

English

A function f is injective iff its kernel equals the bottom Setoid.

Русский

Функция f инъективна тогда и только тогда, когда её ядро равно нижнему отношению.

LaTeX

$$$$ \\text{Injective } f \\iff ker f = \\perp. $$$$

Lean4

/-- A function from α to β is injective iff its kernel is the bottom element of the complete lattice
of equivalence relations on α. -/
theorem injective_iff_ker_bot (f : α → β) : Injective f ↔ ker f = ⊥ :=
  (@eq_bot_iff (Setoid α) _ _ (ker f)).symm

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