closedBall_zero_eq — Mathlib

English

The closed ball of radius r around the origin is the set of x with sum of coordinate squares at most r^2: ∑_i x_i^2 ≤ r^2.

Русский

Закрытый шар радиуса r вокруг нуля; сумма квадратов координат не превосходит r^2: \sum_i x_i^2 ≤ r^2.

LaTeX

$$$\{ x : \mathbb{R}^n : \sum_i x_i^2 \le r^2 \}$$$

Lean4

theorem closedBall_zero_eq {n : Type*} [Fintype n] (r : ℝ) (hr : 0 ≤ r) :
    Metric.closedBall (0 : EuclideanSpace ℝ n) r = {x | ∑ i, x i ^ 2 ≤ r ^ 2} :=
  by
  ext
  simp_rw [mem_setOf, mem_closedBall_zero_iff, norm_eq, norm_eq_abs, sq_abs, sqrt_le_left hr]

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