Theorems · Theorem · special functions
Continuous.rexp
∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ}, Continuous f → Continuous fun y => Real.exp (f y)- Defined in
- Mathlib.Analysis.SpecialFunctions.Exp
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 168 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpace
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
- TopologicalSpacestatement and proof · cited by 24,529
- Continuousstatement and proof · cited by 2,592
- Real.expstatement · cited by 871
- Continuous.continuousAtproof · cited by 297
- continuous_iff_continuousAtproof · cited by 139
- ContinuousAt.rexpproof · cited by 3
Cited by17
Results whose statement or proof uses this declaration.
- ProbabilityTheory.IsGaussian.memLp_idproof · cited by 4
- Complex.GammaIntegral_convergentproof · cited by 3
- ProbabilityTheory.integrable_rpow_mul_exp_of_integrable_exp_mulproof · cited by 3
- ProbabilityTheory.integrable_exp_mul_abs_addproof · cited by 2
- ProbabilityTheory.integrable_rpow_abs_mul_exp_add_of_integrable_exp_mulproof · cited by 2
- Real.continuous_mulExpNegMulSqproof · cited by 1
- Complex.partialGamma_add_oneproof · cited by 1
- ProbabilityTheory.lintegral_exponentialPDF_eq_antiDerivproof · cited by 1
- ProbabilityTheory.Kernel.HasSubgaussianMGF.of_ratproof · cited by 1
- ProbabilityTheory.exists_integrable_exp_sq_of_map_rotation_eq_self'proof · cited by 1
- ProbabilityTheory.IsGaussian.integrable_exp_sq_of_conv_negproof · cited by 1