diam_nonneg

Mathlib.Topology.MetricSpace.Bounded

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

English

Let s be a subset of a pseudometric space. Then the diameter of s is nonnegative: 0 ≤ diam(s).

Русский

Пусть s — подмножество псевдометрического пространства. Тогда диаметр s неотрицателен: 0 ≤ diam(s).

LaTeX

$$$0 \\le \\operatorname{diam}(s)$$$

Lean4

/-- The diameter of a set is always nonnegative -/
theorem diam_nonneg : 0 ≤ diam s :=
  ENNReal.toReal_nonneg

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

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

Разделы

Аффилиация

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