Empty

Mathlib.Data.Ordmap.Ordset

URI: https://scilib.ai/kg/mathlib#Ordset.Empty

English

Definition: Empty( s ) holds iff s equals the empty Ordset.

Русский

Определение: Empty(s) истинно тогда, когда s равно пустому Ordset.

LaTeX

$$Empty(s) := (s = ∅)$$

Lean4

/-- O(1). Is the set empty? -/
def Empty (s : Ordset α) : Prop :=
  s = ∅

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

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

Разделы

Аффилиация

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