Documentation

Init.Grind.Ordered.Module

source
class Lean.Grind.OrderedAdd (M : Type u) [HAdd M M M] [LE M] [LT M] [Preorder 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] [LT M] [Preorder 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] [LT M] [Preorder 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] [LT M] [Preorder M] [AddCommMonoid M] [OrderedAdd M] {a b : M} (c : M) (h : a ≤ b) :
      c + a ≤ c + b
      source
      theorem Lean.Grind.OrderedAdd.add_lt_left {M : Type u} [LE M] [LT M] [Preorder M] [AddCommMonoid M] [OrderedAdd 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] [LT M] [Preorder M] [AddCommMonoid M] [OrderedAdd 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] [LT M] [Preorder M] [AddCommMonoid M] [OrderedAdd 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] [LT M] [Preorder M] [AddCommMonoid M] [OrderedAdd M] {a b : M} (c : M) :
      a < b ↔ c + a < c + b
      source
      theorem Lean.Grind.OrderedAdd.add_le_add {M : Type u} [LE M] [LT M] [Preorder 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.nsmul_le_nsmul {M : Type u} [LE M] [LT M] [Preorder M] [NatModule M] [OrderedAdd M] {k : Nat} {a b : M} (h : a ≤ b) :
      k * a ≤ k * b
      source
      theorem Lean.Grind.OrderedAdd.nsmul_lt_nsmul_iff {M : Type u} [LE M] [LT M] [Preorder M] [NatModule M] [OrderedAdd 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] [LT M] [Preorder M] [NatModule M] [OrderedAdd M] {k : Nat} {a : M} (h : 0 < a) :
      0 < k * a ↔ 0 < k
      source
      theorem Lean.Grind.OrderedAdd.nsmul_nonneg {M : Type u} [LE M] [LT M] [Preorder 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] [LT M] [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
      source
      theorem Lean.Grind.OrderedAdd.neg_le_iff {M : Type u} [LE M] [LT M] [Preorder M] [AddCommGroup M] [OrderedAdd M] {a b : M} :
      -a ≤ b ↔ -b ≤ a
      source
      theorem Lean.Grind.OrderedAdd.zsmul_pos_iff {M : Type u} [LE M] [LT M] [Preorder M] [IntModule M] [OrderedAdd M] (k : Int) {x : M} (h : 0 < x) :
      0 < k * x ↔ 0 < k
      source
      theorem Lean.Grind.OrderedAdd.zsmul_nonneg {M : Type u} [LE M] [LT M] [Preorder M] [IntModule M] [OrderedAdd M] {k : Int} {x : M} (h : 0 ≤ k) (hx : 0 ≤ x) :
      0 ≤ k * x
      source
      theorem Lean.Grind.OrderedAdd.le_neg_iff {M : Type u} [LE M] [LT M] [Preorder M] [AddCommGroup M] [OrderedAdd M] {a b : M} :
      a ≤ -b ↔ b ≤ -a
      source
      theorem Lean.Grind.OrderedAdd.neg_lt_iff {M : Type u} [LE M] [LT M] [Preorder M] [AddCommGroup M] [OrderedAdd M] {a b : M} :
      -a < b ↔ -b < a
      source
      theorem Lean.Grind.OrderedAdd.lt_neg_iff {M : Type u} [LE M] [LT M] [Preorder 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] [LT M] [Preorder M] [AddCommGroup M] [OrderedAdd M] {a : M} :
      0 ≤ -a ↔ a ≤ 0
      source
      theorem Lean.Grind.OrderedAdd.neg_pos_iff {M : Type u} [LE M] [LT M] [Preorder M] [AddCommGroup M] [OrderedAdd M] {a : M} :
      0 < -a ↔ a < 0
      source
      theorem Lean.Grind.OrderedAdd.sub_nonneg_iff {M : Type u} [LE M] [LT M] [Preorder M] [AddCommGroup M] [OrderedAdd M] {a b : M} :
      0 ≤ a - b ↔ b ≤ a
      source
      theorem Lean.Grind.OrderedAdd.sub_pos_iff {M : Type u} [LE M] [LT M] [Preorder M] [AddCommGroup M] [OrderedAdd M] {a b : M} :
      0 < a - b ↔ b < a
      source
      theorem Lean.Grind.OrderedAdd.zsmul_neg_iff {M : Type u} [LE M] [LT M] [Preorder M] [IntModule M] [OrderedAdd M] (k : Int) {a : M} (h : a < 0) :
      k * a < 0 ↔ 0 < k
      source
      theorem Lean.Grind.OrderedAdd.zsmul_nonpos {M : Type u} [LE M] [LT M] [Preorder 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] [LT M] [Preorder 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_lt_zsmul_iff {M : Type u} [LE M] [LT M] [Preorder M] [IntModule M] [OrderedAdd M] (k : Int) {a b : M} (h : a < b) :
      k * a < k * b ↔ 0 < k
      source
      theorem Lean.Grind.OrderedAdd.zsmul_le_zsmul_of_le_of_le_of_nonneg_of_nonneg {M : Type u} [LE M] [LT M] [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