norm_le

Mathlib.Topology.ContinuousMap.Bounded.Normed

URI: https://scilib.ai/kg/mathlib#BoundedContinuousFunction.norm_le

← MathLib Explorer

English

The norm of the constant map const α b is at most ‖b‖.

Русский

Норма константной функции const α b не превышает ‖b‖.

LaTeX

$$$\\|const\\,\\alpha b\\| \\le \\|b\\|$$$

Lean4

/-- The norm of a function is controlled by the supremum of the pointwise norms. -/
theorem norm_le (C0 : (0 : ℝ) ≤ C) : ‖f‖ ≤ C ↔ ∀ x : α, ‖f x‖ ≤ C := by simpa using @dist_le _ _ _ _ f 0 _ C0

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru