Documentation Verification Report

Continuity

📁 Source: Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean

Statistics

Metric	Count
Definitions	0
Theorems `continuousAt_cpow_const_of_re_pos`, `continuousAt_cpow_of_re_pos`, `continuousAt_cpow_zero_of_re_pos`, `continuousAt_ofReal_cpow`, `continuousAt_ofReal_cpow_const`, `continuous_ofReal_cpow_const`, `const_cpow`, `cpow`, `rpow`, `rpow_const`, `const_cpow`, `cpow`, `rpow`, `rpow_const`, `const_cpow`, `cpow`, `cpow_const`, `rpow`, `rpow_const`, `const_cpow`, `cpow`, `rpow`, `rpow_const`, `continuous_rpow_const`, `eventually_pow_one_div_le`, `tendsto_const_mul_rpow_nhds_zero_of_pos`, `const_cpow`, `cpow`, `ennrpow_const`, `nnrpow`, `rpow`, `rpow_const`, `continuousAt_rpow`, `continuousAt_rpow_const`, `continuousOn_rpow_const`, `continuousOn_rpow_const_compl_zero`, `continuous_rpow_const`, `eventually_pow_one_div_le`, `continuousAt_const_rpow`, `continuousAt_const_rpow'`, `continuousAt_rpow`, `continuousAt_rpow_const`, `continuousAt_rpow_of_ne`, `continuousAt_rpow_of_pos`, `continuous_const_rpow`, `continuous_rpow_const`, `rpow_eq_nhds_of_neg`, `rpow_eq_nhds_of_pos`, `continuousAt_const_cpow`, `continuousAt_const_cpow'`, `continuousAt_cpow`, `continuousAt_cpow_const`, `continuous_const_cpow`, `cpow_eq_nhds`, `cpow_eq_nhds'`, `zero_cpow_eq_nhds`	56
Total	56

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_cpow_const_of_re_pos` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `re` `Real.instLT`	`ContinuousAt` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instPow`	—	`Filter.Tendsto.comp` `continuousAt_cpow_of_re_pos` `ContinuousAt.prodMk` `continuousAt_id` `continuousAt_const`
`continuousAt_cpow_of_re_pos` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `re` `Complex` `Real.instLT`	`ContinuousAt` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instPow`	—	`not_le_zero_iff` `not_and_or` `lt_iff_le_and_ne` `not_lt_zero_iff` `continuousAt_cpow` `continuousAt_cpow_zero_of_re_pos`
`continuousAt_cpow_zero_of_re_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `re`	`ContinuousAt` `Complex` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instPow` `instZero`	—	`LT.lt.ne'` `ContinuousAt.eq_1` `zero_cpow` `tendsto_zero_iff_norm_tendsto_zero` `squeeze_zero` `norm_nonneg` `norm_cpow_le` `div_eq_mul_inv` `Filter.Tendsto.zero_mul_isBoundedUnder_le` `norm_zero` `Real.zero_rpow` `Filter.Tendsto.rpow` `Continuous.tendsto` `Continuous.norm` `continuous_fst` `Continuous.comp` `continuous_re` `continuous_snd` `abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.exp_pos` `NoMaxOrder.exists_gt` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `Filter.eventually_map` `Filter.Eventually.mono` `Filter.Tendsto.eventually` `Continuous.abs` `instOrderTopologyReal` `continuous_im` `gt_mem_nhds` `Real.exp_le_exp` `LE.le.trans` `neg_le_abs` `abs_mul` `mul_le_mul` `IsOrderedRing.toPosMulMono` `IsOrderedRing.toMulPosMono` `abs_le` `LT.lt.le` `neg_pi_lt_arg` `arg_le_pi` `abs_nonneg` `covariant_swap_add_of_covariant_add` `Real.pi_pos`
`continuousAt_ofReal_cpow` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `re`	`ContinuousAt` `Complex` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instPow` `ofReal`	—	`lt_trichotomy` `ContinuousAt.prodMk` `ContinuousAt.comp'` `Continuous.continuousAt` `continuous_ofReal` `ContinuousAt.fst` `continuousAt_id'` `ContinuousAt.snd` `ContinuousAt.comp` `continuousAt_cpow` `ofReal_re` `ofReal_zero` `continuousAt_cpow_zero_of_re_pos` `ContinuousAt.comp_of_eq` `ContinuousAt.neg` `IsTopologicalRing.toContinuousNeg` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousAt.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `neg_re` `neg_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `ContinuousAt.cexp` `ContinuousAt.fun_mul` `continuousAt_const` `ContinuousAt.congr` `Filter.eventually_of_mem` `prod_mem_nhds` `Iio_mem_nhds` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Filter.univ_mem` `ofReal_cpow_of_nonpos` `le_of_lt`
`continuousAt_ofReal_cpow_const` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `re`	`ContinuousAt` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instPow` `ofReal`	—	`ContinuousAt.comp₂_of_eq` `continuousAt_ofReal_cpow` `continuousAt_id'` `continuousAt_const`
`continuous_ofReal_cpow_const` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `re`	`Continuous` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instPow` `ofReal`	—	`continuous_iff_continuousAt` `continuousAt_ofReal_cpow_const`

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_cpow` 📖	mathematical	`Continuous` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`Complex.instPow`	—	`continuous_iff_continuousAt` `ContinuousAt.const_cpow` `continuousAt`
`cpow` 📖	mathematical	`Continuous` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Set` `Set.instMembership` `Complex.slitPlane`	`Complex.instPow`	—	`continuous_iff_continuousAt` `ContinuousAt.cpow` `continuousAt`
`rpow` 📖	mathematical	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLT` `Real.instZero`	`Real.instPow`	—	`continuous_iff_continuousAt` `ContinuousAt.rpow` `continuousAt`
`rpow_const` 📖	mathematical	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLE` `Real.instZero`	`Real.instPow`	—	`continuous_iff_continuousAt` `ContinuousAt.rpow_const` `continuousAt`

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_cpow` 📖	mathematical	`ContinuousAt` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`Complex.instPow`	—	`Filter.Tendsto.const_cpow`
`cpow` 📖	mathematical	`ContinuousAt` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Set` `Set.instMembership` `Complex.slitPlane`	`Complex.instPow`	—	`Filter.Tendsto.cpow`
`rpow` 📖	mathematical	`ContinuousAt` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLT` `Real.instZero`	`Real.instPow`	—	`Filter.Tendsto.rpow`
`rpow_const` 📖	mathematical	`ContinuousAt` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLE` `Real.instZero`	`Real.instPow`	—	`Filter.Tendsto.rpow_const`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_cpow` 📖	mathematical	`ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`Complex.instPow`	—	`ContinuousWithinAt.const_cpow`
`cpow` 📖	mathematical	`ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Set` `Set.instMembership` `Complex.slitPlane`	`Complex.instPow`	—	`ContinuousWithinAt.cpow`
`cpow_const` 📖	mathematical	`ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Set` `Set.instMembership` `Complex.slitPlane`	`Complex.instPow`	—	`cpow` `continuousOn_const`
`rpow` 📖	mathematical	`ContinuousOn` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLT` `Real.instZero`	`Real.instPow`	—	`ContinuousWithinAt.rpow`
`rpow_const` 📖	mathematical	`ContinuousOn` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLE` `Real.instZero`	`Real.instPow`	—	`ContinuousWithinAt.rpow_const`

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_cpow` 📖	mathematical	`ContinuousWithinAt` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`Complex.instPow`	—	`Filter.Tendsto.const_cpow`
`cpow` 📖	mathematical	`ContinuousWithinAt` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Set` `Set.instMembership` `Complex.slitPlane`	`Complex.instPow`	—	`Filter.Tendsto.cpow`
`rpow` 📖	mathematical	`ContinuousWithinAt` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLT` `Real.instZero`	`Real.instPow`	—	`Filter.Tendsto.rpow`
`rpow_const` 📖	mathematical	`ContinuousWithinAt` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLE` `Real.instZero`	`Real.instPow`	—	`Filter.Tendsto.rpow_const`

ENNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_rpow_const` 📖	mathematical	—	`Continuous` `ENNReal` `instTopologicalSpace` `Real` `instPowReal`	—	`continuous_iff_continuousAt` `lt_trichotomy` `rpow_zero` `continuousAt_const` `neg_neg` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `rpow_neg` `ContinuousAt.comp` `Continuous.continuousAt` `ContinuousInv.continuous_inv` `instContinuousInv`
`eventually_pow_one_div_le` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`Filter.Eventually` `Preorder.toLE` `Real` `instPowReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instNatCast` `Filter.atTop` `Nat.instPreorder`	—	`CanLift.prf` `canLift` `Filter.Eventually.of_forall` `le_top` `NNReal.eventually_pow_one_div_le` `Nat.cast_one` `Filter.Eventually.congr` `coe_rpow_of_nonneg` `Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `coe_le_coe`
`tendsto_const_mul_rpow_nhds_zero_of_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Filter.Tendsto` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `instPowReal` `nhds` `instTopologicalSpace` `instZeroENNReal`	—	`zero_rpow_of_pos` `MulZeroClass.mul_zero` `Tendsto.const_mul` `Continuous.tendsto` `continuous_rpow_const`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_cpow` 📖	mathematical	`Filter.Tendsto` `Complex` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`Complex.instPow`	—	`comp` `ContinuousAt.tendsto` `continuousAt_const_cpow` `continuousAt_const_cpow'`
`cpow` 📖	mathematical	`Filter.Tendsto` `Complex` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Set` `Set.instMembership` `Complex.slitPlane`	`Complex.instPow`	—	`comp` `ContinuousAt.tendsto` `continuousAt_cpow` `prodMk_nhds`
`ennrpow_const` 📖	mathematical	`Filter.Tendsto` `ENNReal` `nhds` `ENNReal.instTopologicalSpace`	`Real` `ENNReal.instPowReal`	—	`comp` `Continuous.tendsto` `ENNReal.continuous_rpow_const`
`nnrpow` 📖	mathematical	`Filter.Tendsto` `NNReal` `nhds` `NNReal.instTopologicalSpace` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLT` `Real.instZero`	`NNReal.instPowReal`	—	`comp` `NNReal.continuousAt_rpow` `prodMk_nhds`
`rpow` 📖	mathematical	`Filter.Tendsto` `Real` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLT` `Real.instZero`	`Real.instPow`	—	`comp` `ContinuousAt.tendsto` `Real.continuousAt_rpow` `prodMk_nhds`
`rpow_const` 📖	mathematical	`Filter.Tendsto` `Real` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLE` `Real.instZero`	`Real.instPow`	—	`Real.rpow_zero` `rpow` `tendsto_const_nhds` `LE.le.lt_of_ne`

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_rpow` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`ContinuousAt` `NNReal` `instTopologicalSpaceProd` `instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instPowReal`	—	`eq` `Nat.cast_zero` `zero_le` `instCanonicallyOrderedAdd` `ContinuousAt.comp` `Continuous.continuousAt` `continuous_real_toNNReal` `Real.continuousAt_rpow` `ContinuousAt.prodMk` `ContinuousAt.comp'` `continuous_subtype_val` `ContinuousAt.fst` `continuousAt_id'` `ContinuousAt.snd`
`continuousAt_rpow_const` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`ContinuousAt` `NNReal` `instTopologicalSpace` `instPowReal`	—	`Filter.Tendsto.nnrpow` `Filter.tendsto_id` `tendsto_const_nhds` `LE.le.eq_or_lt` `rpow_zero`
`continuousOn_rpow_const` 📖	mathematical	`NNReal` `Set` `Set.instMembership` `instZeroNNReal` `Real` `Real.instLE` `Real.instZero`	`ContinuousOn` `instTopologicalSpace` `instPowReal`	—	`ContinuousOn.mono` `continuousOn_rpow_const_compl_zero` `Continuous.continuousOn` `continuous_rpow_const`
`continuousOn_rpow_const_compl_zero` 📖	mathematical	—	`ContinuousOn` `NNReal` `instTopologicalSpace` `Real` `instPowReal` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `instZeroNNReal`	—	`ContinuousAt.continuousWithinAt` `continuousAt_rpow_const`
`continuous_rpow_const` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Continuous` `NNReal` `instTopologicalSpace` `instPowReal`	—	`continuous_iff_continuousAt` `continuousAt_rpow_const`
`eventually_pow_one_div_le` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal`	`Filter.Eventually` `Preorder.toLE` `Real` `instPowReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instNatCast` `Filter.atTop` `Nat.instPreorder`	—	`add_one_pow_unbounded_of_pos` `instIsStrictOrderedRing` `instArchimedean` `tsub_pos_of_lt` `instCanonicallyOrderedAdd` `instOrderedSub` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `one_div` `rpow_inv_le_iff` `Nat.cast_pos` `Real.instIsOrderedRing` `Real.instNontrivial` `LT.lt.trans_le` `rpow_natCast` `LE.le.trans` `LT.lt.le` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `addLeftMono` `pow_right_mono₀` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `IsOrderedRing.toPosMulMono` `instIsOrderedRing`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_const_rpow` 📖	mathematical	—	`ContinuousAt` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instPow`	—	`ContinuousAt.comp` `Continuous.continuousAt` `Complex.continuous_re` `continuousAt_const_cpow` `Nat.cast_zero` `Complex.continuous_ofReal`
`continuousAt_const_rpow'` 📖	mathematical	—	`ContinuousAt` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instPow`	—	`ContinuousAt.comp` `Continuous.continuousAt` `Complex.continuous_re` `continuousAt_const_cpow'` `Nat.cast_zero` `Complex.continuous_ofReal`
`continuousAt_rpow` 📖	mathematical	`Real` `instLT` `instZero`	`ContinuousAt` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instPow`	—	`continuousAt_rpow_of_ne` `continuousAt_rpow_of_pos`
`continuousAt_rpow_const` 📖	mathematical	`Real` `instLE` `instZero`	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instPow`	—	`le_iff_lt_or_eq` `ContinuousAt.comp₂` `continuousAt_rpow` `continuousAt_id` `continuousAt_const` `rpow_zero`
`continuousAt_rpow_of_ne` 📖	mathematical	—	`ContinuousAt` `Real` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instPow`	—	`ne_iff_lt_or_gt` `continuousAt_congr` `rpow_eq_nhds_of_neg` `ContinuousAt.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousAt.comp` `Continuous.continuousAt` `continuous_exp` `continuousAt_log` `LT.lt.ne` `continuous_fst` `continuous_snd` `ContinuousAt.comp'` `continuous_cos` `ContinuousAt.fun_mul` `ContinuousAt.snd` `continuousAt_id'` `continuousAt_const` `rpow_eq_nhds_of_pos` `LT.lt.ne'`
`continuousAt_rpow_of_pos` 📖	mathematical	`Real` `instLT` `instZero`	`ContinuousAt` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instPow`	—	`ne_or_eq` `continuousAt_rpow_of_ne` `Filter.Tendsto.comp` `tendsto_exp_atBot` `Filter.Tendsto.atBot_mul_pos` `instIsStrictOrderedRing` `instOrderTopologyReal` `tendsto_log_nhdsNE_zero` `Filter.tendsto_fst` `Filter.tendsto_snd` `squeeze_zero_norm` `abs_rpow_le_exp_log_mul` `nhdsWithin_singleton` `Filter.tendsto_pure` `Filter.pure_prod` `Filter.eventually_map` `Filter.Eventually.mono` `lt_mem_nhds` `zero_rpow` `LT.lt.ne'` `nhds_prod_eq` `Set.compl_union_self` `nhdsWithin_univ` `Filter.Tendsto.sup` `Filter.Tendsto.mono_right` `pure_le_nhds`
`continuous_const_rpow` 📖	mathematical	—	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instPow`	—	`continuous_iff_continuousAt` `continuousAt_const_rpow`
`continuous_rpow_const` 📖	mathematical	`Real` `instLE` `instZero`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instPow`	—	`continuous_iff_continuousAt` `continuousAt_rpow_const`
`rpow_eq_nhds_of_neg` 📖	mathematical	`Real` `instLT` `instZero`	`Filter.EventuallyEq` `nhds` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instPow` `instMul` `exp` `log` `cos` `pi`	—	`IsOpen.eventually_mem` `isOpen_lt` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `instIsOrderedAddMonoid` `continuous_fst` `continuous_const` `Filter.Eventually.mono` `rpow_def_of_neg`
`rpow_eq_nhds_of_pos` 📖	mathematical	`Real` `instLT` `instZero`	`Filter.EventuallyEq` `nhds` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instPow` `exp` `instMul` `log`	—	`IsOpen.eventually_mem` `isOpen_lt` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `instIsOrderedAddMonoid` `continuous_const` `continuous_fst` `Filter.Eventually.mono` `rpow_def_of_pos`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_const_cpow` 📖	mathematical	—	`ContinuousAt` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instPow`	—	`Complex.cpow_def_of_ne_zero` `ContinuousAt.comp` `Continuous.continuousAt` `Complex.continuous_exp` `ContinuousAt.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `continuousAt_const` `continuousAt_id`
`continuousAt_const_cpow'` 📖	mathematical	—	`ContinuousAt` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instPow`	—	`continuousAt_congr` `zero_cpow_eq_nhds` `continuousAt_const` `continuousAt_const_cpow`
`continuousAt_cpow` 📖	mathematical	`Complex` `Set` `Set.instMembership` `Complex.slitPlane`	`ContinuousAt` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instPow`	—	`continuousAt_congr` `cpow_eq_nhds'` `Complex.slitPlane_ne_zero` `ContinuousAt.comp` `Continuous.continuousAt` `Complex.continuous_exp` `ContinuousAt.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `continuousAt_clog` `continuous_fst` `continuous_snd`
`continuousAt_cpow_const` 📖	mathematical	`Complex` `Set` `Set.instMembership` `Complex.slitPlane`	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instPow`	—	`Filter.Tendsto.comp` `continuousAt_cpow` `ContinuousAt.prodMk` `continuousAt_id` `continuousAt_const`
`continuous_const_cpow` 📖	mathematical	—	`Continuous` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instPow`	—	`Continuous.const_cpow` `continuous_id`
`cpow_eq_nhds` 📖	mathematical	—	`Filter.EventuallyEq` `Complex` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instPow` `Complex.exp` `Complex.instMul` `Complex.log`	—	`IsOpen.eventually_mem` `isOpen_ne` `T2Space.t1Space` `Complex.instT2Space` `Filter.Eventually.mono` `Complex.cpow_def_of_ne_zero`
`cpow_eq_nhds'` 📖	mathematical	—	`Filter.EventuallyEq` `Complex` `nhds` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instPow` `Complex.exp` `Complex.instMul` `Complex.log`	—	`IsOpen.eventually_mem` `isOpen_compl_iff` `isClosed_eq` `Complex.instT2Space` `continuous_fst` `continuous_const` `Filter.Eventually.mono` `Complex.cpow_def_of_ne_zero`
`zero_cpow_eq_nhds` 📖	mathematical	—	`Filter.EventuallyEq` `Complex` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instPow` `Complex.instZero` `Pi.instZero`	—	`IsOpen.eventually_mem` `isOpen_ne` `T2Space.t1Space` `Complex.instT2Space` `Filter.Eventually.mono` `Complex.zero_cpow` `Pi.zero_apply`

---

← Back to Index