norm_lt_iff

Mathlib.Topology.ContinuousMap.Compact

URI: https://scilib.ai/kg/mathlib#ContinuousMap.norm_lt_iff

← MathLib Explorer

English

If M > 0, then ‖f‖ < M if and only if ∀ x ∈ α, ‖f(x)‖ < M.

Русский

Если M > 0, тогда ‖f‖ < M тогда и только тогда, когда ∀ x, ‖f(x)‖ < M.

LaTeX

$$$M>0 \Rightarrow ( \|f\| < M \iff \forall x\in \alpha, \|f(x)\| < M )$$$

Lean4

theorem norm_lt_iff {M : ℝ} (M0 : 0 < M) : ‖f‖ < M ↔ ∀ x, ‖f x‖ < M :=
  @BoundedContinuousFunction.norm_lt_iff_of_compact _ _ _ _ _ (mkOfCompact f) _ M0

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

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

Разделы

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

Аффилиация

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