zero_lt_two

Mathlib.Algebra.Order.Monoid.NatCast

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

English

Under the given assumptions, 0 < 2.

Русский

При данных предпосылках 0 < 2.

LaTeX

$$$0 < 2$$$

Lean4

/-- See `zero_lt_two'` for a version with the type explicit. -/
@[simp]
theorem zero_lt_two : (0 : α) < 2 :=
  zero_lt_one.trans_le one_le_two

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

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

Разделы

Аффилиация

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