Theorems · Theorem · special functions
Real.Gamma_pos_of_pos
∀ {s : ℝ}, 0 < s → 0 < Real.Gamma s- Cited by
- 17 results in Mathlib
- Foundations
- Depth 282 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites27
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setproof · cited by 53,352
- Realstatement and proof · cited by 25,697
- ENNRealproof · cited by 9,879
- Top.topproof · cited by 9,680
- LT.lt.leproof · cited by 2,189
- Set.Ioiproof · cited by 1,463
- LT.lt.ne'proof · cited by 1,417
- MeasureTheory.MeasureSpace.volumeproof · cited by 1,323
- Real.expproof · cited by 871
- Function.supportproof · cited by 610
- mul_posproof · cited by 374
Cited by17
Results whose statement or proof uses this declaration.
- Real.convexOn_log_Gammaproof · cited by 5
- Real.Gamma_ne_zeroproof · cited by 3
- ProbabilityTheory.beta_posproof · cited by 2
- Real.convexOn_Gammaproof · cited by 2
- ProbabilityTheory.lintegral_gammaPDF_eq_oneproof · cited by 2
- Real.deriv_Gamma_natproof · cited by 2
- Real.Gamma_three_div_two_lt_oneproof · cited by 2
- ProbabilityTheory.gammaPDFReal_nonnegproof · cited by 2
- MeasureTheory.measure_unitBall_eq_integral_div_gammaproof · cited by 1
- Real.BohrMollerup.tendsto_log_gammaproof · cited by 1
- Real.Gamma_mul_Gamma_add_half_of_posproof · cited by 1
- Real.doublingGamma_eq_Gammaproof · cited by 1