English
In a dual context, the image infimum equals the composition of a supremum and an infimum.
Русский
В двойственном контексте инфимума образа равен композиции супрема и инфимума.
LaTeX
$$$(h_1 : ∀ b, GaloisConnection (toDual ∘ l_1 b) (swap u b ∘ ofDual)) (h_2 : ∀ a, GaloisConnection (l_2 a) (u a)) : s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sInf (image2 u s t) = u (sSup s) (sInf t)$$$
Lean4
/-- Create a `ConditionallyCompleteLattice` from a `PartialOrder` and `inf` function
that returns the greatest lower bound of a nonempty set which is bounded below. 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, sSup
..conditionallyCompleteLatticeOfsInf my_T _ }
```
-/
def conditionallyCompleteLatticeOfsInf (α : Type*) [H1 : PartialOrder α] [H2 : InfSet α]
(bddAbove_pair : ∀ a b : α, BddAbove ({ a, b } : Set α)) (bddBelow_pair : ∀ a b : α, BddBelow ({ a, b } : Set α))
(isGLB_sInf : ∀ s : Set α, BddBelow s → s.Nonempty → IsGLB s (sInf s)) : ConditionallyCompleteLattice α :=
{ H1, H2 with
inf := fun a b => sInf { a, b }
inf_le_left := fun a b => (isGLB_sInf { a, b } (bddBelow_pair a b) (insert_nonempty _ _)).1 (mem_insert _ _)
inf_le_right := fun a b =>
(isGLB_sInf { a, b } (bddBelow_pair a b) (insert_nonempty _ _)).1 (mem_insert_of_mem _ (mem_singleton _))
le_inf := fun _ a b hca hcb =>
(isGLB_sInf { a, b } (bddBelow_pair a b) (insert_nonempty _ _)).2
(forall_insert_of_forall (forall_eq.mpr hcb) hca)
sup := fun a b => sInf (upperBounds { a, b })
le_sup_left := fun a b =>
(isGLB_sInf (upperBounds { a, b }) (Nonempty.bddBelow_upperBounds ⟨a, mem_insert _ _⟩) (bddAbove_pair a b)).2
fun _ hc => hc <| mem_insert _ _
le_sup_right := fun a b =>
(isGLB_sInf (upperBounds { a, b }) (Nonempty.bddBelow_upperBounds ⟨a, mem_insert _ _⟩) (bddAbove_pair a b)).2
fun _ hc => hc <| mem_insert_of_mem _ (mem_singleton _)
sup_le := fun a b c hac hbc =>
(isGLB_sInf (upperBounds { a, b }) (Nonempty.bddBelow_upperBounds ⟨a, mem_insert _ _⟩)
⟨c, forall_insert_of_forall (forall_eq.mpr hbc) hac⟩).1
(forall_insert_of_forall (forall_eq.mpr hbc) hac)
sSup := fun s => sInf (upperBounds s)
le_csInf := fun s a hs ha => (isGLB_sInf s ⟨a, ha⟩ hs).2 ha
csInf_le := fun s a hs ha => (isGLB_sInf s hs ⟨a, ha⟩).1 ha
le_csSup := fun s a hs ha =>
(isGLB_sInf (upperBounds s) (Nonempty.bddBelow_upperBounds ⟨a, ha⟩) hs).2 fun _ hb => hb ha
csSup_le := fun s a hs ha => (isGLB_sInf (upperBounds s) hs.bddBelow_upperBounds ⟨a, ha⟩).1 ha }
