nonempty_sInter — Mathlib

English

For a collection c of subsets of α, the nonemptiness of the intersection is equivalent to there being an element contained in every member of c.

Русский

Для коллекции c подмножеств α непустость пересечения эквивалентна существованию элемента, принадлежащего каждому элементу c.

LaTeX

$$$$ (\\bigcap_{U \\in c} U).Nonempty \\iff \\exists a, \\forall B \\in c, a \\in B. $$$$

Lean4

@[simp]
theorem nonempty_sInter {c : Set (Set α)} : (⋂₀ c).Nonempty ↔ ∃ a, ∀ b ∈ c, a ∈ b := by
  simp [nonempty_iff_ne_empty, sInter_eq_empty_iff]
    -- classical

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