diam_closure — Mathlib

English

For any set S in a metric space, the diameter of the closure equals the diameter of S.

Русский

Для множества S в метрическом пространстве диаметр замыкания равен диаметру S.

LaTeX

$$$\operatorname{Metric}.diam(\overline{S}) = \operatorname{Metric}.diam(S)$.$$

Lean4

@[simp]
theorem diam_closure {α : Type*} [PseudoMetricSpace α] (s : Set α) : Metric.diam (closure s) = diam s := by
  simp only [Metric.diam, EMetric.diam_closure]

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