nonempty_iInter₂ — Mathlib

English

For a two-index family s i j, the nonemptiness of the double intersection is equivalent to the existence of an element common to all s i j: (⋂ i)(⋂ j) s i j Nonempty ↔ ∃ a ∀ i j, a ∈ s i j.

Русский

Для двойного индексированного семейства s(i,j) непустость двойного пересечения эквивалентна существованию элемента, принадлежащего всем s(i,j): (⋂ i)(⋂ j) s i j Nonempty ↔ ∃ a ∀ i j, a ∈ s i j.

LaTeX

$$$$ (\\bigcap_{i} \\bigcap_{j} s(i,j)).Nonempty \\iff \\exists a, \\forall i, \\forall j, a \\in s(i,j). $$$$

Lean4

theorem nonempty_iInter₂ {s : ∀ i, κ i → Set α} : (⋂ (i) (j), s i j).Nonempty ↔ ∃ a, ∀ i j, a ∈ s i j := by
  simp
    -- classical

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