English
A finite bounded lattice is complete.
Русский
Конечная ограниченная решётка полна.
LaTeX
$$[Lattice α] [BoundedOrder α] ⇒ CompleteLattice α$$
Lean4
/-- A finite bounded lattice is complete. -/
noncomputable abbrev toCompleteLattice [Lattice α] [BoundedOrder α] : CompleteLattice α
where
__ := ‹Lattice α›
__ := ‹BoundedOrder α›
sSup := fun s => s.toFinset.sup id
sInf := fun s => s.toFinset.inf id
le_sSup := fun _ _ ha => Finset.le_sup (f := id) (Set.mem_toFinset.mpr ha)
sSup_le := fun _ _ ha => Finset.sup_le fun _ hb => ha _ <| Set.mem_toFinset.mp hb
sInf_le := fun _ _ ha => Finset.inf_le (Set.mem_toFinset.mpr ha)
le_sInf := fun _ _ ha => Finset.le_inf fun _ hb => ha _ <| Set.mem_toFinset.mp hb
