diam_subsingleton

Mathlib.Topology.MetricSpace.Bounded

URI: https://scilib.ai/kg/mathlib#Metric.diam_subsingleton

English

If s is a subsingleton, then diam(s) = 0.

Русский

Если s состоит из одного элемента (подмножество с одним элементом), то diam(s) = 0.

LaTeX

$$$|s| \\le 1 \\Rightarrow \\operatorname{diam}(s) = 0$$$

Lean4

theorem diam_subsingleton (hs : s.Subsingleton) : diam s = 0 := by
  simp only [diam, EMetric.diam_subsingleton hs, ENNReal.toReal_zero]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru