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.

theorem Mathlib.Tactic.Linarith.lt_irrefl {α : Type u} [Preorder α] {a : α} :

¬a < a

theorem Mathlib.Tactic.Linarith.eq_of_eq_of_eq {α : Type u_1} [Semiring α] {a b : α} (ha : a = 0) (hb : b = 0) :

a + b = 0

theorem Mathlib.Tactic.Linarith.zero_lt_one {α : Type u} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] :

0 < 1

theorem Mathlib.Tactic.Linarith.le_of_eq_of_le {α : Type u} [Semiring α] [PartialOrder α] {a b : α} (ha : a = 0) (hb : b ≤ 0) :

a + b ≤ 0

theorem Mathlib.Tactic.Linarith.lt_of_eq_of_lt {α : Type u} [Semiring α] [PartialOrder α] {a b : α} (ha : a = 0) (hb : b < 0) :

a + b < 0

theorem Mathlib.Tactic.Linarith.le_of_le_of_eq {α : Type u} [Semiring α] [PartialOrder α] {a b : α} (ha : a ≤ 0) (hb : b = 0) :

a + b ≤ 0

theorem Mathlib.Tactic.Linarith.lt_of_lt_of_eq {α : Type u} [Semiring α] [PartialOrder α] {a b : α} (ha : a < 0) (hb : b = 0) :

a + b < 0

theorem Mathlib.Tactic.Linarith.add_nonpos {α : Type u} [Semiring α] [PartialOrder α] [IsOrderedRing α] {a b : α} (ha : a ≤ 0) (hb : b ≤ 0) :

a + b ≤ 0

theorem Mathlib.Tactic.Linarith.add_lt_of_le_of_neg {α : Type u} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] {a b c : α} (hbc : b ≤ c) (ha : a < 0) :

b + a < c

theorem Mathlib.Tactic.Linarith.add_lt_of_neg_of_le {α : Type u} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] {a b c : α} (ha : a < 0) (hbc : b ≤ c) :

a + b < c

theorem Mathlib.Tactic.Linarith.add_neg {α : Type u} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : b < 0) :

a + b < 0

theorem Mathlib.Tactic.Linarith.natCast_nonneg (α : Type u) [Semiring α] [PartialOrder α] [IsOrderedRing α] (n : ℕ) :

0 ≤ ↑n

theorem Mathlib.Tactic.Linarith.mul_eq {α : Type u} [Semiring α] [PartialOrder α] [IsOrderedRing α] {a b : α} (ha : a = 0) :

0 < b → b * a = 0

theorem Mathlib.Tactic.Linarith.mul_neg {α : Type u} [Ring α] [PartialOrder α] [IsStrictOrderedRing α] {a b : α} (ha : a < 0) (hb : 0 < b) :

b * a < 0

theorem Mathlib.Tactic.Linarith.mul_nonpos {α : Type u} [Ring α] [PartialOrder α] [IsOrderedRing α] {a b : α} (ha : a ≤ 0) (hb : 0 < b) :

b * a ≤ 0

theorem Mathlib.Tactic.Linarith.sub_nonpos_of_le {α : Type u} [Ring α] [PartialOrder α] [IsOrderedRing α] {a b : α} :

a ≤ b → a - b ≤ 0

theorem Mathlib.Tactic.Linarith.sub_neg_of_lt {α : Type u} [Ring α] [PartialOrder α] [IsOrderedRing α] {a b : α} :

a < b → a - b < 0

def Mathlib.Ineq.toConstMulName :

Ineq → Lean.Name

Finds the name of a multiplicative lemma corresponding to an inequality strength.

Equations

Mathlib.Ineq.lt.toConstMulName = `Mathlib.Tactic.Linarith.mul_neg
Mathlib.Ineq.le.toConstMulName = `Mathlib.Tactic.Linarith.mul_nonpos
Mathlib.Ineq.eq.toConstMulName = `Mathlib.Tactic.Linarith.mul_eq

Instances For

theorem Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt {α : Type u_1} [LinearOrder α] (a b : α) (h1 : ¬a < b) (h2 : ¬b < a) :

a = b

theorem Mathlib.Tactic.Linarith.mul_zero_eq {α : Type u_1} {R : α → α → Prop} [Semiring α] {a b : α} :

R a 0 → ∀ (h : b = 0), a * b = 0

theorem Mathlib.Tactic.Linarith.zero_mul_eq {α : Type u_1} {R : α → α → Prop} [Semiring α] {a b : α} (h : a = 0) :

R b 0 → a * b = 0