English
Given a poset α with InfSet and a function isGLB_sInf assigning to each s a greatest lower bound, one constructs a complete lattice on α where the bottom and top are defined by sInf of the whole/universal sets, and the inf and sup are defined by appropriate InfSet constructions.
Русский
Дано упорядоченное множество α с InfSet и функция isGLB_sInf, сопоставляющая каждому множесту s наибольшую нижнюю грань sInf s; строится полное решёточное множество на α, где bot и top задаются через sInf univ и sInf ∅, а операция inf и sup задаются через соответствующие InfSet-конструкции.
LaTeX
$$$\text{CompleteLattice}(\alpha) \text{ с инфом } \inf(a,b) = sInf\{x \mid a \le x \land b \le x\},\; \top = sInf\,\{\},\; \bot = sInf\,\text{univ}$ (при наличии соответствующих условий) $$
Lean4
/-- Create a `CompleteLattice` from a `PartialOrder` and `InfSet`
that returns the greatest lower 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, sSup, bot, top
__ := completeLatticeOfInf my_T _
```
-/
def completeLatticeOfInf (α : Type*) [H1 : PartialOrder α] [H2 : InfSet α]
(isGLB_sInf : ∀ s : Set α, IsGLB s (sInf s)) : CompleteLattice α
where
__ := H1; __ := H2
bot := sInf univ
bot_le _ := (isGLB_sInf univ).1 trivial
top := sInf ∅
le_top a := (isGLB_sInf ∅).2 <| by simp
sup a b := sInf {x : α | a ≤ x ∧ b ≤ x}
inf a b := sInf { a, b }
le_inf a b c hab
hac := by
apply (isGLB_sInf _).2
simp [*]
inf_le_right _ _ := (isGLB_sInf _).1 <| mem_insert_of_mem _ <| mem_singleton _
inf_le_left _ _ := (isGLB_sInf _).1 <| mem_insert _ _
sup_le a b c hac hbc := (isGLB_sInf _).1 <| by simp [*]
le_sup_left _ _ := (isGLB_sInf _).2 fun _ => And.left
le_sup_right _ _ := (isGLB_sInf _).2 fun _ => And.right
le_sInf s _ ha := (isGLB_sInf s).2 ha
sInf_le s _ ha := (isGLB_sInf s).1 ha
sSup s := sInf (upperBounds s)
le_sSup s _ ha := (isGLB_sInf (upperBounds s)).2 fun _ hb => hb ha
sSup_le s _ ha := (isGLB_sInf (upperBounds s)).1 ha
