absorbent_ball — Mathlib

English

A seminorm is convex on E with respect to the scalar field; more precisely, the map p is a convex functional on E over the reals.

Русский

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

LaTeX

$$ConvexOn ℝ univ p$$

Lean4

/-- Seminorm-balls containing the origin are absorbent. -/
protected theorem absorbent_ball (hpr : p x < r) : Absorbent 𝕜 (ball p x r) :=
  by
  refine (p.absorbent_ball_zero <| sub_pos.2 hpr).mono fun y hy => ?_
  rw [p.mem_ball_zero] at hy
  exact p.mem_ball.2 ((map_sub_le_add p _ _).trans_lt <| add_lt_of_lt_sub_right hy)

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