factZeroLeOne

Mathlib.Algebra.Order.ZeroLEOne

URI: https://scilib.ai/kg/mathlib#ZeroLEOneClass.factZeroLeOne

English

In any ordered type with zero and one, zero is less than or equal to one.

Русский

В любом упорядоченном типе с нулём и единицей ноль не больше единицы.

LaTeX

$$(0 ≤ 1)$$

Lean4

instance factZeroLeOne [Zero α] [One α] [LE α] [ZeroLEOneClass α] : Fact ((0 : α) ≤ 1) where out := zero_le_one

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

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

Разделы

Аффилиация

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