instOrderIsoClass — Mathlib

English

If F is an equivalence of star rings, then it induces an order isomorphism between the underlying ordered rings.

Русский

Если F — эквивалентность звёздных колец, то она порождает потому и отображение порядка между базовыми упорядоченными кольцами.

LaTeX

$$∀ F, R, S, [conditions], OrderIsoClass F R S$$

Lean4

instance (priority := 100) instOrderIsoClass [EquivLike F R S] [StarRingEquivClass F R S] : OrderIsoClass F R S where
  map_le_map_iff f x
    y := by
    refine ⟨fun h ↦ ?_, map_rel f⟩
    let f_inv : S →⋆ₙ+* R := (f : R ≃⋆+* S).symm
    have f_inv_f (r : R) : f_inv (f r) = r := EquivLike.inv_apply_apply f r
    rw [← f_inv_f x, ← f_inv_f y]
    exact NonUnitalStarRingHom.map_le_map_of_map_star f_inv h

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