map_le_map_of_map_star — Mathlib

English

Any star-ring homomorphism between star-ordered rings preserves order.

Русский

Любой гомоморфизм векторного кольца со звёздой между звёздно упорядоченными кольцами сохраняет порядок.

LaTeX

$$∀ x y, x ≤ y ⇒ f(x) ≤ f(y)$$

Lean4

theorem map_le_map_of_map_star (f : R →⋆ₙ+* S) {x y : R} (hxy : x ≤ y) : f x ≤ f y :=
  by
  rw [StarOrderedRing.le_iff] at hxy ⊢
  obtain ⟨p, hp, rfl⟩ := hxy
  refine ⟨f p, ?_, map_add f _ _⟩
  have hf : ∀ r, f (star r) = star (f r) := map_star _
  induction hp using AddSubmonoid.closure_induction
  all_goals aesop

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