diam_pos_iff'

Mathlib.Topology.EMetricSpace.Diam

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

English

0 < diam(s) iff ∃ x ∈ s, ∃ y ∈ s, x ≠ y.

Русский

0 < diam(s) если и только если существуют x,y ∈ s с x ≠ y.

LaTeX

$$0 < \operatorname{diam}(s) \iff \exists x \in s, \exists y \in s, x \neq y$$

Lean4

theorem diam_pos_iff' : 0 < diam s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y := by simp only [diam_pos_iff, Set.Nontrivial]

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

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

Разделы

Аффилиация

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