norm_cfc_lt — Mathlib

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

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