zero_lt_one

Mathlib.Algebra.Order.ZeroLEOne

URI: https://scilib.ai/kg/mathlib#zero_lt_one

English

In a structure with 0 and 1, and appropriate order, 0 < 1.

Русский

В структуре с 0 и 1 и подходящим порядком 0 < 1.

LaTeX

$$$0 < 1$$$

Lean4

/-- See `zero_lt_one'` for a version with the type explicit. -/
@[simp]
theorem zero_lt_one : (0 : α) < 1 :=
  zero_le_one.lt_of_ne (NeZero.ne' 1)

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

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

Разделы

Аффилиация

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