Mathlib.Algebra.Order.Monoid.NatCast

lt_add_one theorem

 [One α] [AddZeroClass α] [PartialOrder α] [ZeroLEOneClass α] [NeZero (1 : α)] [AddLeftStrictMono α] (a : α) : a < a + 1

Full source

lemma lt_add_one [One α] [AddZeroClass α] [PartialOrder α] [ZeroLEOneClass α]
    [NeZero (1 : α)] [AddLeftStrictMono α] (a : α) : a < a + 1 :=
  lt_add_of_pos_right _ zero_lt_one

Strict inequality under adding one: $a < a + 1$

Informal description

Let $\alpha$ be a type with a partial order, equipped with a zero element, a one element, and an addition operation such that: 1. $0 \leq 1$ (ZeroLEOneClass) 2. $1 \neq 0$ (NeZero) 3. Addition is strictly monotone on the left (AddLeftStrictMono) Then for any element $a \in \alpha$, we have $a < a + 1$.

lt_one_add theorem

 [One α] [AddZeroClass α] [PartialOrder α] [ZeroLEOneClass α] [NeZero (1 : α)] [AddRightStrictMono α] (a : α) :
  a < 1 + a

Full source

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

Strict inequality under right addition of one in ordered monoids

Informal description

Let $\alpha$ be a type with a partial order, equipped with a zero element, a one element, and an addition operation satisfying the properties of an `AddMonoidWithOne`. Suppose further that: 1. $0 \leq 1$ holds in $\alpha$ (from `ZeroLEOneClass`), 2. $1 \neq 0$ (from `NeZero (1 : α)`), and 3. Addition is strictly monotone on the right (from `AddRightStrictMono`). Then for any element $a \in \alpha$, we have $a < 1 + a$.

zero_le_two theorem

[Preorder α] [ZeroLEOneClass α] [AddLeftMono α] : (0 : α) ≤ 2

Full source

lemma zero_le_two [Preorder α] [ZeroLEOneClass α] [AddLeftMono α] :
    (0 : α) ≤ 2 := by
  rw [← one_add_one_eq_two]
  exact add_nonneg zero_le_one zero_le_one

Nonnegativity of Two in Ordered Monoids: $0 \leq 2$

Informal description

Let $\alpha$ be a type with a preorder, equipped with a zero element and a one element such that $0 \leq 1$, and where addition is monotone on the left. Then the zero element is less than or equal to the canonical image of the natural number $2$ in $\alpha$, i.e., $0 \leq 2$.

zero_le_three theorem

[Preorder α] [ZeroLEOneClass α] [AddLeftMono α] : (0 : α) ≤ 3

Full source

lemma zero_le_three [Preorder α] [ZeroLEOneClass α] [AddLeftMono α] :
    (0 : α) ≤ 3 := by
  rw [← two_add_one_eq_three]
  exact add_nonneg zero_le_two zero_le_one

Nonnegativity of Three in Ordered Monoids: $0 \leq 3$

Informal description

Let $\alpha$ be a type with a preorder, equipped with a zero element and a one element such that $0 \leq 1$, and where addition is monotone on the left. Then the zero element is less than or equal to the canonical image of the natural number $3$ in $\alpha$, i.e., $0 \leq 3$.

zero_le_four theorem

[Preorder α] [ZeroLEOneClass α] [AddLeftMono α] : (0 : α) ≤ 4

Full source

lemma zero_le_four [Preorder α] [ZeroLEOneClass α] [AddLeftMono α] :
    (0 : α) ≤ 4 := by
  rw [← three_add_one_eq_four]
  exact add_nonneg zero_le_three zero_le_one

Nonnegativity of Four in Ordered Monoids: $0 \leq 4$

Informal description

Let $\alpha$ be a type with a preorder, equipped with a zero element and a one element such that $0 \leq 1$, and where addition is monotone on the left. Then the zero element is less than or equal to the canonical image of the natural number $4$ in $\alpha$, i.e., $0 \leq 4$.

one_le_two theorem

[LE α] [ZeroLEOneClass α] [AddLeftMono α] : (1 : α) ≤ 2

Full source

lemma 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

Inequality of One and Two in Ordered Additive Monoids with One

Informal description

For any type $\alpha$ equipped with a preorder relation $\leq$, a zero element, and a one element, and where addition is monotone with respect to the order, the inequality $1 \leq 2$ holds.

one_le_two' theorem

[LE α] [ZeroLEOneClass α] [AddRightMono α] : (1 : α) ≤ 2

Full source

lemma 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

Inequality of One and Two in Right-Monotone Additive Structures

Informal description

For any type $\alpha$ equipped with a preorder relation $\leq$, a zero and one element, and a right-monotone addition operation, the inequality $1 \leq 2$ holds.

zero_lt_two theorem

: (0 : α) < 2

Full source

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

Positivity of Two in Ordered Additive Monoids with One: $0 < 2$

Informal description

In any additive monoid with one $\alpha$ where addition is monotone with respect to the order, the element $2$ is strictly greater than $0$, i.e., $0 < 2$.

zero_lt_three theorem

: (0 : α) < 3

Full source

/-- See `zero_lt_three'` for a version with the type explicit. -/
@[simp] lemma zero_lt_three : (0 : α) < 3 := by
  rw [← two_add_one_eq_three]
  exact lt_add_of_lt_of_nonneg zero_lt_two zero_le_one

Positivity of Three in Ordered Additive Monoids with One: $0 < 3$

Informal description

In any additive monoid with one $\alpha$ where addition is monotone with respect to the order, the element $3$ is strictly greater than $0$, i.e., $0 < 3$.

zero_lt_four theorem

: (0 : α) < 4

Full source

/-- See `zero_lt_four'` for a version with the type explicit. -/
@[simp] lemma zero_lt_four : (0 : α) < 4 := by
  rw [← three_add_one_eq_four]
  exact lt_add_of_lt_of_nonneg zero_lt_three zero_le_one

Positivity of Four in Ordered Additive Monoids with One: $0 < 4$

Informal description

In any additive monoid with one $\alpha$ where addition is monotone with respect to the order, the element $4$ is strictly greater than $0$, i.e., $0 < 4$.

zero_lt_two' theorem

: (0 : α) < 2

Full source

/-- See `zero_lt_two` for a version with the type implicit. -/
lemma zero_lt_two' : (0 : α) < 2 := zero_lt_two

Positivity of Two in Ordered Additive Monoids with One: $0 < 2$

Informal description

In any additive monoid with one $\alpha$ where addition is monotone with respect to the order, the element $2$ is strictly greater than $0$, i.e., $0 < 2$.

zero_lt_three' theorem

: (0 : α) < 3

Full source

/-- See `zero_lt_three` for a version with the type implicit. -/
lemma zero_lt_three' : (0 : α) < 3 := zero_lt_three

Positivity of Three in Ordered Additive Monoids with One: $0 < 3$

Informal description

In any additive monoid with one $\alpha$ where addition is monotone with respect to the order, the element $3$ is strictly greater than $0$, i.e., $0 < 3$.

zero_lt_four' theorem

: (0 : α) < 4

Full source

/-- See `zero_lt_four` for a version with the type implicit. -/
lemma zero_lt_four' : (0 : α) < 4 := zero_lt_four

Positivity of Four in Ordered Additive Monoids with One: $0 < 4$

Informal description

In any additive monoid with one $\alpha$ where addition is monotone with respect to the order, the element $4$ is strictly greater than $0$, i.e., $0 < 4$.

ZeroLEOneClass.neZero.two instance

: NeZero (2 : α)

Full source

instance ZeroLEOneClass.neZero.two : NeZero (2 : α) := ⟨zero_lt_two.ne'⟩

Nonzero Property of Two in Additive Monoids with One

Informal description

In any additive monoid with one $\alpha$ where $0 \leq 1$, the element $2$ is nonzero.

ZeroLEOneClass.neZero.three instance

: NeZero (3 : α)

Full source

instance ZeroLEOneClass.neZero.three : NeZero (3 : α) := ⟨zero_lt_three.ne'⟩

Nonzero Property of Three in Additive Monoids with One

Informal description

In any additive monoid with one $\alpha$ where $0 \leq 1$, the element $3$ is nonzero.

ZeroLEOneClass.neZero.four instance

: NeZero (4 : α)

Full source

instance ZeroLEOneClass.neZero.four : NeZero (4 : α) := ⟨zero_lt_four.ne'⟩

Nonzero Property of Four in Additive Monoids with One

Informal description

In any additive monoid with one $\alpha$ where $0 \leq 1$, the element $4$ is nonzero.

one_lt_two theorem

[AddLeftStrictMono α] : (1 : α) < 2

Full source

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

Strict Inequality: $1 < 2$ in Ordered Additive Monoids with One

Informal description

Let $\alpha$ be a type with a partial order, equipped with a zero element, a one element, and an addition operation such that addition is strictly monotone on the left. Then the multiplicative identity $1$ is strictly less than $2$ in $\alpha$, i.e., $1 < 2$.