ball_zero_eq — Mathlib

English

The ball centered at the origin with radius r consists of all x such that the sum of squares of coordinates is less than r^2: ∑_i x_i^2 < r^2.

Русский

Шар с центром в начале координат и радиусом r состоит из всех x, для которых сумма квадратов координат меньше r^2: \sum_i x_i^2 < r^2.

LaTeX

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

Lean4

theorem ball_zero_eq {n : Type*} [Fintype n] (r : ℝ) (hr : 0 ≤ r) :
    Metric.ball (0 : EuclideanSpace ℝ n) r = {x | ∑ i, x i ^ 2 < r ^ 2} :=
  by
  ext x
  have : (0 : ℝ) ≤ ∑ i, x i ^ 2 := Finset.sum_nonneg fun _ _ => sq_nonneg _
  simp_rw [mem_setOf, mem_ball_zero_iff, norm_eq, norm_eq_abs, sq_abs, sqrt_lt this hr]

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