diam_eq_zero_iff

Mathlib.Topology.EMetricSpace.Diam

URI: https://scilib.ai/kg/mathlib#EMetric.diam_eq_zero_iff

← MathLib Explorer

English

For EMetrics, diam(s) = 0 if and only if s is subsingleton.

Русский

Для эмэтик diam(s) = 0 тогда и только тогда, когда s — subsingleton.

LaTeX

$$\operatorname{diam}(s) = 0 \iff s \text{ subsingleton}$$

Lean4

theorem diam_eq_zero_iff : diam s = 0 ↔ s.Subsingleton :=
  ⟨fun h _x hx _y hy => edist_le_zero.1 <| h ▸ edist_le_diam_of_mem hx hy, diam_subsingleton⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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