gaugeSeminorm — Mathlib

English

The gaugeSeminorm ball 0 1 equals the unit ball for p.

Русский

Мяч gaugeSeminorm в точке 0 радиуса 1 равен единичному шару для p.

LaTeX

$$$$ (gaugeSeminorm hs₀ hs₁ hs₂).ball\\ 0\\ 1 = s, $$$$

Lean4

/-- `gauge s` as a seminorm when `s` is balanced, convex and absorbent. -/
@[simps!]
def gaugeSeminorm (hs₀ : Balanced 𝕜 s) (hs₁ : Convex ℝ s) (hs₂ : Absorbent ℝ s) : Seminorm 𝕜 E :=
  Seminorm.of (gauge s) (gauge_add_le hs₁ hs₂) (gauge_smul hs₀)

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