iInter_eq_empty_iff — Mathlib

English

For a family f : ι → Set α, the intersection over i of f i is empty if and only if for every x there exists i with x ∉ f i.

Русский

Для семейства f : ι → Set α пересечение по i пустое тогда и только тогда для каждого x существует i such that x ∉ f(i).

LaTeX

$$$$ \\bigcap_{i} f(i) = \\emptyset \\iff \\forall x, \\exists i, x \\notin f(i). $$$$

Lean4

theorem iInter_eq_empty_iff {f : ι → Set α} : ⋂ i, f i = ∅ ↔ ∀ x, ∃ i, x ∉ f i := by
  simp [Set.eq_empty_iff_forall_notMem]
    -- classical

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