norm_image_zero_le

Mathlib.Analysis.Normed.Affine.ContinuousAffineMap

URI: https://scilib.ai/kg/mathlib#ContinuousAffineMap.norm_image_zero_le

English

The image of zero under an affine map is bounded by the norm of the map itself.

Русский

Изображение нуля аффинного отображения ограничено нормой отображения.

LaTeX

$$$$\|f(0)\| \leq \|f\|.$$$$

Lean4

theorem norm_image_zero_le : ‖f 0‖ ≤ ‖f‖ :=
  le_max_left _ _

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

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

Разделы

Аффилиация

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