Theorems · Theorem · real analysis
Real.continuousAt_rpow_const
∀ (x q : ℝ), x ≠ 0 ∨ 0 ≤ q → ContinuousAt (fun x => x ^ q) x
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 204 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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
- ContinuousAtstatement and proof · cited by 697
- Real.rpow_zeroproof · cited by 69
- continuousAt_constproof · cited by 59
- continuousAt_idproof · cited by 28
- le_iff_lt_or_eqproof · cited by 26
- Real.continuousAt_rpowproof · cited by 3
- ContinuousAt.comp₂proof · cited by 3
Cited by8
Results whose statement or proof uses this declaration.
- Real.continuous_rpow_constproof · cited by 8
- contDiff_norm_rpowproof · cited by 2
- mellin_convergent_of_isBigO_scalarproof · cited by 2
- mellin_convergent_top_of_isBigOproof · cited by 1
- mellin_convergent_zero_of_isBigOproof · cited by 1
- Asymptotics.IsEquivalent.rpowproof · cited by 1
- Real.Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gammaproof · cited by 1
- WeakFEPair.hf_modif_intproof · cited by 0