Theorems · Theorem · real analysis
Real.rpow_inv_log_le_exp_one
∀ {x : ℝ}, x ^ (Real.log x)⁻¹ ≤ Real.exp 1See Real.rpow_inv_log for the equality when x ≠ 1 is strictly positive.
- Cited by
- 0 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.
Cites15
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
- absproof · cited by 1,814
- Real.logstatement and proof · cited by 939
- Real.expstatement and proof · cited by 871
- inv_zeroproof · cited by 184
- abs_nonnegproof · cited by 168
- le_abs_selfproof · cited by 113
- Real.log_zeroproof · cited by 84
- Real.rpow_zeroproof · cited by 69
- Real.rpow_def_of_posproof · cited by 35
- Real.exp_monotoneproof · cited by 30
- LE.le.eq_or_lt'proof · cited by 27
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.