English
Boundary behavior of spectrum in S mirrors the above frontier relations with ambient A.
Русский
Граничное поведение спектра в S следует из ранее указанных границ и вложений в A.
LaTeX
$$frontier_spectrum S x$$
Lean4
/-- Let `S` be a closed subalgebra of a Banach algebra `A`, and let `x : S`. If `z` is in the
spectrum of `x`, then the connected component of `z` in the complement of the spectrum of `↑x : A`
is bounded (or else `z` actually belongs to the spectrum of `↑x : A`). -/
theorem spectrum_isBounded_connectedComponentIn {z : 𝕜} (hz : z ∈ σ 𝕜 x) :
Bornology.IsBounded (connectedComponentIn (σ 𝕜 (x : A))ᶜ z) :=
by
by_cases hz' : z ∈ σ 𝕜 (x : A)
· simp [connectedComponentIn_eq_empty (show z ∉ (σ 𝕜 (x : A))ᶜ from not_not.mpr hz')]
· have : CompleteSpace S := hS.completeSpace_coe
suffices connectedComponentIn (σ 𝕜 (x : A))ᶜ z ⊆ σ 𝕜 x from spectrum.isBounded x |>.subset this
rw [spectrum_sUnion_connectedComponentIn S]
exact subset_biUnion_of_mem (mem_diff_of_mem hz hz') |>.trans subset_union_right
