iSup_eigenspace_toLin'_diagonal_eq_top

English

For a diagonal operator with respect to a basis, the iSup of eigen spaces equals the top subspace.

Русский

Для диагонального оператора относительно базиса, iSup эйгенпространств даёт верхнее подпространство.

LaTeX

$$$iSup_{\\mu} \\; \\mathrm{eigenspace}((\\text{diagonal } d).toLin' b b)\\, \\mu = \\top$$$

Lean4

@[simp]
theorem iSup_eigenspace_toLin'_diagonal_eq_top : ⨆ μ, eigenspace (diagonal d).toLin' μ = ⊤ :=
  iSup_eigenspace_toLin_diagonal_eq_top d <| Pi.basisFun R n

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