nnnorm_lt_iff — Mathlib

English

For any M ∈ ℝ≥0, if 0 < M then ‖f‖₊ < M iff ∀ x, ‖f(x)‖₊ < M.

Русский

Для любого M ∈ ℝ≥0, если 0 < M, то ‖f‖₊ < M тогда и только тогда, когда ∀ x, ‖f(x)‖₊ < M.

LaTeX

$$$M \in \mathbb{R}_{\ge 0},\; M>0 \Rightarrow ( \|f\|_{+} < M \iff \forall x, \|f(x)\|_{+} < M )$$$

Lean4

theorem nnnorm_lt_iff {M : ℝ≥0} (M0 : 0 < M) : ‖f‖₊ < M ↔ ∀ x : α, ‖f x‖₊ < M :=
  f.norm_lt_iff M0

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