one_le_two

Mathlib.Algebra.Order.Monoid.NatCast

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

← MathLib Explorer

English

Under LE and AddLeftMono, 1 ≤ 2 holds.

Русский

При наличии LE и AddLeftMono выполняется 1 ≤ 2.

LaTeX

$$$1 \le 2$$$

Lean4

theorem one_le_two [LE α] [ZeroLEOneClass α] [AddLeftMono α] : (1 : α) ≤ 2 :=
  calc
    (1 : α) = 1 + 0 := (add_zero 1).symm
    _ ≤ 1 + 1 := (add_le_add_left zero_le_one _)
    _ = 2 := one_add_one_eq_two

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

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

Разделы

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

Аффилиация

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