English
There is a second constructor mk₂ that builds a closure operator from a function f, a basic inflation condition x ≤ f x, and a minimality condition: ∀ {x y}, x ≤ f y → f x ≤ f y.
Русский
Существует второй конструктор mk₂, который строит оператор замыкания из функции f, базового инфляционного условия x ≤ f x и минимальности: ∀ x,y, x ≤ f y → f x ≤ f y.
LaTeX
$$$mk_2(f)(hf)(hmin)$ defines a ClosureOperator with monotone' given by hf and idempotent' via hf, and le_closure' by hf.$$
Lean4
/-- Convenience constructor for a closure operator using the weaker minimality axiom:
`x ≤ f y → f x ≤ f y`, which is sometimes easier to prove in practice. -/
@[simps]
def mk₂ (f : α → α) (hf : ∀ x, x ≤ f x) (hmin : ∀ ⦃x y⦄, x ≤ f y → f x ≤ f y) : ClosureOperator α
where
toFun := f
monotone' _ y hxy := hmin (hxy.trans (hf y))
le_closure' := hf
idempotent' _ := (hmin le_rfl).antisymm (hf _)
