compl_sInf' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem compl_sInf' : (sInf s)ᶜ = sSup (HasCompl.compl '' s) :=
  compl_sInf.trans sSup_image.symm

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