conjugate_le_conjugate

Mathlib.Algebra.Order.Star.Basic

URI: https://scilib.ai/kg/mathlib#IsSelfAdjoint.conjugate_le_conjugate

← MathLib Explorer

English

If a ≤ b and c is self-adjoint, then c a c ≤ c b c.

Русский

Если a ≤ b и c самосопряжён, то c a c ≤ c b c.

LaTeX

$$$a \le b \land \text{IsSelfAdjoint}(c) \Rightarrow c a c \le c b c$$$

Lean4

protected theorem conjugate_le_conjugate {a b : R} (hab : a ≤ b) {c : R} (hc : IsSelfAdjoint c) :
    c * a * c ≤ c * b * c := by simpa only [hc.star_eq] using conjugate_le_conjugate hab c

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru