English
Under the same setup as above, if c > 0 and ‖f(x)‖ < c for all x in the spectrum of a, then the image under cfc is strictly bounded: ‖cfc f a‖ < c.
Русский
При той же постановке, если c > 0 и для каждого x в спектре a выполняется ‖f(x)‖ < c, то ‖cfc f a‖ < c.
LaTeX
$$$0 < c \land \Big( \forall x \in \sigma 𝕜 a, \|f(x)\| < c \Big) \Rightarrow \|cfc f a\| < c$$$
Lean4
theorem norm_cfc_lt {f : 𝕜 → 𝕜} {a : A} {c : ℝ} (hc : 0 < c) (h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c) : ‖cfc f a‖ < c :=
by
obtain (_ | _) := subsingleton_or_nontrivial A
· simpa [Subsingleton.elim (cfc f a) 0]
· refine cfc_cases (‖·‖ < c) a f (by simpa) fun hf ha ↦ ?_
simp only [← cfc_apply f a, (IsGreatest.norm_cfc f a hf ha |>.lt_iff)]
rintro - ⟨x, hx, rfl⟩
exact h x hx