Cast of natural numbers: lemmas about order #

source

theorem Nat.mono_cast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] :

Monotone Nat.cast

source

@[deprecated Nat.mono_cast]

theorem Nat.cast_le_cast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] {a : ℕ} {b : ℕ} (h : a ≤ b) :

↑a ≤ ↑b

source

theorem GCongr.natCast_le_natCast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] {a : ℕ} {b : ℕ} (h : a ≤ b) :

↑a ≤ ↑b

source

@[simp]

theorem Nat.cast_nonneg' {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] (n : ℕ) :

0 ≤ ↑n

See also Nat.cast_nonneg, specialised for an OrderedSemiring.

source

@[simp]

theorem Nat.cast_nonneg {α : Type u_3} [OrderedSemiring α] (n : ℕ) :

0 ≤ ↑n

Specialisation of Nat.cast_nonneg', which seems to be easier for Lean to use.

source

@[simp]

theorem Nat.ofNat_nonneg' {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] (n : ℕ) [Nat.AtLeastTwo n] :

0 ≤ OfNat.ofNat n

See also Nat.ofNat_nonneg, specialised for an OrderedSemiring.

source

@[simp]

theorem Nat.ofNat_nonneg {α : Type u_3} [OrderedSemiring α] (n : ℕ) [Nat.AtLeastTwo n] :

0 ≤ OfNat.ofNat n

Specialisation of Nat.ofNat_nonneg', which seems to be easier for Lean to use.

source

@[simp]

theorem Nat.cast_min {α : Type u_3} [LinearOrderedSemiring α] {a : ℕ} {b : ℕ} :

↑(min a b) = min ↑a ↑b

source

@[simp]

theorem Nat.cast_max {α : Type u_3} [LinearOrderedSemiring α] {a : ℕ} {b : ℕ} :

↑(max a b) = max ↑a ↑b

source

theorem Nat.cast_add_one_pos {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [NeZero 1] (n : ℕ) :

0 < ↑n + 1

source

@[simp]

theorem Nat.cast_pos' {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [NeZero 1] {n : ℕ} :

0 < ↑n ↔ 0 < n

See also Nat.cast_pos, specialised for an OrderedSemiring.

source

@[simp]

theorem Nat.cast_pos {α : Type u_3} [OrderedSemiring α] [Nontrivial α] {n : ℕ} :

0 < ↑n ↔ 0 < n

Specialisation of Nat.cast_pos', which seems to be easier for Lean to use.

source

@[simp]

theorem Nat.ofNat_pos' {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [NeZero 1] {n : ℕ} [Nat.AtLeastTwo n] :

0 < OfNat.ofNat n

See also Nat.ofNat_pos, specialised for an OrderedSemiring.

source

@[simp]

theorem Nat.ofNat_pos {α : Type u_3} [OrderedSemiring α] [Nontrivial α] {n : ℕ} [Nat.AtLeastTwo n] :

0 < OfNat.ofNat n

Specialisation of Nat.ofNat_pos', which seems to be easier for Lean to use.

source

theorem Nat.strictMono_cast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] :

StrictMono Nat.cast

source

@[simp]

theorem Nat.castOrderEmbedding_apply {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] :

⇑Nat.castOrderEmbedding = Nat.cast

source

def Nat.castOrderEmbedding {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] :

ℕ ↪o α

Nat.cast : ℕ → α as an OrderEmbedding

Equations

Nat.castOrderEmbedding = OrderEmbedding.ofStrictMono Nat.cast ⋯

Instances For

source

@[simp]

theorem Nat.cast_le {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {m : ℕ} {n : ℕ} :

↑m ≤ ↑n ↔ m ≤ n

source

@[simp]

theorem Nat.cast_lt {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {m : ℕ} {n : ℕ} :

↑m < ↑n ↔ m < n

source

@[simp]

theorem Nat.one_lt_cast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {n : ℕ} :

1 < ↑n ↔ 1 < n

source

@[simp]

theorem Nat.one_le_cast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {n : ℕ} :

1 ≤ ↑n ↔ 1 ≤ n

source

@[simp]

theorem Nat.cast_lt_one {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {n : ℕ} :

↑n < 1 ↔ n = 0

source

@[simp]

theorem Nat.cast_le_one {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {n : ℕ} :

↑n ≤ 1 ↔ n ≤ 1

source

theorem Nat.ofNat_le {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {m : ℕ} {n : ℕ} [Nat.AtLeastTwo m] [Nat.AtLeastTwo n] :

OfNat.ofNat m ≤ OfNat.ofNat n ↔ OfNat.ofNat m ≤ OfNat.ofNat n

source

theorem Nat.ofNat_lt {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {m : ℕ} {n : ℕ} [Nat.AtLeastTwo m] [Nat.AtLeastTwo n] :

OfNat.ofNat m < OfNat.ofNat n ↔ OfNat.ofNat m < OfNat.ofNat n

source

@[simp]

theorem Nat.ofNat_le_cast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {m : ℕ} {n : ℕ} [Nat.AtLeastTwo m] :

OfNat.ofNat m ≤ ↑n ↔ OfNat.ofNat m ≤ n

source

@[simp]

theorem Nat.ofNat_lt_cast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {m : ℕ} {n : ℕ} [Nat.AtLeastTwo m] :

OfNat.ofNat m < ↑n ↔ OfNat.ofNat m < n

source

@[simp]

theorem Nat.cast_le_ofNat {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {m : ℕ} {n : ℕ} [Nat.AtLeastTwo n] :

↑m ≤ OfNat.ofNat n ↔ m ≤ OfNat.ofNat n

source

@[simp]

theorem Nat.cast_lt_ofNat {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {m : ℕ} {n : ℕ} [Nat.AtLeastTwo n] :

↑m < OfNat.ofNat n ↔ m < OfNat.ofNat n

source

@[simp]

theorem Nat.one_lt_ofNat {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {n : ℕ} [Nat.AtLeastTwo n] :

1 < OfNat.ofNat n

source

@[simp]

theorem Nat.one_le_ofNat {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {n : ℕ} [Nat.AtLeastTwo n] :

1 ≤ OfNat.ofNat n

source

@[simp]

theorem Nat.not_ofNat_le_one {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {n : ℕ} [Nat.AtLeastTwo n] :

¬OfNat.ofNat n ≤ 1

source

@[simp]

theorem Nat.not_ofNat_lt_one {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [CharZero α] {n : ℕ} [Nat.AtLeastTwo n] :

¬OfNat.ofNat n < 1

source

@[simp]

theorem Nat.cast_tsub {α : Type u_1} [CanonicallyOrderedCommSemiring α] [Sub α] [OrderedSub α] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (m : ℕ) (n : ℕ) :

↑(m - n) = ↑m - ↑n

A version of Nat.cast_sub that works for ℝ≥0 and ℚ≥0. Note that this proof doesn't work for ℕ∞ and ℝ≥0∞, so we use type-specific lemmas for these types.

source

@[simp]

theorem Nat.abs_cast {α : Type u_1} [LinearOrderedRing α] (a : ℕ) :

|↑a| = ↑a

source

@[simp]

theorem Nat.abs_ofNat {α : Type u_1} [LinearOrderedRing α] (n : ℕ) [Nat.AtLeastTwo n] :

|OfNat.ofNat n| = OfNat.ofNat n

source

instance instNontrivial {α : Type u_1} [AddMonoidWithOne α] [CharZero α] :

Nontrivial α

Equations

⋯ = ⋯

source

theorem NeZero.nat_of_injective {R : Type u_3} {S : Type u_4} {F : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] [FunLike F R S] {n : ℕ} [h : NeZero ↑n] [RingHomClass F R S] {f : F} (hf : Function.Injective ⇑f) :

NeZero ↑n

Documentation

Mathlib.Data.Nat.Cast.Order

Cast of natural numbers: lemmas about order #