one_lt_two — Mathlib

English

Let α be a type with an AddMonoidWithOne and a PartialOrder, such that addition on the left is strictly monotone. Then (1 : α) < (2 : α).

Русский

Пусть α имеет структуру AddMonoidWithOne и частичный порядок, и слева сложение действует строго монотонно. Тогда (1 : α) < (2 : α).

LaTeX

$$$(1 : \alpha) < (2 : \alpha)$$$

Lean4

theorem one_lt_two [AddLeftStrictMono α] : (1 : α) < 2 :=
  by
  rw [← one_add_one_eq_two]
  exact lt_add_one _

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