compl_iUnion₂ — Mathlib

English

For s : ∀ i, κ i → Set α, the complement of the union over i and j satisfies (⋃ i (⋃ j s(i,j)))^c = ⋂ i (⋂ j (s(i,j))^c).

Русский

Для s(i,j) верно: (⋃_i ⋃_j s(i,j))^c = ⋂_i ⋂_j (s(i,j))^c.

LaTeX

$$$$ \\left( \\bigcup_{i} \\bigcup_{j} s(i,j) \\right)^c = \\bigcap_{i} \\bigcap_{j} (s(i,j))^c $$$$

Lean4

theorem compl_iUnion₂ (s : ∀ i, κ i → Set α) : (⋃ (i) (j), s i j)ᶜ = ⋂ (i) (j), (s i j)ᶜ := by simp_rw [compl_iUnion]

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