preimage_singleton_eq_empty — Mathlib

English

For all f and y, f^{-1}({y}) = ∅ iff y ∉ range f.

Русский

Пусть f: A → B. Тогда f^{-1}({y}) = ∅ тогда и только тогда, когда y не принадлежит образу f.

LaTeX

$$$$ f^{-1}(\\{y\\}) = \\emptyset \\iff y \\notin \\operatorname{range}(f) $$$$

Lean4

theorem preimage_singleton_eq_empty {f : α → β} {y : β} : f ⁻¹' { y } = ∅ ↔ y ∉ range f :=
  not_nonempty_iff_eq_empty.symm.trans preimage_singleton_nonempty.not

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