Subsingleton

Mathlib.Data.List.Cycle

URI: https://scilib.ai/kg/mathlib#Cycle.Subsingleton

Lean4

/-- A `s : Cycle α` that is at most one element. -/
def Subsingleton (s : Cycle α) : Prop :=
  s.length ≤ 1

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

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

Разделы

Аффилиация

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