English
Dual to Inf-based construction: given a poset α with SupSet and a function isLUB_sSup providing least upper bounds, define a complete lattice where top is sSup univ, bottom is sSup ∅, and inf/sup are defined via SupSet constructions.
Русский
Дубликат конструкций через верхние границы: дано упорядоченное множество α с SupSet и функция isLUB_sSup, задающая наименьшие верхние границы. Строим полную решётку, где top = sSup univ, bot = sSup ∅, а operations inf и sup задаются через соответствующие конструкции SupSet.
LaTeX
$$$\text{CompleteLattice}(\alpha) \text{ с верх } \top = sSup(\{\,\}),\; \bot = sSup(∅),\; \text{inf/ Sup через SupSet}$$$
Lean4
/-- Create a `CompleteLattice` from a `PartialOrder` and `SupSet`
that returns the least upper bound of a set. 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 `CompleteLattice`
instance as
```
instance : CompleteLattice my_T where
inf := better_inf
le_inf := ...
inf_le_right := ...
inf_le_left := ...
-- don't care to fix sup, sInf, bot, top
__ := completeLatticeOfSup my_T _
```
-/
def completeLatticeOfSup (α : Type*) [H1 : PartialOrder α] [H2 : SupSet α]
(isLUB_sSup : ∀ s : Set α, IsLUB s (sSup s)) : CompleteLattice α
where
__ := H1; __ := H2
top := sSup univ
le_top _ := (isLUB_sSup univ).1 trivial
bot := sSup ∅
bot_le x := (isLUB_sSup ∅).2 <| by simp
sup a b := sSup { a, b }
sup_le a b c hac hbc := (isLUB_sSup _).2 (by simp [*])
le_sup_left _ _ := (isLUB_sSup _).1 <| mem_insert _ _
le_sup_right _ _ := (isLUB_sSup _).1 <| mem_insert_of_mem _ <| mem_singleton _
inf a b := sSup {x | x ≤ a ∧ x ≤ b}
le_inf a b c hab hac := (isLUB_sSup _).1 <| by simp [*]
inf_le_left _ _ := (isLUB_sSup _).2 fun _ => And.left
inf_le_right _ _ := (isLUB_sSup _).2 fun _ => And.right
sInf s := sSup (lowerBounds s)
sSup_le s _ ha := (isLUB_sSup s).2 ha
le_sSup s _ ha := (isLUB_sSup s).1 ha
sInf_le s _ ha := (isLUB_sSup (lowerBounds s)).2 fun _ hb => hb ha
le_sInf s _ ha := (isLUB_sSup (lowerBounds s)).1 ha
