completeLattice — Mathlib

English

In a dual setting, the image supremum equals the composition of infimum and supremum under Galois connections.

Русский

В двойственной постановке образ верхнего предела равен композиции инфимума и супремума с учётом Гало-соединений.

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

Lean4

noncomputable instance completeLattice {α : Type*} [ConditionallyCompleteLattice α] :
    CompleteLattice (WithTop (WithBot α)) :=
  { instInfSet, instSupSet, boundedOrder,
    lattice with
    le_sSup := fun _ a haS => (WithTop.isLUB_sSup' ⟨a, haS⟩).1 haS
    sSup_le := fun S a ha => by
      rcases S.eq_empty_or_nonempty with h | h
      · change ite _ _ _ ≤ a
        simp [h]
      · exact (WithTop.isLUB_sSup' h).2 ha
    sInf_le := fun S a haS =>
      show ite _ _ _ ≤ a by
        simp only [OrderBot.bddBelow, not_true_eq_false, or_false]
        split_ifs with h₁
        · cases a
          · exact le_rfl
          cases h₁ haS
        · cases a
          · exact le_top
          · apply WithTop.coe_le_coe.2
            refine csInf_le ?_ haS
            use ⊥
            intro b _
            exact bot_le
    le_sInf := fun _ a haS => (WithTop.isGLB_sInf' ⟨a, haS⟩).2 haS }

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