le_of_mul_eq_left — Mathlib

English

Let p and q be star projections in a star-ordered ring with no unit necessarily assumed, and suppose p q = p. Then p is less than or equal to q.

Русский

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

LaTeX

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

Lean4

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

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