instCompleteLattice — Mathlib

English

The supremum in Set.Iic a commutes with the ambient supremum of the image.

Русский

Супремум в Set.Iic a коммутирует с верхним супремумом образов в α.

LaTeX

$$$$ \uparrow(\operatorname{sSup} S) = \operatorname{sSup}(\uparrow''S). $$$$

Lean4

instance instCompleteLattice : CompleteLattice (Iic a)
    where
  sSup S := ⟨sSup ((↑) '' S), by simpa using fun b hb _ ↦ hb⟩
  sInf S := ⟨a ⊓ sInf ((↑) '' S), by simp⟩
  le_sSup _ _ hb := le_sSup <| mem_image_of_mem Subtype.val hb
  sSup_le _ _ hb := sSup_le <| fun _ ⟨c, hc, hc'⟩ ↦ hc' ▸ hb c hc
  sInf_le _ _ hb := inf_le_of_right_le <| sInf_le <| mem_image_of_mem Subtype.val hb
  le_sInf _ b hb := le_inf_iff.mpr ⟨b.property, le_sInf fun _ ⟨d, hd, hd'⟩ ↦ hd' ▸ hb d hd⟩
  le_top := by simp
  bot_le := by simp

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