conditionallyCompleteLattice — Mathlib

English

Equations hold with dualities between LHS and RHS infima in a dual setting.

Русский

С учётом двойственных отображений инфимумы сохраняются в двойственной постановке.

LaTeX

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

Lean4

/-- Adding a bottom element to a conditionally complete lattice
gives a conditionally complete lattice -/
noncomputable instance conditionallyCompleteLattice {α : Type*} [ConditionallyCompleteLattice α] :
    ConditionallyCompleteLattice (WithBot α) :=
  { WithBot.lattice with
    le_csSup := (WithTop.conditionallyCompleteLattice (α := αᵒᵈ)).csInf_le
    csSup_le := (WithTop.conditionallyCompleteLattice (α := αᵒᵈ)).le_csInf
    csInf_le := (WithTop.conditionallyCompleteLattice (α := αᵒᵈ)).le_csSup
    le_csInf := (WithTop.conditionallyCompleteLattice (α := αᵒᵈ)).csSup_le }

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