instOrderHomClass — Mathlib

English

If F is an order isomorphism between star-ordered rings, then x ≤ y holds iff F(x) ≤ F(y).

Русский

Если F — отображение-переводчик порядка между звёздно упорядоченными кольцами, то x ≤ y тогда и только тогда, когда F(x) ≤ F(y).

LaTeX

$$$ x \le y \iff F(x) \le F(y) $$$

Lean4

instance (priority := 100) instOrderHomClass [FunLike F R S] [NonUnitalSemiring R] [StarRing R] [StarOrderedRing R]
    [NonUnitalSemiring S] [StarRing S] [StarOrderedRing S] [NonUnitalRingHomClass F R S]
    [NonUnitalStarRingHomClass F R S] : OrderHomClass F R S where map_rel f := (f : R →⋆ₙ+* S).map_le_map_of_map_star

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