English
The boundary of the spectrum in a closed subalgebra is contained in the boundary of the ambient spectrum.
Русский
Граница спектра внутри подалгебры включена в границу спектра надмножества.
LaTeX
$$frontier (σ 𝕜 x) ⊆ frontier (σ 𝕜 (x : A))$$
Lean4
/-- If `S` is a closed subalgebra of a Banach algebra `A`, then for any `x : S`, the boundary of
the spectrum of `x` relative to `S` is a subset of the boundary of the spectrum of `↑x : A`
relative to `A`. -/
theorem frontier_subset_frontier : frontier (σ 𝕜 x) ⊆ frontier (σ 𝕜 (x : A)) :=
by
rw [frontier_eq_closure_inter_closure (s := σ 𝕜 (x : A)), (spectrum.isClosed (x : A)).closure_eq]
apply subset_inter (frontier_spectrum S x)
rw [frontier_eq_closure_inter_closure]
exact inter_subset_right |>.trans <| closure_mono <| compl_subset_compl.mpr <| spectrum.subset_subalgebra x
