preimage_eq_empty_iff — Mathlib

English

The preimage of a singleton is empty if and only if the singleton value is not in the range.

Русский

Предобраз одноточечного множества пусто тогда и только тогда, когда значение не принадлежит диапазону.

LaTeX

$$$f^{-1}({b}) = \\emptyset \\iff b \\notin f.range$$$

Lean4

theorem preimage_eq_empty_iff (f : α →ₛ β) (b : β) : f ⁻¹' { b } = ∅ ↔ b ∉ f.range :=
  preimage_singleton_eq_empty.trans <| not_congr mem_range.symm

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