Theorems · Theorem · real analysis
Real.abs_rpow_le_exp_log_mul
∀ (x y : ℝ), |x ^ y| ≤ Real.exp (Real.log x * y)
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 201 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- LE.le.transproof · cited by 3,151
- MulZeroClass.mul_zeroproof · cited by 2,091
- le_reflproof · cited by 2,061
- absstatement and proof · cited by 1,814
- MulZeroClass.zero_mulproof · cited by 1,625
- Real.logstatement and proof · cited by 939
- Real.expstatement and proof · cited by 871
- abs_zeroproof · cited by 88
- Real.log_zeroproof · cited by 84
- Real.exp_zeroproof · cited by 81
- Real.rpow_zeroproof · cited by 69
Cited by1
Results whose statement or proof uses this declaration.
- Real.continuousAt_rpow_of_posproof · cited by 1