instOrderHomClass — Mathlib

English

Positive linear maps carry an order-homomorphism structure; i.e., they preserve order relations.

Русский

Положительные линейные отображения образуют структуру гомоморфизма порядка и сохраняют отношения порядка.

LaTeX

$$$\\text{OrderHomClass }(F',E'_1,E'_2)$$$

Lean4

instance : OrderHomClass (E₁ →ₚ[R] E₂) E₁ E₂ where map_rel f := fun {_ _} hab => f.monotone' hab

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