English
Define a closure operator from a predicate p preserved under infima: p(sInf S) holds when p holds for all s-elements; the resulting c is a closure operator.
Русский
Задаётся замыкатель из предиката p, сохраняющего минот по инфимума: p(sInf S) при условии, что p выполняется на всех элементах S, образует замыкатель.
LaTeX
$$$\\text{ofCompletePred}(p, hsinf) : \\text{ClosureOperator } \\alpha$, with $hsinf$ expressing preservation of infima and $p$ the closed predicate.$$
Lean4
/-- Define a closure operator from a predicate that's preserved under infima. -/
@[simps!]
def ofCompletePred (p : α → Prop) (hsinf : ∀ s, (∀ a ∈ s, p a) → p (sInf s)) : ClosureOperator α :=
ofPred (fun a ↦ ⨅ b : { b // a ≤ b ∧ p b }, b) p (fun a ↦ by simp +contextual)
(fun _ ↦ hsinf _ <| forall_mem_range.2 fun b ↦ b.2.2) (fun _ b hab hb ↦ iInf_le_of_le ⟨b, hab, hb⟩ le_rfl)
