conjugate_lt_conjugate — Mathlib

English

Let a < b in a star-ordered ring and c be regular. Then conjugating by star c preserves the inequality: star c a c < star 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) : star c * a * c < star c * b * c :=
  by
  rw [(conjugate_le_conjugate hab.le _).lt_iff_ne, hc.right.ne_iff, hc.star.left.ne_iff]
  exact hab.ne

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