absorbent_closedBall_zero — Mathlib

English

Negation preserves membership in closed balls: -x ∈ closedBall p 0 r iff x ∈ closedBall p 0 r.

Русский

Негирование сохраняет принадлежность к замкнутому шару: -x ∈ closedBall p 0 r ⇔ x ∈ closedBall p 0 r.

LaTeX

$$$-x \in closedBall\ p\ 0\ r \iff x \in closedBall\ p\ 0\ r$$$

Lean4

/-- Closed seminorm-balls at the origin are absorbent. -/
protected theorem absorbent_closedBall_zero (hr : 0 < r) : Absorbent 𝕜 (closedBall p (0 : E) r) :=
  (p.absorbent_ball_zero hr).mono (p.ball_subset_closedBall _ _)

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