gauge_unit_ball

Mathlib.Analysis.Convex.Gauge

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

English

The unit ball for the gauge is the set of all x with gauge x < 1.

Русский

Единичный шар по gauge — множество всех x с gauge x < 1.

LaTeX

$$$$ gauge\\ unit\\ ball\\, 0\\ 1 = \\{x\\,|\\ gauge x < 1\\}. $$$$

Lean4

theorem gauge_unit_ball (x : E) : gauge (ball (0 : E) 1) x = ‖x‖ := by
  rw [← ball_normSeminorm ℝ, Seminorm.gauge_ball, coe_normSeminorm]

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

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

Разделы

Аффилиация

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