English
Given an inflationary function f, a predicate p for closedness, and an accompanying minimality condition, construct a closure operator whose closed sets are precisely those satisfying p.
Русский
Задавая инфляционную функцию f, предикат p для замкнутости и соответствующее минимальное условие, построим оператор замыкания, чьи замкнутые множества совпадают с множествами, удовлетворяющими p.
LaTeX
$$$\ofPred(f,p,hf,hfp,hmin)$ defines a ClosureOperator with IsClosed := p and isClosed_iff given by hmin and hf.$$
Lean4
/-- Construct a closure operator from an inflationary function `f` and a "closedness" predicate `p`
witnessing minimality of `f x` among closed elements greater than `x`. -/
@[simps!]
def ofPred (f : α → α) (p : α → Prop) (hf : ∀ x, x ≤ f x) (hfp : ∀ x, p (f x)) (hmin : ∀ ⦃x y⦄, x ≤ y → p y → f x ≤ y) :
ClosureOperator α where
__ := mk₂ f hf fun _ y hxy => hmin hxy (hfp y)
IsClosed := p
isClosed_iff := ⟨fun hx ↦ (hmin le_rfl hx).antisymm <| hf _, fun hx ↦ hx ▸ hfp _⟩
