zeroLEOneClass

Mathlib.Data.Num.ZNum

URI: https://scilib.ai/kg/mathlib#ZNum.zeroLEOneClass

English

Zero ≤ One holds in ZNum.

Русский

Ноль не больше единицы в ZNum.

LaTeX

$$$$0 \le 1.$$$$

Lean4

instance zeroLEOneClass : ZeroLEOneClass ZNum :=
  { zero_le_one := by decide }

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

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

Разделы

Аффилиация

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