norm_lt_iff_of_compactlySupported

English

For a compactly supported bounded continuous function f and a real M, with M > 0, we have ∥f∥ < M if and only if ∀ x, ∥f(x)∥ < M.

Русский

Для ограниченно поддерживаемой непрерывной функции f и числа M, если M > 0, тогда ∥f∥ < M тогда и только если для всех x: ∥f(x)∥ < M.

LaTeX

$$$\\|f\\| < M \\iff \\forall x : \\alpha, \\|f(x)\\| < M \\quad( M>0 )$$$

Lean4

theorem norm_lt_iff_of_compactlySupported {f : α →ᵇ γ} (h : f ∈ C_cb(α, γ)) {M : ℝ} (M0 : 0 < M) :
    ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M :=
  by
  refine ⟨fun hn x ↦ lt_of_le_of_lt (norm_coe_le_norm f x) hn, ?_⟩
  · obtain (he | he) := isEmpty_or_nonempty α
    · simpa
    · obtain ⟨x, hx⟩ := exist_norm_eq h
      exact fun h ↦ hx ▸ h x

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