instOrderHomClass — Mathlib

English

If α has a preorder, then ClosureOperator α carries the structure of an OrderHomClass to α → α; i.e., each closure operator acts as an order-preserving endomorphism on α.

Русский

Если у α есть порядок, то ClosureOperator α обладает структурой OrderHomClass к α → α; то есть каждый оператор замыкания действует как монотонное отображение α в α.

LaTeX

$$$\\text{OrderHomClass}(\\ClosureOperator(\\alpha), \\alpha, \\alpha).$$$

Lean4

instance [Preorder α] : OrderHomClass (ClosureOperator α) α α where map_rel f _ _ h := f.mono h

Похожие утверждения