Documentation Verification Report

CPolynomialDef

📁 Source: Mathlib/Analysis/Analytic/CPolynomialDef.lean

Statistics

Metric	Count
Definitions `CPolynomialAt`, `CPolynomialOn`, `HasFiniteFPowerSeriesAt`, `HasFiniteFPowerSeriesOnBall`	4
Theorems `analyticAt`, `analyticWithinAt`, `continuousAt`, `eventually_cpolynomialAt`, `exists_ball_cpolynomialOn`, `exists_mem_nhds_cpolynomialOn`, `CPolynomialAt_congr`, `analyticOn`, `analyticOnNhd`, `congr'`, `continuous`, `continuousOn`, `mono`, `CPolynomialOn_congr`, `CPolynomialOn_congr'`, `comp_cpolynomialOn`, `comp_hasFiniteFPowerSeriesOnBall`, `changeOriginSeriesTerm_bound`, `changeOriginSeries_finite_of_finite`, `changeOriginSeries_sum_eq_partialSum_of_finite`, `changeOrigin_eval_of_finite`, `changeOrigin_finite_of_finite`, `continuousOn_of_finite`, `cpolynomialAt_changeOrigin_of_finite`, `hasFiniteFPowerSeriesOnBall_changeOrigin`, `hasFiniteFPowerSeriesOnBall_of_finite`, `hasSum_of_finite`, `sum_of_finite`, `continuousAt`, `cpolynomialAt`, `eventually`, `eventually_const_of_bound_one`, `eventually_zero_of_bound_zero`, `finite`, `hasFPowerSeriesAt`, `of_le`, `bound_zero_of_eq_zero`, `changeOrigin`, `comp_sub`, `continuousOn`, `cpolynomialAt`, `cpolynomialAt_of_mem`, `cpolynomialOn`, `eq_const_of_bound_one`, `eq_partialSum`, `eq_partialSum'`, `eq_zero_of_bound_zero`, `finite`, `hasFiniteFPowerSeriesAt`, `mk'`, `mono`, `of_le`, `sum`, `toHasFPowerSeriesOnBall`, `isOpen_cpolynomialAt`	55
Total	59

CPolynomialAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticAt` 📖	mathematical	`CPolynomialAt`	`AnalyticAt`	—	`HasFiniteFPowerSeriesAt.hasFPowerSeriesAt`
`analyticWithinAt` 📖	mathematical	`CPolynomialAt`	`AnalyticWithinAt`	—	`AnalyticAt.analyticWithinAt` `analyticAt`
`continuousAt` 📖	mathematical	`CPolynomialAt`	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`AnalyticAt.continuousAt` `analyticAt`
`eventually_cpolynomialAt` 📖	mathematical	`CPolynomialAt`	`Filter.Eventually` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`IsOpen.mem_nhds` `isOpen_cpolynomialAt`
`exists_ball_cpolynomialOn` 📖	mathematical	`CPolynomialAt`	`Real` `Real.instLT` `Real.instZero` `CPolynomialOn` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`Metric.isOpen_iff` `isOpen_cpolynomialAt`
`exists_mem_nhds_cpolynomialOn` 📖	mathematical	`CPolynomialAt`	`Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `CPolynomialOn`	—	`Filter.Eventually.exists_mem` `eventually_cpolynomialAt`

CPolynomialOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticOn` 📖	mathematical	`CPolynomialOn`	`AnalyticOn`	—	`AnalyticOnNhd.analyticOn` `analyticOnNhd`
`analyticOnNhd` 📖	mathematical	`CPolynomialOn`	`AnalyticOnNhd`	—	`CPolynomialAt.analyticAt`
`congr'` 📖	—	`CPolynomialOn` `Filter.EventuallyEq` `nhdsSet` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`CPolynomialAt.congr` `mem_nhdsSet_iff_forall`
`continuous` 📖	mathematical	`CPolynomialOn` `Set.univ`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`continuousOn_univ` `continuousOn`
`continuousOn` 📖	mathematical	`CPolynomialOn`	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`AnalyticOnNhd.continuousOn` `analyticOnNhd`
`mono` 📖	—	`CPolynomialOn` `Set` `Set.instHasSubset`	—	—	—

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_cpolynomialOn` 📖	mathematical	`CPolynomialOn`	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `funLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `comp_hasFiniteFPowerSeriesOnBall`
`comp_hasFiniteFPowerSeriesOnBall` 📖	mathematical	`HasFiniteFPowerSeriesOnBall`	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `funLike` `compFormalMultilinearSeries` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `comp_hasFPowerSeriesOnBall` `HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall` `compFormalMultilinearSeries_apply` `HasFiniteFPowerSeriesOnBall.finite` `ContinuousMultilinearMap.ext` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `continuousSemilinearMapClass`

FormalMultilinearSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`changeOriginSeriesTerm_bound` 📖	mathematical	`ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instZero` `Finset.card`	`changeOriginSeriesTerm` `ContinuousMultilinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousMultilinearMap.instModule` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousMultilinearMap.instTopologicalSpace` `SeminormedAddCommGroup.toAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `changeOriginSeriesTerm.eq_1` `map_zero` `AddMonoidHomClass.toZeroHomClass` `ContinuousMultilinearMap.instIsTopologicalAddGroup` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `SemilinearIsometryEquivClass.toSemilinearIsometryClass` `LinearIsometryEquiv.instSemilinearIsometryEquivClass`
`changeOriginSeries_finite_of_finite` 📖	mathematical	`ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instZero`	`changeOriginSeries` `ContinuousMultilinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousMultilinearMap.instModule` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousMultilinearMap.instTopologicalSpace` `SeminormedAddCommGroup.toAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `changeOriginSeries.eq_1` `Finset.sum_eq_zero` `changeOriginSeriesTerm_bound`
`changeOriginSeries_sum_eq_partialSum_of_finite` 📖	mathematical	`ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instZero`	`sum` `ContinuousMultilinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousMultilinearMap.instModule` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousMultilinearMap.instTopologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.instIsTopologicalAddGroup` `ContinuousMultilinearMap.instContinuousConstSMul` `changeOriginSeries` `partialSum`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `ContinuousMultilinearMap.instIsTopologicalAddGroup` `ContinuousMultilinearMap.instContinuousConstSMul` `ContinuousMultilinearMap.ext` `partialSum.eq_1` `sum.eq_1` `tsum_eq_sum` `SummationFilter.instLeAtTopUnconditional` `changeOriginSeries_finite_of_finite` `add_comm` `not_lt` `Finset.mem_range` `ContinuousMultilinearMap.zero_apply`
`changeOrigin_eval_of_finite` 📖	mathematical	`ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instZero`	`sum` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `changeOrigin` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `Set.Finite.subset` `Set.Finite.preimage` `Function.Injective.injOn` `Equiv.injective` `Set.iUnion_of_singleton_coe` `Set.preimage_iUnion` `Set.finite_iUnion` `Finite.of_fintype` `Set.finite_range` `Not.imp_symm` `changeOriginSeriesTerm_bound` `ContinuousMultilinearMap.zero_apply` `ContinuousMultilinearMap.sum_apply` `hasSum_fintype` `SummationFilter.instLeAtTopUnconditional` `changeOriginSeries_finite_of_finite` `le_add_of_le_right` `Nat.instCanonicallyOrderedAdd` `not_lt` `Finset.mem_range` `changeOrigin.eq_1` `sum.eq_1` `ContinuousMultilinearMap.tsum_eval` `IsBoundedSMul.continuousSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `summable_of_ne_finset_zero` `SummationFilter.instHasSupportOfLeAtTop` `HasSum.sigma_of_hasSum` `T4Space.t3Space` `instT4SpaceOfT1SpaceOfNormalSpace` `T2Space.t1Space` `CompletelyNormalSpace.toNormalSpace` `UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity` `EMetric.instIsCountablyGeneratedUniformity` `Summable.hasSum` `summable_of_finite_support` `sigma_mk_injective` `hasSum_of_finite` `changeOrigin_finite_of_finite` `HasSum.unique` `SummationFilter.instNeBotUnconditional` `Equiv.hasSum_iff` `Pi.add_def` `ContinuousMultilinearMap.map_add_univ` `Finset.sum_congr` `Equiv.summable_iff` `HasSum.summable`
`changeOrigin_finite_of_finite` 📖	mathematical	`ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instZero`	`changeOrigin`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `changeOrigin.eq_1` `smulCommClass_self` `ContinuousMultilinearMap.instIsTopologicalAddGroup` `ContinuousMultilinearMap.instContinuousConstSMul` `changeOriginSeries_sum_eq_partialSum_of_finite` `Finset.sum_eq_zero` `changeOriginSeries_finite_of_finite` `le_add_of_le_left` `Nat.instCanonicallyOrderedAdd` `ContinuousMultilinearMap.zero_apply`
`continuousOn_of_finite` 📖	mathematical	`ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instZero`	`Continuous` `sum` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `continuousOn_univ` `Metric.eball_top` `HasFiniteFPowerSeriesOnBall.continuousOn` `hasFiniteFPowerSeriesOnBall_of_finite`
`cpolynomialAt_changeOrigin_of_finite` 📖	mathematical	`ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instZero`	`CPolynomialAt` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `changeOrigin` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFiniteFPowerSeriesOnBall.cpolynomialAt` `smulCommClass_self` `hasFiniteFPowerSeriesOnBall_changeOrigin` `LE.le.trans` `le_self_add` `Nat.instCanonicallyOrderedAdd`
`hasFiniteFPowerSeriesOnBall_changeOrigin` 📖	mathematical	`ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instZero`	`HasFiniteFPowerSeriesOnBall` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `changeOrigin` `changeOriginSeries` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Top.top` `ENNReal` `instTopENNReal`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `hasFiniteFPowerSeriesOnBall_of_finite` `smulCommClass_self` `changeOriginSeries_finite_of_finite` `le_imp_le_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `le_refl` `add_comm`
`hasFiniteFPowerSeriesOnBall_of_finite` 📖	mathematical	`ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instZero`	`HasFiniteFPowerSeriesOnBall` `sum` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `Top.top` `ENNReal` `instTopENNReal`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `radius_eq_top_of_forall_image_add_eq_zero` `le_refl` `ENNReal.zero_lt_top` `zero_add` `hasSum_of_finite`
`hasSum_of_finite` 📖	mathematical	`ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instZero`	`HasSum` `DFunLike.coe` `ContinuousMultilinearMap.funLike` `sum` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `SummationFilter.unconditional`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Summable.hasSum` `summable_of_ne_finset_zero` `not_lt` `Finset.mem_range` `SummationFilter.instHasSupportOfLeAtTop` `SummationFilter.instLeAtTopUnconditional`
`sum_of_finite` 📖	mathematical	`ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instZero`	`sum` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `partialSum`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `tsum_eq_sum` `SummationFilter.instLeAtTopUnconditional` `not_lt` `Finset.mem_range`

HasFiniteFPowerSeriesAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt` 📖	mathematical	`HasFiniteFPowerSeriesAt`	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesAt.continuousAt` `hasFPowerSeriesAt`
`cpolynomialAt` 📖	mathematical	`HasFiniteFPowerSeriesAt`	`CPolynomialAt`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`eventually` 📖	mathematical	`HasFiniteFPowerSeriesAt`	`Filter.Eventually` `ENNReal` `HasFiniteFPowerSeriesOnBall` `nhdsWithin` `ENNReal.instTopologicalSpace` `instZeroENNReal` `Set.Ioi` `PartialOrder.toPreorder` `ENNReal.instPartialOrder`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Filter.Eventually.mono` `HasFPowerSeriesAt.eventually` `hasFPowerSeriesAt` `finite`
`eventually_const_of_bound_one` 📖	mathematical	`HasFiniteFPowerSeriesAt`	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Filter.eventuallyEq_iff_exists_mem` `Metric.eball_mem_nhds` `HasFPowerSeriesOnBall.r_pos` `HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall` `HasFiniteFPowerSeriesOnBall.eq_const_of_bound_one`
`eventually_zero_of_bound_zero` 📖	mathematical	`HasFiniteFPowerSeriesAt`	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Filter.eventuallyEq_iff_exists_mem` `Metric.eball_mem_nhds` `HasFPowerSeriesOnBall.r_pos` `HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall` `HasFiniteFPowerSeriesOnBall.eq_zero_of_bound_zero`
`finite` 📖	mathematical	`HasFiniteFPowerSeriesAt`	`ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instZero`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFiniteFPowerSeriesOnBall.finite`
`hasFPowerSeriesAt` 📖	mathematical	`HasFiniteFPowerSeriesAt`	`HasFPowerSeriesAt`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall`
`of_le` 📖	—	`HasFiniteFPowerSeriesAt`	—	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFiniteFPowerSeriesOnBall.of_le`

HasFiniteFPowerSeriesOnBall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bound_zero_of_eq_zero` 📖	mathematical	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instZero`	`HasFiniteFPowerSeriesOnBall`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero` `add_zero` `le_top` `Metric.mem_eball` `edist_eq_enorm_sub` `add_comm` `add_sub_cancel_right` `edist_zero_right` `ContinuousMultilinearMap.zero_apply` `hasSum_zero`
`changeOrigin` 📖	mathematical	`HasFiniteFPowerSeriesOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup`	`FormalMultilinearSeries.changeOrigin` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ENNReal.instSub`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `LE.le.trans` `tsub_le_tsub_right` `ENNReal.instOrderedSub` `HasFPowerSeriesOnBall.r_le` `toHasFPowerSeriesOnBall` `FormalMultilinearSeries.changeOrigin_radius` `ENNReal.instCanonicallyOrderedAdd` `FormalMultilinearSeries.changeOrigin_eval_of_finite` `finite` `add_assoc` `sum` `mem_eball_zero_iff` `LE.le.trans_lt` `enorm_add_le` `add_comm` `lt_tsub_iff_right` `FormalMultilinearSeries.hasSum_of_finite` `FormalMultilinearSeries.changeOrigin_finite_of_finite`
`comp_sub` 📖	mathematical	`HasFiniteFPowerSeriesOnBall`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesOnBall.comp_sub` `toHasFPowerSeriesOnBall` `finite`
`continuousOn` 📖	mathematical	`HasFiniteFPowerSeriesOnBall`	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesOnBall.continuousOn` `toHasFPowerSeriesOnBall`
`cpolynomialAt` 📖	mathematical	`HasFiniteFPowerSeriesOnBall`	`CPolynomialAt`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFiniteFPowerSeriesAt.cpolynomialAt` `hasFiniteFPowerSeriesAt`
`cpolynomialAt_of_mem` 📖	mathematical	`HasFiniteFPowerSeriesOnBall` `Set` `Set.instMembership` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	`CPolynomialAt`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `edist_eq_enorm_sub` `changeOrigin` `cpolynomialAt` `add_sub_cancel`
`cpolynomialOn` 📖	mathematical	`HasFiniteFPowerSeriesOnBall`	`CPolynomialOn` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `cpolynomialAt_of_mem`
`eq_const_of_bound_one` 📖	—	`HasFiniteFPowerSeriesOnBall` `Set` `Set.instMembership` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `eq_partialSum'` `le_rfl` `Metric.mem_eball` `PseudoEMetricSpace.edist_self` `HasFPowerSeriesOnBall.r_pos` `toHasFPowerSeriesOnBall` `Finset.sum_singleton` `Fin.isEmpty'`
`eq_partialSum` 📖	mathematical	`HasFiniteFPowerSeriesOnBall` `Set` `Set.instMembership` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `FormalMultilinearSeries.partialSum` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toIsBoundedSMul`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasSum.unique` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `HasFPowerSeriesOnBall.hasSum` `toHasFPowerSeriesOnBall` `hasSum_sum_of_ne_finset_zero` `finite` `le_trans` `ContinuousMultilinearMap.zero_apply` `SummationFilter.instLeAtTopUnconditional`
`eq_partialSum'` 📖	mathematical	`HasFiniteFPowerSeriesOnBall` `Set` `Set.instMembership` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	`FormalMultilinearSeries.partialSum` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `eq_partialSum` `mem_eball_zero_iff` `edist_eq_enorm_sub` `Metric.mem_eball` `add_sub_cancel`
`eq_zero_of_bound_zero` 📖	mathematical	`HasFiniteFPowerSeriesOnBall` `Set` `Set.instMembership` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `eq_partialSum'` `le_rfl` `FormalMultilinearSeries.partialSum.eq_1`
`finite` 📖	mathematical	`HasFiniteFPowerSeriesOnBall`	`ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instZero`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`hasFiniteFPowerSeriesAt` 📖	mathematical	`HasFiniteFPowerSeriesOnBall`	`HasFiniteFPowerSeriesAt`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`mk'` 📖	mathematical	`ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instZero` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `Finset.sum` `Finset.range` `DFunLike.coe` `ContinuousMultilinearMap.funLike` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`HasFiniteFPowerSeriesOnBall`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `le_top` `FormalMultilinearSeries.radius_eq_top_of_eventually_eq_zero` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `hasSum_sum_of_ne_finset_zero` `not_lt` `Finset.mem_range` `SummationFilter.instLeAtTopUnconditional`
`mono` 📖	—	`HasFiniteFPowerSeriesOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `Preorder.toLE`	—	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesOnBall.mono` `toHasFPowerSeriesOnBall` `finite`
`of_le` 📖	—	`HasFiniteFPowerSeriesOnBall`	—	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `toHasFPowerSeriesOnBall` `finite` `LE.le.trans`
`sum` 📖	mathematical	`HasFiniteFPowerSeriesOnBall` `Set` `Set.instMembership` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `FormalMultilinearSeries.sum` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toIsBoundedSMul`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `HasFPowerSeriesOnBall.hasSum` `toHasFPowerSeriesOnBall`
`toHasFPowerSeriesOnBall` 📖	mathematical	`HasFiniteFPowerSeriesOnBall`	`HasFPowerSeriesOnBall`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`

(root)

Definitions

Name	Category	Theorems
`CPolynomialAt` 📖	MathDef	12 math math: `ContinuousLinearMap.cpolynomialAt`, `isOpen_cpolynomialAt`, `HasFiniteFPowerSeriesOnBall.cpolynomialAt`, `FormalMultilinearSeries.cpolynomialAt_changeOrigin_of_finite`, `ContinuousLinearMap.cpolynomialAt_uncurry_of_multilinear`, `ContinuousMultilinearMap.cpolynomialAt_uncurry_of_linear`, `ContinuousMultilinearMap.cpolynomialAt`, `HasFiniteFPowerSeriesOnBall.cpolynomialAt_of_mem`, `HasFiniteFPowerSeriesAt.cpolynomialAt`, `CPolynomialAt_congr`, `CPolynomialAt_const`, `ContinuousMultilinearMap.cpolynomialAt_uncurry_compContinuousLinearMap`
`CPolynomialOn` 📖	MathDef	12 math math: `ContinuousMultilinearMap.cpolynomialOn`, `ContinuousLinearMap.cpolynomialOn_uncurry_of_multilinear`, `HasFiniteFPowerSeriesOnBall.cpolynomialOn`, `CPolynomialAt.exists_mem_nhds_cpolynomialOn`, `CPolynomialOn_congr`, `ContinuousLinearMap.cpolyomialOn_uncurry_of_multilinear`, `ContinuousMultilinearMap.cpolyomialOn_uncurry_of_linear`, `CPolynomialAt.exists_ball_cpolynomialOn`, `ContinuousMultilinearMap.cpolynomialOn_uncurry_compContinuousLinearMap`, `CPolynomialOn_const`, `ContinuousLinearMap.cpolynomialOn`, `CPolynomialOn_congr'`
`HasFiniteFPowerSeriesAt` 📖	MathDef	2 math math: `HasFiniteFPowerSeriesOnBall.hasFiniteFPowerSeriesAt`, `hasFiniteFPowerSeriesAt_const`
`HasFiniteFPowerSeriesOnBall` 📖	CompData	9 math math: `FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_changeOrigin`, `HasFiniteFPowerSeriesOnBall.bound_zero_of_eq_zero`, `ContinuousLinearMap.hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear`, `ContinuousMultilinearMap.hasFiniteFPowerSeriesOnBall`, `ContinuousLinearMap.hasFiniteFPowerSeriesOnBall`, `hasFiniteFPowerSeriesOnBall_const`, `HasFiniteFPowerSeriesOnBall.mk'`, `FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_of_finite`, `HasFiniteFPowerSeriesAt.eventually`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`CPolynomialAt_congr` 📖	mathematical	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`CPolynomialAt`	—	`CPolynomialAt.congr` `Filter.EventuallyEq.symm`
`CPolynomialOn_congr` 📖	mathematical	`IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.EqOn`	`CPolynomialOn`	—	`CPolynomialOn.congr` `Set.EqOn.symm`
`CPolynomialOn_congr'` 📖	mathematical	`Filter.EventuallyEq` `nhdsSet` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`CPolynomialOn`	—	`CPolynomialOn.congr'` `Filter.EventuallyEq.symm`
`isOpen_cpolynomialAt` 📖	mathematical	—	`IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `setOf` `CPolynomialAt`	—	`isOpen_iff_mem_nhds` `Filter.mem_of_superset` `Metric.eball_mem_nhds` `HasFPowerSeriesOnBall.r_pos` `HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall` `HasFiniteFPowerSeriesOnBall.cpolynomialAt_of_mem`

---

← Back to Index