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