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

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

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

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

Instances

source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
theorem Lean.Grind.OrderedAdd.add_lt_add {M : Type u} [LE M] [Std.IsPreorder M] [AddCommMonoid M] [OrderedAdd M] [LT M] [Std.LawfulOrderLT M] {a b c d : M} (hab : a < b) (hcd : c < d) :
a + c < b + d
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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