completeLattice — Mathlib

English

Under two Galois connections, the image infimum equals a double-infimum composition.

Русский

При двух Гало-соединениях образ инфимума равен двойной композиции инфимума.

LaTeX

$$$(h_1 : ∀ b, GaloisConnection (l_1 b) (swap u b)) (h_2 : ∀ a, GaloisConnection (l_2 a) (u a)) : s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sInf (image2 u s t) = u (sInf s) (sInf t)$$$

Lean4

noncomputable instance completeLattice {α : Type*} [ConditionallyCompleteLattice α] :
    CompleteLattice (WithBot (WithTop α)) :=
  { instInfSet, instSupSet, instBoundedOrder,
    lattice with
    le_sSup := (WithTop.WithBot.completeLattice (α := αᵒᵈ)).sInf_le
    sSup_le := (WithTop.WithBot.completeLattice (α := αᵒᵈ)).le_sInf
    sInf_le := (WithTop.WithBot.completeLattice (α := αᵒᵈ)).le_sSup
    le_sInf := (WithTop.WithBot.completeLattice (α := αᵒᵈ)).sSup_le }

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