compl_sSup — Mathlib

English

Complement of the supremum over a set equals the supremum over complements.

Русский

Комплемент над множеством верхних множеств равен верхнему пределу комплементов элементов множества.

LaTeX

$$$(sSup S).\mathrm{compl} = \bigvee_{s \in S} s.\mathrm{compl}$$$

Lean4

@[simp]
protected theorem compl_sSup (S : Set (UpperSet α)) : (sSup S).compl = ⨆ s ∈ S, UpperSet.compl s :=
  LowerSet.ext <| by simp only [coe_compl, coe_sSup, compl_iInter₂, LowerSet.coe_iSup₂]

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