conjugate_lt_conjugate' — Mathlib

English

If a < b and c is regular, then conjugating by c on the other side preserves the inequality: c a c^* < c b c^*.

Русский

Если a < b и c регулярен, то конъюгирование по c с обеих сторон через сопряжение сохраняет неравенство: c a c^* < c b c^*.

LaTeX

$$$ a < b \Rightarrow IsRegular(c) \Rightarrow c a c^* < c b c^* $$$

Lean4

theorem conjugate_lt_conjugate' {a b : R} (hab : a < b) {c : R} (hc : IsRegular c) : c * a * star c < c * b * star c :=
  by simpa only [star_star] using conjugate_lt_conjugate hab hc.star

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