le_egauge_ball_one

Mathlib.Analysis.Convex.EGauge

URI: https://scilib.ai/kg/mathlib#le_egauge_ball_one

English

For every x, ||x|| ≤ egauge 𝕜 (ball 0 1) x.

Русский

Для любого x выполняется: ||x|| ≤ egauge 𝕜 (ball 0 1) x.

LaTeX

$$$\\forall x:\\; \\|x\\|_{e} \\le \\operatorname{egauge}_{\\mathbb{k}}(\\mathsf{ball}\\ 0\\ 1, x).$$$

Lean4

theorem le_egauge_ball_one (x : E) : ‖x‖ₑ ≤ egauge 𝕜 (ball 0 1) x := by simpa using div_le_egauge_ball 𝕜 1 x

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

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

Разделы

Аффилиация

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