instMetricSpace — Mathlib

English

The unit circle is endowed with a metric space structure inherited from the ambient complex plane, i.e., distance on Circle is induced from the Euclidean distance in ℂ.

Русский

Единичная окружность наделяется структурой метрического пространства, полученной как ограничение евклидовой метрики плоскости ℂ.

LaTeX

$$$$ d_{\\mathbb{S}^1}(x, y) = |x - y| \\quad (x,y \\in \\mathbb{S}^1). $$$$

Lean4

instance instMetricSpace : MetricSpace Circle :=
  Subtype.metricSpace

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