compl_iInter₂ — Mathlib

English

For s : ∀ i, κ i → Set α, the complement of the intersection over i and j equals the union over i and j of the complements: (⋂ 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

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

Lean4

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

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