ker_iff_mem_preimage — Mathlib

English

The elements related to x by the kernel of f are exactly those in the preimage of {f(y)} under f.

Русский

Элементы, связанные с x через ядро f, равны тем, что лежат в предобразе множества {f(y)}.

LaTeX

$$$$ ker f\\ x y \\iff x \\in f^{-1}\\{ f y \\}. $$$$

Lean4

/-- The elements related to x ∈ α by the kernel of f are those in the preimage of f(x) under f. -/
theorem ker_iff_mem_preimage {f : α → β} {x y} : ker f x y ↔ x ∈ f ⁻¹' {f y} :=
  Iff.rfl

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