compl_sInf — Mathlib

English

Let S be a set of lower sets. Then the complement of the infimum of S equals the infimum (in upper sets) of the complements: (sInf S).compl = ⨅ s ∈ S, LowerSet.compl s.

Русский

Пусть S — множество нижних множеств. Тогда комплемент на-inf множества S равен infimum над комплементами элементов S.

LaTeX

$$$ (\operatorname{sInf} S).\mathrm{compl} = \big\wedge_{s \in S} s.\mathrm{compl} $$$

Lean4

protected theorem compl_sInf (S : Set (LowerSet α)) : (sInf S).compl = ⨅ s ∈ S, LowerSet.compl s :=
  UpperSet.ext <| by simp only [coe_compl, coe_sInf, compl_iInter₂, UpperSet.coe_iInf₂]

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