compl_iInf₂ — Mathlib

English

Complement commutes with iInf₂: the complement of the infimum over two indices equals the infimum of complements over those indices.

Русский

Комплемент сохраняет двойной iInf: комплемент ⨅_{i,j} f(i,j) = ⨅_{i,j} (f(i,j)).compl.

LaTeX

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

Lean4

theorem compl_iInf₂ (f : ∀ i, κ i → UpperSet α) : (⨅ (i) (j), f i j).compl = ⨅ (i) (j), (f i j).compl := by simp

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