lt_one_add — Mathlib

English

For any α with One, AddZeroClass, PartialOrder and ZeroLEOneClass and AddLeftMono, a < a + 1.

Русский

Для любого α c единицей, AddZeroClass, частично упорядоченной структурой и ZeroLEOneClass и AddLeftMono выполняется a < a + 1.

LaTeX

$$$a < a+1$$$

Lean4

theorem lt_one_add [One α] [AddZeroClass α] [PartialOrder α] [ZeroLEOneClass α] [NeZero (1 : α)] [AddRightStrictMono α]
    (a : α) : a < 1 + a :=
  lt_add_of_pos_left _ zero_lt_one

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