eigenvalues₀_antitone — Mathlib

English

The eigenvalues of a Hermitian matrix, as listed by eigenvalues₀, form a nonincreasing sequence with respect to the natural order.

Русский

Собственные значения эрмитовой матрицы, перечисленные через eigenvalues₀, образуют неубывающую последовательность по естественному порядку (невозрастающую).

LaTeX

$$$\text{If } h_A \text{ is Hermitian, then } h_A.\text{eigenvalues}_0 \text{ is Antitone.}$$$

Lean4

theorem eigenvalues₀_antitone : Antitone hA.eigenvalues₀ :=
  LinearMap.IsSymmetric.eigenvalues_antitone ..

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