ball — Mathlib

English

The n-ball is the set of points in ℝ^n whose norm is strictly less than 1, endowed with the subspace topology.

Русский

n-мяч — множество точек в ℝ^n с нормой строго меньше 1, с вложенной топологией.

LaTeX

$$$B^n = \\{ x \\in \\mathbb{R}^n : \\|x\\| < 1 \\}. $$$

Lean4

/-- The `n`-ball is the set of points in ℝⁿ whose norm is strictly less than `1`,
endowed with the subspace topology. -/
noncomputable def ball (n : ℕ) : TopCat.{u} :=
  TopCat.of <| ULift <| Metric.ball (0 : EuclideanSpace ℝ (Fin n)) 1

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