closedBall_bot — Mathlib

English

For each radius r, the origin-centered ball p.ball 0 r is a balanced set in the underlying field: it is closed under scalar multiplication by scalars of modulus at most 1.

Русский

Для каждого радиуса r шар p.ball 0 r, сосредоточенный в начале координат, является сбалансированным множеством: если |λ| ≤ 1 и y ∈ ball p 0 r, то λ y ∈ ball p 0 r.

LaTeX

$$Balanced 𝕜 (ball p 0 r)$$

Lean4

@[simp]
theorem closedBall_bot {r : ℝ} (x : E) (hr : 0 < r) : closedBall (⊥ : Seminorm 𝕜 E) x r = Set.univ :=
  closedBall_zero' x hr

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