English
With a dual pair of Galois connections, the image infimum equals the infimum of the dual supremums.
Русский
С двойной парой связей Гало инфимума образа равна инфимуму двойственных верхних пределов.
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 (sSup s) (sSup t)$$$
Lean4
/-- A version of `conditionallyCompleteLatticeOfsSup` when we already know that `α` is a lattice.
This should only be used when it is both hard and unnecessary to provide `inf` explicitly. -/
def conditionallyCompleteLatticeOfLatticeOfsSup (α : Type*) [H1 : Lattice α] [SupSet α]
(isLUB_sSup : ∀ s : Set α, BddAbove s → s.Nonempty → IsLUB s (sSup s)) : ConditionallyCompleteLattice α :=
{ H1,
conditionallyCompleteLatticeOfsSup α
(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⟩) isLUB_sSup with }
