English
Let f be a bounded continuous function on α with compact support; then the sup norm of f is attained at some point x ∈ α, i.e. there exists x with ∥f(x)∥ = ∥f∥.
Русский
Пусть f: α → γ является ограниченно непрерывной функцией с компактной опорой; тогда норма f достигается в некоторой точке x ∈ α: существует x such that ∥f(x)∥ = ∥f∥.
LaTeX
$$$\\exists x : \\alpha, \\|f(x)\\| = \\|f\\|$$$
Lean4
theorem exist_norm_eq [c : Nonempty α] {f : α →ᵇ γ} (h : f ∈ C_cb(α, γ)) : ∃ (x : α), ‖f x‖ = ‖f‖ :=
by
by_cases hs : (tsupport f).Nonempty
· obtain ⟨x, _, hmax⟩ := mem_compactlySupported.mp h |>.exists_isMaxOn hs <| (map_continuous f).norm.continuousOn
refine ⟨x, le_antisymm (norm_coe_le_norm f x) (norm_le (norm_nonneg _) |>.mpr fun y ↦ ?_)⟩
by_cases hy : y ∈ tsupport f
· exact hmax hy
· simp [image_eq_zero_of_notMem_tsupport hy]
· suffices f = 0 by simp [this]
rwa [not_nonempty_iff_eq_empty, tsupport_eq_empty_iff, ← coe_zero, ← DFunLike.ext'_iff] at hs
