conditionallyCompleteLattice — Mathlib

English

If appropriate Galois connections exist, the two-argument image infimum equals an infimum-supremum combination.

Русский

Если существуют подходящие Гало-соединения, инфимума образа двух аргументов равна сочетанию инфимума и супремума.

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 → BddAbove t → sInf (image2 u s t) = u (sInf s) (sSup t)$$$

Lean4

/-- Adding a top element to a conditionally complete lattice
gives a conditionally complete lattice -/
noncomputable instance conditionallyCompleteLattice {α : Type*} [ConditionallyCompleteLattice α] :
    ConditionallyCompleteLattice (WithTop α) :=
  { lattice, instSupSet,
    instInfSet with
    le_csSup := fun _ a _ haS => (WithTop.isLUB_sSup' ⟨a, haS⟩).1 haS
    csSup_le := fun _ _ hS haS => (WithTop.isLUB_sSup' hS).2 haS
    csInf_le := fun _ _ hS haS => (WithTop.isGLB_sInf' hS).1 haS
    le_csInf := fun _ a _ haS => (WithTop.isGLB_sInf' ⟨a, haS⟩).2 haS }

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