iInter₂_eq_empty_iff — Mathlib

English

For a two-parameter family s i j, the intersection over i and j is empty iff for every a there exist i and j with a ∉ s i j.

Русский

Для двухпараметрического семейства s(i,j) пересечение по i и j пустое тогда и только тогда существует пара i,j с a ∉ s(i,j).

LaTeX

$$$$ \\bigcap_{i} \\bigcap_{j} s(i,j) = \\emptyset \\iff \\forall a, \\exists i, \\exists j, a \\notin s(i,j). $$$$

Lean4

theorem iInter₂_eq_empty_iff {s : ∀ i, κ i → Set α} : ⋂ (i) (j), s i j = ∅ ↔ ∀ a, ∃ i j, a ∉ s i j := by
  simp only [eq_empty_iff_forall_notMem, mem_iInter, not_forall]
    -- classical

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