Documentation

Mathlib.Tactic.Linarith.Lemmas

Lemmas for linarith. #

Those in the Linarith namespace should stay here.

Those outside the Linarith namespace may be deleted as they are ported to mathlib4.

source
ink
theorem Linarith.lt_irrefl {α : Type u} [inst : Preorder α] {a : α} :
¬a < a
source
ink
theorem Linarith.eq_of_eq_of_eq {α : Type u_1} [inst : OrderedSemiring α] {a : α} {b : α} (ha : a = 0) (hb : b = 0) :
a + b = 0
source
ink
theorem Linarith.le_of_eq_of_le {α : Type u_1} [inst : OrderedSemiring α] {a : α} {b : α} (ha : a = 0) (hb : b ≤ 0) :
a + b ≤ 0
source
ink
theorem Linarith.lt_of_eq_of_lt {α : Type u_1} [inst : OrderedSemiring α] {a : α} {b : α} (ha : a = 0) (hb : b < 0) :
a + b < 0
source
ink
theorem Linarith.le_of_le_of_eq {α : Type u_1} [inst : OrderedSemiring α] {a : α} {b : α} (ha : a ≤ 0) (hb : b = 0) :
a + b ≤ 0
source
ink
theorem Linarith.lt_of_lt_of_eq {α : Type u_1} [inst : OrderedSemiring α] {a : α} {b : α} (ha : a < 0) (hb : b = 0) :
a + b < 0
source
ink
theorem Linarith.mul_neg {α : Type u_1} [inst : StrictOrderedRing α] {a : α} {b : α} (ha : a < 0) (hb : 0 < b) :
b * a < 0
source
ink
theorem Linarith.mul_nonpos {α : Type u_1} [inst : OrderedRing α] {a : α} {b : α} (ha : a ≤ 0) (hb : 0 < b) :
b * a ≤ 0
source
ink
theorem Linarith.mul_eq {α : Type u_1} [inst : OrderedSemiring α] {a : α} {b : α} (ha : a = 0) :
0 < b → b * a = 0
source
ink
theorem Linarith.eq_of_not_lt_of_not_gt {α : Type u_1} [inst : LinearOrder α] (a : α) (b : α) (h1 : ¬a < b) (h2 : ¬b < a) :
a = b
source
ink
theorem Linarith.mul_zero_eq {α : Type u_1} {R : α → α → Prop} [inst : Semiring α] {a : α} {b : α} :
R a 0 → b = 0 → a * b = 0
source
ink
theorem Linarith.zero_mul_eq {α : Type u_1} {R : α → α → Prop} [inst : Semiring α] {a : α} {b : α} (h : a = 0) :
R b 0 → a * b = 0
source
ink
theorem lt_zero_of_zero_gt {α : Type u_1} [inst : Zero α] [inst : LT α] {a : α} (h : 0 > a) :
a < 0
source
ink
theorem le_zero_of_zero_ge {α : Type u_1} [inst : Zero α] [inst : LE α] {a : α} (h : 0 ≥ a) :
a ≤ 0