diam_pos_iff

Mathlib.Topology.EMetricSpace.Diam

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

English

0 < diam(s) if and only if s is nontrivial (not subsingleton).

Русский

0 < diam(s) тогда и только тогда, когда s не является subsingleton.

LaTeX

$$0 < \operatorname{diam}(s) \iff s \text{ Nontrivial}$$

Lean4

theorem diam_pos_iff : 0 < diam s ↔ s.Nontrivial := by
  simp only [pos_iff_ne_zero, Ne, diam_eq_zero_iff, Set.not_subsingleton_iff]

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

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

Разделы

Аффилиация

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