apply_le_norm

Mathlib.Topology.ContinuousMap.Bounded.Normed

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

English

For f ∈ α →ᵇ ℝ and x ∈ α, f(x) ≤ ‖f‖.

Русский

Для f ∈ α →ᵇ ℝ и x ∈ α выполнено f(x) ≤ ‖f‖.

LaTeX

$$$f(x) \\le \|f\\|$$$

Lean4

theorem apply_le_norm (f : α →ᵇ ℝ) (x : α) : f x ≤ ‖f‖ :=
  (abs_le.mp (norm_coe_le_norm f x)).2

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

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

Разделы

Аффилиация

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