isUniformEmbedding_of_bound

Mathlib.Analysis.Normed.Operator.ContinuousLinearMap

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.isUniformEmbedding_of_bound

← MathLib Explorer

English

Same as above: the mkContinuous map evaluated at x equals f x.

Русский

То же самое: mkContinuous(x) = f x.

LaTeX

$$$(f.mkContinuous C h) x = f x$$$

Lean4

theorem isUniformEmbedding_of_bound {K : ℝ≥0} (hf : ∀ x, ‖x‖ ≤ K * ‖f x‖) : IsUniformEmbedding f :=
  (AddMonoidHomClass.antilipschitz_of_bound f hf).isUniformEmbedding f.uniformContinuous

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

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

Разделы

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

Аффилиация

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