coe_mk — Mathlib

English

The metric sphere with center c and radius r is exactly the set of points x at distance r from c: { x ∈ P | dist(x,c) = r }.

Русский

Метрическая сфера с центром c и радиусом r есть ровно множество точек x, расстояние от которых до c равно r: { x ∈ P | dist(x,c) = r }.

LaTeX

$$$$ \operatorname{Metric.sphere}(c,r) = \{ x \in P \mid \operatorname{dist}(x,c) = r \}. $$$$

Lean4

@[simp]
theorem coe_mk (c : P) (r : ℝ) : ↑(⟨c, r⟩ : Sphere P) = Metric.sphere c r :=
  rfl

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