dist_le_two_norm

Mathlib.Topology.ContinuousMap.Bounded.Normed

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

← MathLib Explorer

English

For any f ∈ α →ᵇ β, and x,y ∈ α, dist (f x) (f y) ≤ 2‖f‖.

Русский

Для любой f и точек x,y выполняется dist (f x) (f y) ≤ 2‖f‖.

LaTeX

$$$\\mathrm{dist}(f(x),f(y)) \\le 2 \\|f\\|$$$

Lean4

/-- Distance between the images of any two points is at most twice the norm of the function. -/
theorem dist_le_two_norm (x y : α) : dist (f x) (f y) ≤ 2 * ‖f‖ :=
  dist_le_two_norm' f.norm_coe_le_norm x y

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

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

Разделы

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

Аффилиация

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