Inequalities

Stream: new members

[Timothy Harevy]

I was doing a project for uni and needed an inequality that wasn't In mathlib . So I've proved them the code is below

import Mathlib.Tactic
import Mathlib.Algebra.Field.Basic

theorem mul_lt_mul_of_nonneg_left {α : Type u_2} [LinearOrderedSemifield α]
(a : α) (b : α)(c : α) (hc: 0 ≤c) : a<b → c*a≤c*b := by{
  intro h'
  by_cases c = 0
  rw[h]
  rw[zero_mul,zero_mul]
  push_neg at h
  have h'' : 0 < c := by{
    by_contra sub
    push_neg at sub
    have sub2 : c=0:=by{
      apply LE.le.antisymm sub hc
    }
    apply h sub2
  }
  have h''': c*a<c*b :=by{
    apply mul_lt_mul_of_pos_left h' h''
  }
  apply LT.lt.le h'''
}
theorem mul_lt_mul_of_nonneg_right {α : Type u_2} [LinearOrderedSemifield α] {a b c : α} (hc: 0 ≤c) : a<b → a*c≤b*c := by{
  intro h'
  by_cases c = 0
  rw[h]
  rw[mul_zero,mul_zero]
  push_neg at h
  have h'' : 0 < c := by{
    by_contra sub
    push_neg at sub
    have sub2 : c=0:=by{
      apply LE.le.antisymm sub hc
    }
    apply h sub2
  }
  have h''': a*c<b*c :=by{
    apply mul_lt_mul_of_pos_right h' h''
  }
  apply LT.lt.le h'''
}

[Yaël Dillies]

Is it not just docs#mul_le_mul_of_nonneg_left ?

[Timothy Harevy]

Oh lol sorry guess I didn't see that

[Yaël Dillies]

Note you would have noticed had you guessed the name right!

[Yaël Dillies]

You could also have tried apply? or gcongr