English
Dual Galois connections give a formula for the image supremum as a composition of infimum and supremum.
Русский
Двойственные Гало-соединения дают формулу для образа верхнего предела как композицию инфимума и супремума.
LaTeX
$$$(h_1 : ∀ b, GaloisConnection (toDual ∘ l_1 b) (swap u b ∘ ofDual)) (h_2 : ∀ a, GaloisConnection (toDual ∘ l_2 a) (u a ∘ ofDual)) : s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sInf (image2 u s t) = u (sInf s) (sSup t)$$$
Lean4
/-- A version of `conditionallyCompleteLatticeOfsInf` when we already know that `α` is a lattice.
This should only be used when it is both hard and unnecessary to provide `sup` explicitly. -/
def conditionallyCompleteLatticeOfLatticeOfsInf (α : Type*) [H1 : Lattice α] [InfSet α]
(isGLB_sInf : ∀ s : Set α, BddBelow s → s.Nonempty → IsGLB s (sInf s)) : ConditionallyCompleteLattice α :=
{ H1,
conditionallyCompleteLatticeOfsInf α
(fun a b => ⟨a ⊔ b, forall_insert_of_forall (forall_eq.mpr le_sup_right) le_sup_left⟩)
(fun a b => ⟨a ⊓ b, forall_insert_of_forall (forall_eq.mpr inf_le_right) inf_le_left⟩) isGLB_sInf with }
