subset_closedBall_norm_mul — Mathlib

English

For any a, the spectrum σ(a) is contained in the closed ball centered at 0 with radius ‖a‖·‖1‖ in 𝕜.

Русский

Для любого a спектр σ(a) содержится в замкнутом шаре centered at 0 радиуса ‖a‖·‖1‖ в 𝕜.

LaTeX

$$$\\sigma_{\\mathbb{K}}(a) \\subseteq \\overline{B}_{\\mathbb{K}}\\bigl(0, \\|a\\|\\cdot \\|1\\|\\bigr).$$$

Lean4

theorem subset_closedBall_norm_mul (a : A) : σ a ⊆ Metric.closedBall (0 : 𝕜) (‖a‖ * ‖(1 : A)‖) := fun k hk => by
  simp [norm_le_norm_mul_of_mem hk]

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