compl_iSup — Mathlib

English

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

Русский

Для произвольной семейной функции нижних множеств справедливо: (⨆ i, f i).compl = ⨆ i, (f i).compl.

LaTeX

$$$ (\big \vee_i f_i).\mathrm{compl} = \big \vee_i (f_i).\mathrm{compl} $$$

Lean4

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

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