norm_lt_iff_of_nonempty_compactlySupported

English

If α is nonempty, then for any f ∈ C_cb(α, γ) and any real M, ∥f∥ < M iff ∀ x, ∥f(x)∥ < M.

Русский

Если α непусто, то для любого f ∈ C_cb(α, γ) и любого числа M, ∥f∥ < M эквивалентно ∀ x, ∥f(x)∥ < M.

LaTeX

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

Lean4

theorem norm_lt_iff_of_nonempty_compactlySupported [c : Nonempty α] {f : α →ᵇ γ} (h : f ∈ C_cb(α, γ)) {M : ℝ} :
    ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M := by
  obtain (hM | hM) := lt_or_ge 0 M
  · exact norm_lt_iff_of_compactlySupported h hM
  ·
    exact
      ⟨fun h ↦ False.elim <| (h.trans_le hM).not_ge (by positivity), fun h ↦
        False.elim <| (h (Classical.arbitrary α) |>.trans_le hM).not_ge (by positivity)⟩

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