nonempty_iInter — Mathlib

English

For a family f : ι → Set α, the nonemptiness of the intersection is equivalent to the existence of a point common to all f(i): (⋂ i, f i).Nonempty ↔ ∃ x, ∀ i, x ∈ f i.

Русский

Для семейства f : ι → Set α непустость пересечения эквивалентна существованию точки, принадлежящей всем f(i): (⋂ i, f i).Nonempty ↔ ∃ x, ∀ i, x ∈ f i.

LaTeX

$$$$ (\\bigcap_{i} f(i)).Nonempty \\iff \\exists x, \\forall i, x \\in f(i). $$$$

Lean4

@[simp]
theorem nonempty_iInter {f : ι → Set α} : (⋂ i, f i).Nonempty ↔ ∃ x, ∀ i, x ∈ f i := by
  simp [nonempty_iff_ne_empty, iInter_eq_empty_iff]
    -- classical

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