Documentation

Init.Grind.Ordered.Module

class Lean.Grind.OrderedAdd (M : Type u) [HAdd M M M] [LE M] [Std.IsPreorder M] :

Addition is compatible with a preorder if a ≤ b ↔ a + c ≤ b + c.

add_le_left_iff {a b : M} (c : M) : a ≤ b ↔ a + c ≤ b + c
a + c ≤ b + c iff a ≤ b.

Instances

class Lean.Grind.ExistsAddOfLT (α : Type u) [LT α] [Zero α] [Add α] :

exists_add_of_le {a b : α} : a < b → ∃ (c : α), 0 < c ∧ b = a + c

Instances

theorem Lean.Grind.OrderedAdd.add_le_right_iff {M : Type u} [LE M] [Std.IsPreorder M] [AddCommMonoid M] [OrderedAdd M] {a b : M} (c : M) :

a ≤ b ↔ c + a ≤ c + b

theorem Lean.Grind.OrderedAdd.add_le_left {M : Type u} [LE M] [Std.IsPreorder M] [AddCommMonoid M] [OrderedAdd M] {a b : M} (h : a ≤ b) (c : M) :

a + c ≤ b + c

theorem Lean.Grind.OrderedAdd.add_le_right {M : Type u} [LE M] [Std.IsPreorder M] [AddCommMonoid M] [OrderedAdd M] {a b : M} (c : M) (h : a ≤ b) :

c + a ≤ c + b

theorem Lean.Grind.OrderedAdd.add_le_add {M : Type u} [LE M] [Std.IsPreorder M] [AddCommMonoid M] [OrderedAdd M] {a b c d : M} (hab : a ≤ b) (hcd : c ≤ d) :

a + c ≤ b + d

theorem Lean.Grind.OrderedAdd.add_lt_left {M : Type u} [LE M] [Std.IsPreorder M] [AddCommMonoid M] [OrderedAdd M] [LT M] [Std.LawfulOrderLT M] {a b : M} (h : a < b) (c : M) :

a + c < b + c

theorem Lean.Grind.OrderedAdd.add_lt_right {M : Type u} [LE M] [Std.IsPreorder M] [AddCommMonoid M] [OrderedAdd M] [LT M] [Std.LawfulOrderLT M] {a b : M} (c : M) (h : a < b) :

c + a < c + b

theorem Lean.Grind.OrderedAdd.add_lt_left_iff {M : Type u} [LE M] [Std.IsPreorder M] [AddCommMonoid M] [OrderedAdd M] [LT M] [Std.LawfulOrderLT M] {a b : M} (c : M) :

a < b ↔ a + c < b + c

theorem Lean.Grind.OrderedAdd.add_lt_right_iff {M : Type u} [LE M] [Std.IsPreorder M] [AddCommMonoid M] [OrderedAdd M] [LT M] [Std.LawfulOrderLT M] {a b : M} (c : M) :

a < b ↔ c + a < c + b

theorem Lean.Grind.OrderedAdd.nsmul_le_nsmul {M : Type u} [LE M] [Std.IsPreorder M] [NatModule M] [OrderedAdd M] {k : Nat} {a b : M} (h : a ≤ b) :

k • a ≤ k • b

theorem Lean.Grind.OrderedAdd.nsmul_nonneg {M : Type u} [LE M] [Std.IsPreorder M] [NatModule M] [OrderedAdd M] {k : Nat} {a : M} (h : 0 ≤ a) :

0 ≤ k • a

theorem Lean.Grind.OrderedAdd.nsmul_le_nsmul_of_le_of_le_of_nonneg {M : Type u} [LE M] [Std.IsPreorder M] [NatModule M] [OrderedAdd M] {k₁ k₂ : Nat} {x y : M} (hk : k₁ ≤ k₂) (h : x ≤ y) (w : 0 ≤ x) :

k₁ • x ≤ k₂ • y

theorem Lean.Grind.OrderedAdd.nsmul_lt_nsmul_iff {M : Type u} [LE M] [Std.IsPreorder M] [NatModule M] [OrderedAdd M] [LT M] [Std.LawfulOrderLT M] (k : Nat) {a b : M} (h : a < b) :

k • a < k • b ↔ 0 < k

theorem Lean.Grind.OrderedAdd.nsmul_pos_iff {M : Type u} [LE M] [Std.IsPreorder M] [NatModule M] [OrderedAdd M] [LT M] [Std.LawfulOrderLT M] {k : Nat} {a : M} (h : 0 < a) :

0 < k • a ↔ 0 < k

theorem Lean.Grind.OrderedAdd.neg_le_iff {M : Type u} [LE M] [Std.IsPreorder M] [AddCommGroup M] [OrderedAdd M] {a b : M} :

-a ≤ b ↔ -b ≤ a

theorem Lean.Grind.OrderedAdd.zsmul_nonneg {M : Type u} [LE M] [Std.IsPreorder M] [IntModule M] [OrderedAdd M] {k : Int} {x : M} (h : 0 ≤ k) (hx : 0 ≤ x) :

0 ≤ k • x

theorem Lean.Grind.OrderedAdd.zsmul_pos_iff {M : Type u} [LE M] [Std.IsPreorder M] [IntModule M] [OrderedAdd M] [LT M] [Std.LawfulOrderLT M] (k : Int) {x : M} (h : 0 < x) :

0 < k • x ↔ 0 < k

theorem Lean.Grind.OrderedAdd.le_neg_iff {M : Type u} [LE M] [Std.IsPreorder M] [AddCommGroup M] [OrderedAdd M] {a b : M} :

a ≤ -b ↔ b ≤ -a

theorem Lean.Grind.OrderedAdd.neg_nonneg_iff {M : Type u} [LE M] [Std.IsPreorder M] [AddCommGroup M] [OrderedAdd M] {a : M} :

0 ≤ -a ↔ a ≤ 0

theorem Lean.Grind.OrderedAdd.sub_nonneg_iff {M : Type u} [LE M] [Std.IsPreorder M] [AddCommGroup M] [OrderedAdd M] {a b : M} :

0 ≤ a - b ↔ b ≤ a

theorem Lean.Grind.OrderedAdd.neg_lt_iff {M : Type u} [LE M] [Std.IsPreorder M] [AddCommGroup M] [OrderedAdd M] [LT M] [Std.LawfulOrderLT M] {a b : M} :

-a < b ↔ -b < a

theorem Lean.Grind.OrderedAdd.lt_neg_iff {M : Type u} [LE M] [Std.IsPreorder M] [AddCommGroup M] [OrderedAdd M] [LT M] [Std.LawfulOrderLT M] {a b : M} :

a < -b ↔ b < -a

theorem Lean.Grind.OrderedAdd.neg_pos_iff {M : Type u} [LE M] [Std.IsPreorder M] [AddCommGroup M] [OrderedAdd M] [LT M] [Std.LawfulOrderLT M] {a : M} :

0 < -a ↔ a < 0

theorem Lean.Grind.OrderedAdd.sub_pos_iff {M : Type u} [LE M] [Std.IsPreorder M] [AddCommGroup M] [OrderedAdd M] [LT M] [Std.LawfulOrderLT M] {a b : M} :

0 < a - b ↔ b < a

theorem Lean.Grind.OrderedAdd.zsmul_nonpos {M : Type u} [LE M] [Std.IsPreorder M] [IntModule M] [OrderedAdd M] {k : Int} {a : M} (hk : 0 ≤ k) (ha : a ≤ 0) :

k • a ≤ 0

theorem Lean.Grind.OrderedAdd.zsmul_le_zsmul {M : Type u} [LE M] [Std.IsPreorder M] [IntModule M] [OrderedAdd M] {a b : M} {k : Int} (hk : 0 ≤ k) (h : a ≤ b) :

k • a ≤ k • b

theorem Lean.Grind.OrderedAdd.zsmul_le_zsmul_of_le_of_le_of_nonneg_of_nonneg {M : Type u} [LE M] [Std.IsPreorder M] [IntModule M] [OrderedAdd M] {k₁ k₂ : Int} {x y : M} (hk : k₁ ≤ k₂) (h : x ≤ y) (w : 0 ≤ k₁) (w' : 0 ≤ x) :

k₁ • x ≤ k₂ • y

theorem Lean.Grind.OrderedAdd.zsmul_neg_iff {M : Type u} [LE M] [Std.IsPreorder M] [IntModule M] [OrderedAdd M] [LT M] [Std.LawfulOrderLT M] (k : Int) {a : M} (h : a < 0) :

k • a < 0 ↔ 0 < k

theorem Lean.Grind.OrderedAdd.zsmul_lt_zsmul_iff {M : Type u} [LE M] [Std.IsPreorder M] [IntModule M] [OrderedAdd M] [LT M] [Std.LawfulOrderLT M] (k : Int) {a b : M} (h : a < b) :

k • a < k • b ↔ 0 < k