le_of_mul_eq_right — Mathlib

English

Let p and q be star projections in a star-ordered ring, and suppose q p = p. Then p ≤ q.

Русский

Пусть p и q — звездные проекции в звездоупорядоченном кольце; если q p = p, то p ≤ q.

LaTeX

$$$$ \forall p,q \in R:\; P(p) \land P(q) \land q p = p \Rightarrow p \le q $$$$

Lean4

/-- A star projection `p` is less than or equal to a star projection `q` when `q * p = p`. -/
theorem le_of_mul_eq_right (hp : IsStarProjection p) (hq : IsStarProjection q) (hpq : q * p = p) : p ≤ q :=
  sub_nonneg.mp (hp.sub_of_mul_eq_right hq hpq).nonneg

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