compl_iSup₂ — Mathlib

English

For any family f i j of lower sets, the complement distributes over the double supremum: (⨆ i ⨆ j, f i j).compl = ⨆ i ⨆ j, (f i j).compl.

Русский

Для двойного объединения нижних множеств справедлив комплемент: (⨆ i ⨆ j, f(i,j)).compl = ⨆ i ⨆ j, f(i,j).compl.

LaTeX

$$$ (\bigsqcup_{i,j} f(i,j)).\mathrm{compl} = \bigsqcup_{i,j} (f(i,j)).\mathrm{compl} $$$

Lean4

@[simp]
theorem compl_iSup₂ (f : ∀ i, κ i → LowerSet α) : (⨆ (i) (j), f i j).compl = ⨆ (i) (j), (f i j).compl := by
  simp_rw [LowerSet.compl_iSup]

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