absorbent_closedBall — Mathlib

English

Closed balls of a seminorm are convex sets.

Русский

Замкнутые шары семинормы выпуклы.

LaTeX

$$Convex ℝ (closedBall p x r)$$

Lean4

/-- Seminorm-balls containing the origin are absorbent. -/
protected theorem absorbent_closedBall (hpr : p x < r) : Absorbent 𝕜 (closedBall p x r) :=
  by
  refine (p.absorbent_closedBall_zero <| sub_pos.2 hpr).mono fun y hy => ?_
  rw [p.mem_closedBall_zero] at hy
  exact p.mem_closedBall.2 ((map_sub_le_add p _ _).trans <| add_le_of_le_sub_right hy)

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