compl_sSup' — Mathlib

English

Complement of supremum over a set equals the infimum of the image under complementation: (sSup s)ᶜ = sInf (HasCompl.compl '' s).

Русский

Дополнение к объединению множества равно инфимума дополнений образа множества под дополнением: (sSup s)ᶜ = sInf (HasCompl.compl '' s).

LaTeX

$$$ (\mathrm{sSup}~s)^{\complement} = \mathrm{Inf} (\mathrm{HasCompl.compl} '' s). $$$

Lean4

theorem compl_sSup' : (sSup s)ᶜ = sInf (HasCompl.compl '' s) :=
  compl_sSup.trans sInf_image.symm

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