norm_lt_iff_of_nonempty — Mathlib

English

If α is nonempty, then ‖f‖ < M is equivalent to ∀ x ∈ α, ‖f(x)‖ < M for any real M.

Русский

Если α непусто, то ‖f‖ < M эквивалентно ∀ x, ‖f(x)‖ < M.

LaTeX

$$$[Nonempty(\alpha)] \Rightarrow ( \|f\| < M \iff \forall x, \|f(x)\| < M )$$$

Lean4

theorem norm_lt_iff_of_nonempty [Nonempty α] {M : ℝ} : ‖f‖ < M ↔ ∀ x, ‖f x‖ < M :=
  @BoundedContinuousFunction.norm_lt_iff_of_nonempty_compact _ _ _ _ _ _ (mkOfCompact f) _

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