of_nonneg

Mathlib.Algebra.Order.Star.Basic

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

English

If x ≥ 0, then x is self-adjoint (i.e., star x = x).

Русский

Если x ≥ 0, то x самоадъюнктно (star x = x).

LaTeX

$$$0 \le x \Rightarrow \star x = x$$$

Lean4

@[aesop 10% apply]
theorem of_nonneg {x : R} (hx : 0 ≤ x) : IsSelfAdjoint x :=
  .mono hx <| .zero R

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

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

Разделы

Аффилиация

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