Documentation

Init.Grind.Ordered.Module

class Lean.Grind.OrderedAdd (M : Type u) [HAdd M M M] [Preorder 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} [Preorder 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} [Preorder 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} [Preorder M] [AddCommMonoid M] [OrderedAdd M] {a b : M} (c : M) (h : a b) :
      c + a c + b
      theorem Lean.Grind.OrderedAdd.add_lt_left {M : Type u} [Preorder M] [AddCommMonoid M] [OrderedAdd M] {a b : M} (h : a < b) (c : M) :
      a + c < b + c
      theorem Lean.Grind.OrderedAdd.add_lt_right {M : Type u} [Preorder M] [AddCommMonoid M] [OrderedAdd M] {a b : M} (c : M) (h : a < b) :
      c + a < c + b
      theorem Lean.Grind.OrderedAdd.add_lt_left_iff {M : Type u} [Preorder M] [AddCommMonoid M] [OrderedAdd M] {a b : M} (c : M) :
      a < b a + c < b + c
      theorem Lean.Grind.OrderedAdd.add_lt_right_iff {M : Type u} [Preorder M] [AddCommMonoid M] [OrderedAdd M] {a b : M} (c : M) :
      a < b c + a < c + b
      theorem Lean.Grind.OrderedAdd.add_le_add {M : Type u} [Preorder M] [AddCommMonoid M] [OrderedAdd M] {a b c d : M} (hab : a b) (hcd : c d) :
      a + c b + d
      theorem Lean.Grind.OrderedAdd.nsmul_le_nsmul {M : Type u} [Preorder M] [NatModule M] [OrderedAdd M] {k : Nat} {a b : M} (h : a b) :
      k * a k * b
      theorem Lean.Grind.OrderedAdd.nsmul_lt_nsmul_iff {M : Type u} [Preorder M] [NatModule M] [OrderedAdd 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} [Preorder M] [NatModule M] [OrderedAdd M] {k : Nat} {a : M} (h : 0 < a) :
      0 < k * a 0 < k
      theorem Lean.Grind.OrderedAdd.nsmul_nonneg {M : Type u} [Preorder 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} [Preorder 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.zsmul_pos_iff {M : Type u} [Preorder M] [IntModule M] [OrderedAdd M] (k : Int) {x : M} (h : 0 < x) :
      0 < k * x 0 < k
      theorem Lean.Grind.OrderedAdd.zsmul_nonneg {M : Type u} [Preorder M] [IntModule M] [OrderedAdd M] {k : Int} {x : M} (h : 0 k) (hx : 0 x) :
      0 k * x
      theorem Lean.Grind.OrderedAdd.neg_lt_iff {M : Type u} [Preorder M] [AddCommGroup M] [OrderedAdd M] {a b : M} :
      -a < b -b < a
      theorem Lean.Grind.OrderedAdd.lt_neg_iff {M : Type u} [Preorder M] [AddCommGroup M] [OrderedAdd M] {a b : M} :
      a < -b b < -a
      theorem Lean.Grind.OrderedAdd.sub_pos_iff {M : Type u} [Preorder M] [AddCommGroup M] [OrderedAdd M] {a b : M} :
      0 < a - b b < a
      theorem Lean.Grind.OrderedAdd.zsmul_neg_iff {M : Type u} [Preorder M] [IntModule M] [OrderedAdd M] (k : Int) {a : M} (h : a < 0) :
      k * a < 0 0 < k
      theorem Lean.Grind.OrderedAdd.zsmul_nonpos {M : Type u} [Preorder 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} [Preorder 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_lt_zsmul_iff {M : Type u} [Preorder M] [IntModule M] [OrderedAdd M] (k : Int) {a b : M} (h : a < b) :
      k * a < k * b 0 < k
      theorem Lean.Grind.OrderedAdd.zsmul_le_zsmul_of_le_of_le_of_nonneg_of_nonneg {M : Type u} [Preorder 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