English
Under duality, the image infimum matches the infimum of both sides.
Русский
Под двойственностью инфимума совпадает с инфимума двух сторон.
LaTeX
$$$(h_1 : ∀ b, GaloisConnection (l_1 b) (swap u b)) (h_2 : ∀ a, GaloisConnection (l_2 a) (u a)) : s.Nonempty → BddBelow s → t.Nonempty → BddBelow t → sInf (image2 u s t) = u (sInf s) (sInf t)$$$
Lean4
/-- Create a `ConditionallyCompleteLattice` from a `PartialOrder` and `sup` function
that returns the least upper bound of a nonempty set which is bounded above. Usually this
constructor provides poor definitional equalities. If other fields are known explicitly, they
should be provided; for example, if `inf` is known explicitly, construct the
`ConditionallyCompleteLattice` instance as
```
instance : ConditionallyCompleteLattice my_T :=
{ inf := better_inf,
le_inf := ...,
inf_le_right := ...,
inf_le_left := ...
-- don't care to fix sup, sInf
..conditionallyCompleteLatticeOfsSup my_T _ }
```
-/
def conditionallyCompleteLatticeOfsSup (α : Type*) [H1 : PartialOrder α] [H2 : SupSet α]
(bddAbove_pair : ∀ a b : α, BddAbove ({ a, b } : Set α)) (bddBelow_pair : ∀ a b : α, BddBelow ({ a, b } : Set α))
(isLUB_sSup : ∀ s : Set α, BddAbove s → s.Nonempty → IsLUB s (sSup s)) : ConditionallyCompleteLattice α :=
{ H1, H2 with
sup := fun a b => sSup { a, b }
le_sup_left := fun a b => (isLUB_sSup { a, b } (bddAbove_pair a b) (insert_nonempty _ _)).1 (mem_insert _ _)
le_sup_right := fun a b =>
(isLUB_sSup { a, b } (bddAbove_pair a b) (insert_nonempty _ _)).1 (mem_insert_of_mem _ (mem_singleton _))
sup_le := fun a b _ hac hbc =>
(isLUB_sSup { a, b } (bddAbove_pair a b) (insert_nonempty _ _)).2
(forall_insert_of_forall (forall_eq.mpr hbc) hac)
inf := fun a b => sSup (lowerBounds { a, b })
inf_le_left := fun a b =>
(isLUB_sSup (lowerBounds { a, b }) (Nonempty.bddAbove_lowerBounds ⟨a, mem_insert _ _⟩) (bddBelow_pair a b)).2
fun _ hc => hc <| mem_insert _ _
inf_le_right := fun a b =>
(isLUB_sSup (lowerBounds { a, b }) (Nonempty.bddAbove_lowerBounds ⟨a, mem_insert _ _⟩) (bddBelow_pair a b)).2
fun _ hc => hc <| mem_insert_of_mem _ (mem_singleton _)
le_inf := fun c a b hca hcb =>
(isLUB_sSup (lowerBounds { a, b }) (Nonempty.bddAbove_lowerBounds ⟨a, mem_insert _ _⟩)
⟨c, forall_insert_of_forall (forall_eq.mpr hcb) hca⟩).1
(forall_insert_of_forall (forall_eq.mpr hcb) hca)
sInf := fun s => sSup (lowerBounds s)
csSup_le := fun s a hs ha => (isLUB_sSup s ⟨a, ha⟩ hs).2 ha
le_csSup := fun s a hs ha => (isLUB_sSup s hs ⟨a, ha⟩).1 ha
csInf_le := fun s a hs ha =>
(isLUB_sSup (lowerBounds s) (Nonempty.bddAbove_lowerBounds ⟨a, ha⟩) hs).2 fun _ hb => hb ha
le_csInf := fun s a hs ha => (isLUB_sSup (lowerBounds s) hs.bddAbove_lowerBounds ⟨a, ha⟩).1 ha }
