instZeroLEOneClass

Mathlib.Data.Nat.PartENat

URI: https://scilib.ai/kg/mathlib#PartENat.instZeroLEOneClass

English

In PartENat, zero is less than or equal to one.

Русский

В PartENat ноль не выше единицы.

LaTeX

$$$ 0 \le 1 $$$

Lean4

instance : ZeroLEOneClass PartENat where zero_le_one := bot_le

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

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

Разделы

Аффилиация

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