English
A meet-semilattice where every inf-closed set has a greatest lower bound is automatically complete: sInf(s) = sInf(infClosure(s)).
Русский
Завершение meet-структуры: если каждый inf-закрытый набор имеет наибольшую нижнюю границу, то вся структура является полной; задаётся sInf(s) = sInf(infClosure(s)).
LaTeX
$$$\\text{CompleteSemilatticeInf } α\\; \\\\text{with } \\mathrm{sInf}(s) = sInf(\\\\operatorname{infClosure}(s)).$$$
Lean4
/-- A meet-semilattice where every inf-closed set has a greatest lower bound is automatically
complete. -/
def toCompleteSemilatticeInf [SemilatticeInf α] (sInf : Set α → α) (h : ∀ s, InfClosed s → IsGLB s (sInf s)) :
CompleteSemilatticeInf α where
sInf := fun s => sInf (infClosure s)
sInf_le _ _ ha := (h _ infClosed_infClosure).1 <| subset_infClosure ha
le_sInf s a ha := (le_isGLB_iff <| h _ infClosed_infClosure).2 <| by rwa [lowerBounds_infClosure]
