English
Let S be a nonempty set of lower sets of a linear ordered type. Then the complement of the supremum of S equals the supremum (in upper sets) of the complements of the elements of S: (sSup S).compl = ⨆ s ∈ S, LowerSet.compl s.
Русский
Пусть S — множество нижних множеств в линейном упорядоченном множестве. Тогда комплемент над наибольшим элементом множества S равен наибольшему в верхних множествах комплементам элементов S: (sSup S).compl = ⨆ s ∈ S, LowerSet.compl s.
LaTeX
$$$ (\operatorname{sSup} S).\mathrm{compl} = \big\vee_{s \in S} s.\mathrm{compl} \ $$$
Lean4
protected theorem compl_sSup (S : Set (LowerSet α)) : (sSup S).compl = ⨆ s ∈ S, LowerSet.compl s :=
UpperSet.ext <| by simp only [coe_compl, coe_sSup, compl_iUnion₂, UpperSet.coe_iSup₂]
