instCoeSphereSet — Mathlib

English

There is a natural way to regard a sphere as a subset of the ambient space: a sphere is the set of points at distance r from its center.

Русский

Существует естественное отображение сферы в множество пространства: сфера — это множество точек на фиксированном расстоянии от центра.

LaTeX

$$$\text{Sphere}(P) \ni s \mapsto\{ x\in P : \operatorname{dist}(x, s.center)=s.radius \}$$$

Lean4

instance : Coe (Sphere P) (Set P) :=
  ⟨fun s => Metric.sphere s.center s.radius⟩

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