dist — Mathlib

English

In a finite-dimensional real inner product space, every closed ball is compact.

Русский

В конечномерном вещественном гильбертовом пространстве любая замкнутая сфера (шар) компактна.

LaTeX

$$IsCompact (closedBall x r)$$

Lean4

/-- If `x` and `y` are two points in a finite-dimensional space over `ℝ`, then `Euclidean.dist x y`
is the distance between these points in the metric defined by some inner product space structure on
`E`. -/
nonrec def dist (x y : E) : ℝ :=
  dist (toEuclidean x) (toEuclidean y)

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