sInter_eq_empty_iff — Mathlib

English

For c ⊆ Set α, the intersection over c is empty iff for every a there exists b ∈ c with a ∉ b.

Русский

Для c ⊆ Set α пересечение над c есть пустое тогда и только тогда существует b ∈ c с a ∉ b.

LaTeX

$$$$ \\bigcap_{U \\in c} U = \\emptyset \\iff \\forall a, \\exists B \\in c, a \\notin B. $$$$

Lean4

theorem sInter_eq_empty_iff {c : Set (Set α)} : ⋂₀ c = ∅ ↔ ∀ a, ∃ b ∈ c, a ∉ b := by
  simp [Set.eq_empty_iff_forall_notMem]
    -- classical

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