spectrum_subset_unitary_of_mem_unitary

English

If u is a unitary element in A, then every spectral value of u lies on the unit circle in ℂ: σ_ℂ(u) ⊆ { z ∈ ℂ : |z| = 1 }. Equivalently, σ_ℂ(u) ⊆ U(1) in ℂ.

Русский

Если u — унитарный элемент в A, то все спектральные значения u лежат на единичной окружности в ℂ: σ_ℂ(u) ⊆ { z ∈ ℂ : |z| = 1 }. Эквивалентно: спектр u лежит в окружности единиц.

LaTeX

$$$$\sigma_{\mathbb{C}}(u) \subseteq \{ z \in \mathbb{C} : |z| = 1 \}.$$$$

Lean4

theorem spectrum_subset_unitary_of_mem_unitary {u : A} (hu : u ∈ unitary A) : spectrum ℂ u ⊆ unitary ℂ :=
  unitary_iff_isStarNormal_and_spectrum_subset_unitary.mp hu |>.right

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