Documentation

Mathlib.Tactic.NormNum.Ineq

norm_num extensions for inequalities. #

Helper function to synthesize a typed OrderedSemiring α expression.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Helper function to synthesize a typed OrderedRing α expression.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Helper function to synthesize a typed LinearOrderedField α expression.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem Mathlib.Meta.NormNum.isNat_le_true {α : Type u_1} [OrderedSemiring α] {a : α} {b : α} {a' : } {b' : } :
        theorem Mathlib.Meta.NormNum.isNat_lt_false {α : Type u_1} [OrderedSemiring α] {a : α} {b : α} {a' : } {b' : } (ha : Mathlib.Meta.NormNum.IsNat a a') (hb : Mathlib.Meta.NormNum.IsNat b b') (h : Nat.ble b' a' = true) :
        ¬a < b
        theorem Mathlib.Meta.NormNum.isRat_le_true {α : Type u_1} [LinearOrderedRing α] {a : α} {b : α} {na : } {nb : } {da : } {db : } :
        theorem Mathlib.Meta.NormNum.isRat_lt_true {α : Type u_1} [LinearOrderedRing α] [Nontrivial α] {a : α} {b : α} {na : } {nb : } {da : } {db : } :
        Mathlib.Meta.NormNum.IsRat a na daMathlib.Meta.NormNum.IsRat b nb dbdecide (na * db < nb * da) = truea < b
        theorem Mathlib.Meta.NormNum.isRat_le_false {α : Type u_1} [LinearOrderedRing α] [Nontrivial α] {a : α} {b : α} {na : } {nb : } {da : } {db : } (ha : Mathlib.Meta.NormNum.IsRat a na da) (hb : Mathlib.Meta.NormNum.IsRat b nb db) (h : decide (nb * da < na * db) = true) :
        ¬a b
        theorem Mathlib.Meta.NormNum.isRat_lt_false {α : Type u_1} [LinearOrderedRing α] {a : α} {b : α} {na : } {nb : } {da : } {db : } (ha : Mathlib.Meta.NormNum.IsRat a na da) (hb : Mathlib.Meta.NormNum.IsRat b nb db) (h : decide (nb * da na * db) = true) :
        ¬a < b

        (In)equalities #

        theorem Mathlib.Meta.NormNum.isNat_lt_true {α : Type u_1} [OrderedSemiring α] [CharZero α] {a : α} {b : α} {a' : } {b' : } :
        theorem Mathlib.Meta.NormNum.isNat_le_false {α : Type u_1} [OrderedSemiring α] [CharZero α] {a : α} {b : α} {a' : } {b' : } (ha : Mathlib.Meta.NormNum.IsNat a a') (hb : Mathlib.Meta.NormNum.IsNat b b') (h : Nat.ble a' b' = false) :
        ¬a b
        theorem Mathlib.Meta.NormNum.isInt_le_true {α : Type u_1} [OrderedRing α] {a : α} {b : α} {a' : } {b' : } :
        theorem Mathlib.Meta.NormNum.isInt_lt_true {α : Type u_1} [OrderedRing α] [Nontrivial α] {a : α} {b : α} {a' : } {b' : } :
        theorem Mathlib.Meta.NormNum.isInt_le_false {α : Type u_1} [OrderedRing α] [Nontrivial α] {a : α} {b : α} {a' : } {b' : } (ha : Mathlib.Meta.NormNum.IsInt a a') (hb : Mathlib.Meta.NormNum.IsInt b b') (h : decide (b' < a') = true) :
        ¬a b
        theorem Mathlib.Meta.NormNum.isInt_lt_false {α : Type u_1} [OrderedRing α] {a : α} {b : α} {a' : } {b' : } (ha : Mathlib.Meta.NormNum.IsInt a a') (hb : Mathlib.Meta.NormNum.IsInt b b') (h : decide (b' a') = true) :
        ¬a < b

        The norm_num extension which identifies expressions of the form a ≤ b, such that norm_num successfully recognises both a and b.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def Mathlib.Meta.NormNum.evalLE.intArm {v : Lean.Level} {β : Q(Type v)} (e : Q(«$β»)) (f : Lean.Expr) (u : Lean.Level) (α : let u := u; Q(Type u)) (a : Q(«$α»)) (b : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) :
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def Mathlib.Meta.NormNum.evalLE.ratArm {v : Lean.Level} {β : Q(Type v)} (e : Q(«$β»)) (f : Lean.Expr) (u : Lean.Level) (α : let u := u; Q(Type u)) (a : Q(«$α»)) (b : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) :
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              The norm_num extension which identifies expressions of the form a < b, such that norm_num successfully recognises both a and b.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def Mathlib.Meta.NormNum.evalLT.intArm {v : Lean.Level} {β : Q(Type v)} (e : Q(«$β»)) (f : Lean.Expr) (u : Lean.Level) (α : let u := u; Q(Type u)) (a : Q(«$α»)) (b : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) :
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def Mathlib.Meta.NormNum.evalLT.ratArm {v : Lean.Level} {β : Q(Type v)} (e : Q(«$β»)) (f : Lean.Expr) (u : Lean.Level) (α : let u := u; Q(Type u)) (a : Q(«$α»)) (b : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) :
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For