English
If z ∈ σ_S(x) then the connected component of z in the complement of σ_A(x) is bounded.
Русский
Если z принадлежит σ_S(x), то связная компонента z в дополнении σ_A(x) ограничена.
LaTeX
$$z ∈ σ 𝕜 x ⇒ Bornology.IsBounded (connectedComponentIn (σ 𝕜 (x : A))ᶜ z)$$
Lean4
/-- Let `S` be a closed subalgebra of a Banach algebra `A`. If for `x : S` the complement of the
spectrum of `↑x : A` is connected, then `spectrum 𝕜 x = spectrum 𝕜 (x : A)`. -/
theorem spectrum_eq_of_isPreconnected_compl (h : IsPreconnected (σ 𝕜 (x : A))ᶜ) : σ 𝕜 x = σ 𝕜 (x : A) :=
by
nontriviality A
suffices σ 𝕜 x \ σ 𝕜 (x : A) = ∅ by
rw [spectrum_sUnion_connectedComponentIn, this]
simp
refine eq_empty_of_forall_notMem fun z hz ↦ NormedSpace.unbounded_univ 𝕜 𝕜 ?_
obtain ⟨hz, hz'⟩ := mem_diff _ |>.mp hz
have :=
(spectrum.isBounded (x : A)).union <| h.connectedComponentIn hz' ▸ spectrum_isBounded_connectedComponentIn S x hz
simpa
