norm_le_of_nonempty

Mathlib.Topology.ContinuousMap.Bounded.Normed

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

← MathLib Explorer

English

If α is nonempty, ‖f‖ ≤ M is equivalent to ∀ x, ‖f x‖ ≤ M.

Русский

Если α непусто, то ‖f‖ ≤ M эквивалентно ∀ x, ‖f(x)‖ ≤ M.

LaTeX

$$$‖f‖ ≤ M \\iff ∀ x, ‖f(x)‖ ≤ M$$$

Lean4

theorem norm_le_of_nonempty [Nonempty α] {f : α →ᵇ β} {M : ℝ} : ‖f‖ ≤ M ↔ ∀ x, ‖f x‖ ≤ M :=
  by
  simp_rw [norm_def, ← dist_zero_right]
  exact dist_le_iff_of_nonempty

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

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

Разделы

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

Аффилиация

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