nnnorm_cfc_nnreal_lt — Mathlib

English

If ∀ x ∈ spectrum a, f x < c (for NNReal), then the NN-norm of cfcₙ f a is < c.

Русский

Если ∀ x в спектре a, f x < c (NNReal), то nnnorm cfcₙ f a < c.

LaTeX

$$$\forall x \in \sigma a,\; f x < c \Rightarrow \|cfc f a\|_+ < c$$$

Lean4

theorem nnnorm_cfc_nnreal_lt {f : ℝ≥0 → ℝ≥0} {a : A} {c : ℝ≥0} (hc : 0 < c) (h : ∀ x ∈ σ ℝ≥0 a, f x < c) :
    ‖cfc f a‖₊ < c := by
  obtain (_ | _) := subsingleton_or_nontrivial A
  · rw [Subsingleton.elim (cfc f a) 0]
    simpa
  · refine cfc_cases (‖·‖₊ < c) a f (by simpa) fun hf ha ↦ ?_
    simp only [← cfc_apply f a, (IsGreatest.nnnorm_cfc_nnreal f a hf ha |>.lt_iff)]
    rintro - ⟨x, hx, rfl⟩
    exact h x hx

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