disk — Mathlib

English

The n-disk is the set of points in Euclidean space ℝ^n whose norm is at most 1, endowed with the subspace topology.

Русский

n-диск – множество точек в Евклидовом пространстве ℝ^n, нормы которых не превосходит 1, с вложенной топологией.

LaTeX

$$$D^n = \\{ x \\in \\mathbb{R}^n : \\|x\\| \\le 1 \\}. $$$

Lean4

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

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