Theorems · Theorem · complex analysis
Real.add_one_le_exp
∀ (x : ℝ), x + 1 ≤ Real.exp x
- Defined in
- Mathlib.Analysis.Complex.Exponential
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 151 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- zero_addproof · cited by 2,366
- LT.lt.leproof · cited by 2,189
- eq_or_neproof · cited by 1,117
- Real.expstatement · cited by 871
- Real.exp_zeroproof · cited by 81
- Real.add_one_lt_expproof · cited by 4
Cited by13
Results whose statement or proof uses this declaration.
- Real.tendsto_exp_atTopproof · cited by 10
- Real.log_le_sub_one_of_posproof · cited by 5
- Stirling.log_stirlingSeq_sdiff_leproof · cited by 3
- Real.mulExpNegMulSq_one_le_oneproof · cited by 2
- Finset.norm_prod_one_add_sub_one_leproof · cited by 1
- Behrend.exp_neg_two_mul_leproof · cited by 1
- Real.exp_one_mul_le_expproof · cited by 1
- Real.one_sub_le_exp_negproof · cited by 1
- Real.prod_one_add_le_exp_sumproof · cited by 1
- Real.le_inv_mul_expproof · cited by 1
- Real.two_mul_le_expproof · cited by 1