compl_iSup — Mathlib

English

Complement commutes with iSup: the complement of the supremum equals the supremum of complements.

Русский

Комплемент сохраняет операцию взятия верхней границы: комплемент ⊔ = ⊔ комплементов.

LaTeX

$$$(\bigvee_i f(i)).\mathrm{compl} = \bigvee_i (f(i)).\mathrm{compl}$$$

Lean4

@[simp]
protected theorem compl_iSup (f : ι → UpperSet α) : (⨆ i, f i).compl = ⨆ i, (f i).compl :=
  LowerSet.ext <| by simp only [coe_compl, coe_iSup, compl_iInter, LowerSet.coe_iSup]

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