one_le_two'

Mathlib.Algebra.Order.Monoid.NatCast

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

← MathLib Explorer

English

A variant stating 1 ≤ 2 in a broader setting.

Русский

Вариант утверждения 1 ≤ 2 в более общем контексте.

LaTeX

$$$1 \le 2$$$

Lean4

theorem one_le_two' [LE α] [ZeroLEOneClass α] [AddRightMono α] : (1 : α) ≤ 2 :=
  calc
    (1 : α) = 0 + 1 := (zero_add 1).symm
    _ ≤ 1 + 1 := (add_le_add_right zero_le_one _)
    _ = 2 := one_add_one_eq_two

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

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

Разделы

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

Аффилиация

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