English
There is a constructor mk' that builds a closure operator from a function f with monotonicity and inflationary/idempotence-type data: f monotone, x ≤ f x, and f f x ≤ f x.
Русский
Существует конструктор mk', который строит оператор замыкания из функции f с монотонностью и данными, аналогичными инфляционности и идемпотентности: f монотонна, x ≤ f x, и f(f x) ≤ f x.
LaTeX
$$$mk'(f)(hf_1)(hf_2)(hf_3)$defines a ClosureOperator with toFun=f, monotone'=hf_1, le_closure'=hf_2, idempotent'\;x=(hf_3 x).$$$
Lean4
/-- Constructor for a closure operator using the weaker idempotency axiom: `f (f x) ≤ f x`. -/
@[simps]
def mk' (f : α → α) (hf₁ : Monotone f) (hf₂ : ∀ x, x ≤ f x) (hf₃ : ∀ x, f (f x) ≤ f x) : ClosureOperator α
where
toFun := f
monotone' := hf₁
le_closure' := hf₂
idempotent' x := (hf₃ x).antisymm (hf₁ (hf₂ x))
