compl_iInf — Mathlib

English

In a complete Boolean algebra, the complement of the infimum equals the supremum of complements: (iInf f)ᶜ = iSup (f i)ᶜ.

Русский

В полной булевой алгебре дополнение к инфимума равно наибольшему элементу дополнений: (iInf f)ᶜ = ⨆ i, (f i)ᶜ.

LaTeX

$$$\forall f,\; (\inf_i f(i))^{\complement} = \sup_i f(i)^{\complement}.$$$

Lean4

theorem compl_iInf : (iInf f)ᶜ = ⨆ i, (f i)ᶜ :=
  le_antisymm (compl_le_of_compl_le <| le_iInf fun i => compl_le_of_compl_le <| le_iSup (HasCompl.compl ∘ f) i)
    (iSup_le fun _ => compl_le_compl <| iInf_le _ _)

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