iUnion₂_eq_univ_iff — Mathlib

English

For a double-indexed family s : ∀ i, κ i → Set α, the union over i and j of s i j equals univ if and only if every element a ∈ α lies in some s(i,j): ⋃ (i) (j), s i j = univ ↔ ∀ a, ∃ i j, a ∈ s i j.

Русский

Для двойного индексированного семейства s i j, объединение по i и j равно единице тогда и только тогда каждый элемент a лежит в некотором s(i,j).

LaTeX

$$$$ \\bigcup_{i} \\bigcup_{j} s(i,j) = \\text{univ} \\iff \\forall a, \\exists i, \\exists j, a \\in s(i,j). $$$$

Lean4

theorem iUnion₂_eq_univ_iff {s : ∀ i, κ i → Set α} : ⋃ (i) (j), s i j = univ ↔ ∀ a, ∃ i j, a ∈ s i j := by
  simp only [iUnion_eq_univ_iff, mem_iUnion]

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