gaugeSeminorm_ball — Mathlib

English

The gauge_ball theorem asserts that the gauge of the ball for a seminorm p equals p itself.

Русский

Теорема gauge_ball утверждает, что gauge_ball для семинорм равна самой семинорме p.

LaTeX

$$$$ \\text{Seminorm.gauge\_ball}(p) \\;:\\; gauge(p.ball\\,0\\,1) = p. $$$$

Lean4

theorem gaugeSeminorm_ball (p : Seminorm ℝ E) :
    gaugeSeminorm (p.balanced_ball_zero 1) (p.convex_ball 0 1) (p.absorbent_ball_zero zero_lt_one) = p :=
  DFunLike.coe_injective p.gauge_ball

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