length_eq_zero

Mathlib.Order.RelSeries

URI: https://scilib.ai/kg/mathlib#RelSeries.length_eq_zero

English

The length equals zero iff the set is subsingleton.

Русский

Длина равна нулю тогда, когда множество элементов является subsingleton.

LaTeX

$$s.length = 0 \\Leftrightarrow {x | x ∈ s}.Subsingleton$$

Lean4

theorem length_eq_zero [r.IsIrrefl] : s.length = 0 ↔ {x | x ∈ s}.Subsingleton := by
  rw [← not_ne_iff, length_ne_zero, Set.not_nontrivial_iff]

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

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

Разделы

Аффилиация

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