zero_le_one'

Mathlib.Algebra.Order.ZeroLEOne

URI: https://scilib.ai/kg/mathlib#zero_le_one'

← MathLib Explorer

English

Explicit version of 0 ≤ 1 in a structure with explicit type parameters.

Русский

Явная версия 0 ≤ 1 для структуры с явными параметрами типа.

LaTeX

$$$(0 : \alpha) \le 1$$$

Lean4

/-- `zero_le_one` with the type argument explicit. -/
theorem zero_le_one' (α) [Zero α] [One α] [LE α] [ZeroLEOneClass α] : (0 : α) ≤ 1 :=
  zero_le_one

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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