bddAbove_range_norm_comp

Mathlib.Topology.ContinuousMap.Bounded.Normed

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

English

The range of the norm of f is bounded above; in other words, {‖f(x)‖ : x ∈ α} is bounded above by some real M.

Русский

Образ множества {‖f(x)‖ : x ∈ α} ограничен сверху некоторой константой M ∈ ℝ.

LaTeX

$$$\exists M\in \mathbb{R}\,\forall x\in α,\ \|f(x)\| ≤ M$$$

Lean4

theorem bddAbove_range_norm_comp : BddAbove <| Set.range <| norm ∘ f :=
  (@isBounded_range _ _ _ _ f.normComp).bddAbove

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

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

Разделы

Аффилиация

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