norm_coe_le_norm

Mathlib.Topology.ContinuousMap.Bounded.Normed

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

← MathLib Explorer

English

For any f ∈ α →ᵇ β and x ∈ α, the pointwise value obeys ‖f(x)‖ ≤ ‖f‖.

Русский

Для любой функции f и элемента x выполняется ‖f(x)‖ ≤ ‖f‖.

LaTeX

$$$‖f(x)‖ \\le ‖f‖$$$

Lean4

theorem norm_coe_le_norm (x : α) : ‖f x‖ ≤ ‖f‖ :=
  calc
    ‖f x‖ = dist (f x) ((0 : α →ᵇ β) x) := by simp [dist_zero_right]
    _ ≤ ‖f‖ := dist_coe_le_dist _

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

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

Разделы

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

Аффилиация

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