Theorems · Theorem · order theory

mul_le_of_forall_lt_of_nonneg

∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b c : α},
  0 ≤ a → 0 ≤ c → (∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c) → a * b ≤ c

Defined in

Mathlib.Algebra.Order.Field.Basic

Cited by

3 results in Mathlib

Foundations

Depth 48 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldLinearOrderIsStrictOrderedRing