nonneg

Mathlib.Algebra.Order.Star.Basic

URI: https://scilib.ai/kg/mathlib#IsStarProjection.nonneg

← MathLib Explorer

English

If x ≤ y and x is self-adjoint, then y is self-adjoint.

Русский

Если x ≤ y и x самосопряжён, то y самосопряжён.

LaTeX

$$$x \le y \land \star x = x \Rightarrow \star y = y$$$

Lean4

/-- A star projection is non-negative in a star-ordered ring. -/
theorem nonneg {p : R} (hp : IsStarProjection p) : 0 ≤ p :=
  hp.isIdempotentElem ▸ hp.isSelfAdjoint.mul_self_nonneg

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

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

Разделы

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

Аффилиация

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