norm_eq — Mathlib

English

The norm of f equals the least upper bound of the pointwise norms: ‖f‖ = sup_{x∈α} ‖f(x)‖ (as a least upper bound).

Русский

Норма функции равна наименьшему верхнему пределу по точкам: ‖f‖ = sup_{x∈α} ‖f(x)‖.

LaTeX

$$$‖f‖ = \\sup_{x\\in\\alpha} ‖f(x)‖$$$

Lean4

/-- The norm of a bounded continuous function is the supremum of `‖f x‖`.
We use `sInf` to ensure that the definition works if `α` has no elements. -/
theorem norm_eq (f : α →ᵇ β) : ‖f‖ = sInf {C : ℝ | 0 ≤ C ∧ ∀ x : α, ‖f x‖ ≤ C} := by
  simp [norm_def, BoundedContinuousFunction.dist_eq]

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