compl_iInf₂ — Mathlib

English

For any family f i j of lower sets, the complement distributes over the double infimum: (⨅ 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

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

Lean4

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

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