Basic

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

Statistics

Metric	Count
Definitions `AnalyticAt`, `AnalyticOn`, `AnalyticOnNhd`, `AnalyticWithinAt`, `HasFPowerSeriesAt`, `HasFPowerSeriesOnBall`, `HasFPowerSeriesWithinAt`, `HasFPowerSeriesWithinOnBall`	8
Theorems `analyticWithinAt`, `comp_sub`, `continuousAt`, `eventually_continuousAt`, `analyticAt`, `comp_sub`, `continuousOn`, `mono`, `analyticOn`, `comp_sub`, `congr'`, `continuous`, `continuousOn`, `mono`, `comp_sub`, `congr_of_eventuallyEq`, `congr_of_eventuallyEq_insert`, `congr_set`, `continuousWithinAt`, `continuousWithinAt_insert`, `mono`, `mono_of_mem_nhdsWithin`, `comp_analyticOn`, `comp_analyticOnNhd`, `comp_hasFPowerSeriesOnBall`, `comp_hasFPowerSeriesWithinOnBall`, `continuousOn`, `hasFPowerSeriesOnBall`, `analyticAt`, `coeff_zero`, `comp_sub`, `continuousAt`, `eventually`, `eventually_eq_zero`, `eventually_hasSum`, `eventually_hasSum_sub`, `hasFPowerSeriesWithinAt`, `isBigO_image_sub_norm_mul_norm_sub`, `isBigO_sub_partialSum_pow`, `radius_pos`, `tendsto_partialSum`, `analyticAt`, `coeff_zero`, `comp_sub`, `continuousOn`, `eventually_eq_zero`, `eventually_hasSum`, `eventually_hasSum_sub`, `hasFPowerSeriesAt`, `hasFPowerSeriesWithinOnBall`, `hasSum`, `hasSum_sub`, `image_sub_sub_deriv_le`, `isBigO_image_sub_image_sub_deriv_principal`, `mono`, `r_le`, `r_pos`, `radius_pos`, `sum`, `tendstoLocallyUniformlyOn`, `tendstoLocallyUniformlyOn'`, `tendstoUniformlyOn`, `tendstoUniformlyOn'`, `tendsto_partialSum`, `tendsto_partialSum_prod`, `uniform_geometric_approx`, `uniform_geometric_approx'`, `unique`, `analyticWithinAt`, `coeff_zero`, `comp_sub`, `continuousWithinAt`, `continuousWithinAt_insert`, `eventually`, `isBigO_image_sub_norm_mul_norm_sub`, `isBigO_sub_partialSum_pow`, `mono`, `mono_of_mem_nhdsWithin`, `analyticWithinAt`, `coeff_zero`, `comp_sub`, `congr'`, `continuousOn`, `continuousWithinAt`, `continuousWithinAt_insert`, `hasFPowerSeriesWithinAt`, `hasSum`, `hasSum_sub`, `image_sub_sub_deriv_le`, `isBigO_image_sub_image_sub_deriv_principal`, `mono`, `of_le`, `r_le`, `r_pos`, `radius_pos`, `sum`, `tendstoLocallyUniformlyOn`, `tendstoLocallyUniformlyOn'`, `tendstoUniformlyOn`, `tendstoUniformlyOn'`, `tendsto_partialSum`, `tendsto_partialSum_prod`, `uniform_geometric_approx`, `uniform_geometric_approx'`, `unique`, `analyticAt_congr`, `analyticOnNhd_congr`, `analyticOnNhd_congr'`, `analyticOnNhd_empty`, `analyticOn_congr`, `analyticOn_empty`, `analyticOn_univ`, `analyticWithinAt_insert`, `analyticWithinAt_univ`, `hasFPowerSeriesAt_iff`, `hasFPowerSeriesAt_iff'`, `hasFPowerSeriesWithinAt_iff_of_nhds`, `hasFPowerSeriesWithinAt_insert`, `hasFPowerSeriesWithinAt_univ`, `hasFPowerSeriesWithinOnBall_insert_self`, `hasFPowerSeriesWithinOnBall_univ`	121
Total	129

AnalyticAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticWithinAt` 📖	mathematical	`AnalyticAt`	`AnalyticWithinAt`	—	`AnalyticWithinAt.mono` `analyticWithinAt_univ` `Set.subset_univ`
`comp_sub` 📖	mathematical	`AnalyticAt`	`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`	—	`HasFPowerSeriesAt.comp_sub`
`continuousAt` 📖	mathematical	`AnalyticAt`	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`HasFPowerSeriesAt.continuousAt`
`eventually_continuousAt` 📖	mathematical	`AnalyticAt`	`Filter.Eventually` `ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `nhds`	—	`Metric.eball_mem_nhds` `HasFPowerSeriesOnBall.r_pos` `Filter.mp_mem` `Filter.univ_mem'` `ContinuousOn.continuousAt` `HasFPowerSeriesOnBall.continuousOn` `IsOpen.mem_nhds` `Metric.isOpen_eball`

AnalyticOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticAt` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AnalyticOn`	`AnalyticAt`	—	`mem_of_mem_nhds` `hasFPowerSeriesWithinAt_iff_of_nhds`
`comp_sub` 📖	mathematical	`AnalyticOn`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Set` `Set.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Set.instSingletonSet`	—	`Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Abel.zero_termg` `AnalyticWithinAt.comp_sub` `Set.add_singleton` `Set.image_add_right`
`continuousOn` 📖	mathematical	`AnalyticOn`	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`AnalyticWithinAt.continuousWithinAt`
`mono` 📖	—	`AnalyticOn` `Set` `Set.instHasSubset`	—	—	`AnalyticWithinAt.mono`

AnalyticOnNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticOn` 📖	mathematical	`AnalyticOnNhd`	`AnalyticOn`	—	`AnalyticAt.analyticWithinAt`
`comp_sub` 📖	mathematical	`AnalyticOnNhd`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Set` `Set.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Set.instSingletonSet`	—	`Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Abel.zero_termg` `AnalyticAt.comp_sub` `Set.add_singleton` `Set.image_add_right`
`congr'` 📖	—	`AnalyticOnNhd` `Filter.EventuallyEq` `nhdsSet` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`AnalyticAt.congr` `mem_nhdsSet_iff_forall`
`continuous` 📖	mathematical	`AnalyticOnNhd` `Set.univ`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`continuousOn_univ` `continuousOn`
`continuousOn` 📖	mathematical	`AnalyticOnNhd`	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`ContinuousAt.continuousWithinAt` `AnalyticAt.continuousAt`
`mono` 📖	—	`AnalyticOnNhd` `Set` `Set.instHasSubset`	—	—	—

AnalyticWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_sub` 📖	mathematical	`AnalyticWithinAt`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Set` `Set.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Set.instSingletonSet`	—	`HasFPowerSeriesWithinAt.comp_sub`
`congr_of_eventuallyEq` 📖	—	`AnalyticWithinAt` `Filter.EventuallyEq` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`HasFPowerSeriesWithinAt.congr`
`congr_of_eventuallyEq_insert` 📖	—	`AnalyticWithinAt` `Filter.EventuallyEq` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instInsert`	—	—	`congr_of_eventuallyEq` `nhdsWithin_mono` `Set.subset_insert` `mem_of_mem_nhdsWithin` `Set.mem_insert`
`congr_set` 📖	—	`AnalyticWithinAt` `Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`mono_of_mem_nhdsWithin` `nhdsWithin_eq_iff_eventuallyEq`
`continuousWithinAt` 📖	mathematical	`AnalyticWithinAt`	`ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`ContinuousWithinAt.mono` `continuousWithinAt_insert` `Set.subset_insert`
`continuousWithinAt_insert` 📖	mathematical	`AnalyticWithinAt`	`ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instInsert`	—	`HasFPowerSeriesWithinAt.continuousWithinAt_insert`
`mono` 📖	—	`AnalyticWithinAt` `Set` `Set.instHasSubset`	—	—	`HasFPowerSeriesWithinAt.mono`
`mono_of_mem_nhdsWithin` 📖	—	`AnalyticWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`HasFPowerSeriesWithinAt.mono_of_mem_nhdsWithin`

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_analyticOn` 📖	mathematical	`AnalyticOn`	`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_hasFPowerSeriesWithinOnBall`
`comp_analyticOnNhd` 📖	mathematical	`AnalyticOnNhd`	`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_hasFPowerSeriesOnBall`
`comp_hasFPowerSeriesOnBall` 📖	mathematical	`HasFPowerSeriesOnBall`	`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` `hasFPowerSeriesWithinOnBall_univ` `comp_hasFPowerSeriesWithinOnBall`
`comp_hasFPowerSeriesWithinOnBall` 📖	mathematical	`HasFPowerSeriesWithinOnBall`	`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` `LE.le.trans` `HasFPowerSeriesWithinOnBall.r_le` `FormalMultilinearSeries.radius_le_radius_continuousLinearMap_comp` `HasFPowerSeriesWithinOnBall.r_pos` `compContinuousMultilinearMap_coe` `hasSum` `HasFPowerSeriesWithinOnBall.hasSum`

FormalMultilinearSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousOn` 📖	mathematical	—	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `sum` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `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` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `radius`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `LE.le.eq_or_lt` `zero_le` `ENNReal.instCanonicallyOrderedAdd` `Metric.eball_zero` `HasFPowerSeriesOnBall.continuousOn` `hasFPowerSeriesOnBall`
`hasFPowerSeriesOnBall` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `radius`	`HasFPowerSeriesOnBall` `sum` `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`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `le_rfl` `zero_add` `hasSum`

HasFPowerSeriesAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticAt` 📖	mathematical	`HasFPowerSeriesAt`	`AnalyticAt`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`coeff_zero` 📖	mathematical	`HasFPowerSeriesAt`	`DFunLike.coe` `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.funLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesOnBall.coeff_zero`
`comp_sub` 📖	mathematical	`HasFPowerSeriesAt`	`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`
`continuousAt` 📖	mathematical	`HasFPowerSeriesAt`	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousOn.continuousAt` `HasFPowerSeriesOnBall.continuousOn` `Metric.eball_mem_nhds` `HasFPowerSeriesOnBall.r_pos`
`eventually` 📖	mathematical	`HasFPowerSeriesAt`	`Filter.Eventually` `ENNReal` `HasFPowerSeriesOnBall` `nhdsWithin` `ENNReal.instTopologicalSpace` `instZeroENNReal` `Set.Ioi` `PartialOrder.toPreorder` `ENNReal.instPartialOrder`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Filter.mem_of_superset` `Ioo_mem_nhdsGT` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `HasFPowerSeriesOnBall.r_pos` `HasFPowerSeriesOnBall.mono` `LT.lt.le`
`eventually_eq_zero` 📖	mathematical	`HasFPowerSeriesAt` `FormalMultilinearSeries` `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` `FormalMultilinearSeries.instAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.toAddCommGroup`	`Filter.Eventually` `nhds`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesOnBall.eventually_eq_zero`
`eventually_hasSum` 📖	mathematical	`HasFPowerSeriesAt`	`Filter.Eventually` `HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule` `ContinuousMultilinearMap.funLike` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SummationFilter.unconditional` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesOnBall.eventually_hasSum`
`eventually_hasSum_sub` 📖	mathematical	`HasFPowerSeriesAt`	`Filter.Eventually` `HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule` `ContinuousMultilinearMap.funLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SummationFilter.unconditional` `nhds`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesOnBall.eventually_hasSum_sub`
`hasFPowerSeriesWithinAt` 📖	mathematical	`HasFPowerSeriesAt`	`HasFPowerSeriesWithinAt`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesWithinAt.mono` `hasFPowerSeriesWithinAt_univ` `Set.subset_univ`
`isBigO_image_sub_norm_mul_norm_sub` 📖	mathematical	`HasFPowerSeriesAt`	`Asymptotics.IsBigO` `Real` `NormedAddCommGroup.toNorm` `Real.norm` `nhds` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.funLike` `Real.instMul` `Norm.norm` `Prod.toNorm` `Prod.instSub`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Set.insert_eq_of_mem` `Set.univ_prod_univ` `nhdsWithin_univ` `HasFPowerSeriesWithinAt.isBigO_image_sub_norm_mul_norm_sub` `hasFPowerSeriesWithinAt_univ`
`isBigO_sub_partialSum_pow` 📖	mathematical	`HasFPowerSeriesAt`	`Asymptotics.IsBigO` `Real` `NormedAddCommGroup.toNorm` `Real.norm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `FormalMultilinearSeries.partialSum` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule` `IsTopologicalAddGroup.toContinuousAdd` `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` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Set.insert_eq_of_mem` `nhdsWithin_univ` `HasFPowerSeriesWithinAt.isBigO_sub_partialSum_pow` `hasFPowerSeriesWithinAt_univ`
`radius_pos` 📖	mathematical	`HasFPowerSeriesAt`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `FormalMultilinearSeries.radius`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesOnBall.radius_pos`
`tendsto_partialSum` 📖	mathematical	`HasFPowerSeriesAt`	`Filter.Eventually` `Filter.Tendsto` `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` `Filter.atTop` `Nat.instPreorder` `nhds` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Filter.mp_mem` `Metric.eball_mem_nhds` `HasFPowerSeriesOnBall.r_pos` `Filter.univ_mem'` `HasFPowerSeriesOnBall.tendsto_partialSum`

HasFPowerSeriesOnBall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticAt` 📖	mathematical	`HasFPowerSeriesOnBall`	`AnalyticAt`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesAt.analyticAt` `hasFPowerSeriesAt`
`coeff_zero` 📖	mathematical	`HasFPowerSeriesOnBall`	`DFunLike.coe` `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.funLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesWithinOnBall.coeff_zero` `hasFPowerSeriesWithinOnBall_univ`
`comp_sub` 📖	mathematical	`HasFPowerSeriesOnBall`	`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` `r_le` `r_pos` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isInt_neg` `add_zero` `Mathlib.Tactic.Abel.zero_termg` `hasSum`
`continuousOn` 📖	mathematical	`HasFPowerSeriesOnBall`	`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` `Set.insert_eq_of_mem` `Set.univ_inter` `HasFPowerSeriesWithinOnBall.continuousOn` `hasFPowerSeriesWithinOnBall_univ`
`eventually_eq_zero` 📖	mathematical	`HasFPowerSeriesOnBall` `FormalMultilinearSeries` `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` `FormalMultilinearSeries.instAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.toAddCommGroup`	`Filter.Eventually` `nhds`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Filter.mp_mem` `eventually_hasSum_sub` `Filter.univ_mem'` `HasSum.unique` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_zero`
`eventually_hasSum` 📖	mathematical	`HasFPowerSeriesOnBall`	`Filter.Eventually` `HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule` `ContinuousMultilinearMap.funLike` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SummationFilter.unconditional` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Filter.mp_mem` `Metric.eball_mem_nhds` `r_pos` `Filter.univ_mem'` `hasSum`
`eventually_hasSum_sub` 📖	mathematical	`HasFPowerSeriesOnBall`	`Filter.Eventually` `HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule` `ContinuousMultilinearMap.funLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SummationFilter.unconditional` `nhds`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Filter.mp_mem` `Metric.eball_mem_nhds` `r_pos` `Filter.univ_mem'` `hasSum_sub`
`hasFPowerSeriesAt` 📖	mathematical	`HasFPowerSeriesOnBall`	`HasFPowerSeriesAt`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`hasFPowerSeriesWithinOnBall` 📖	mathematical	`HasFPowerSeriesOnBall`	`HasFPowerSeriesWithinOnBall`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesWithinOnBall.mono` `hasFPowerSeriesWithinOnBall_univ` `Set.subset_univ`
`hasSum` 📖	mathematical	`HasFPowerSeriesOnBall` `Set` `Set.instMembership` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule` `ContinuousMultilinearMap.funLike` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SummationFilter.unconditional`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`hasSum_sub` 📖	mathematical	`HasFPowerSeriesOnBall` `Set` `Set.instMembership` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule` `ContinuousMultilinearMap.funLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SummationFilter.unconditional`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `edist_eq_enorm_sub` `sub_zero` `add_sub_cancel` `hasSum`
`image_sub_sub_deriv_le` 📖	mathematical	`HasFPowerSeriesOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder`	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DFunLike.coe` `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.funLike` `Real.instMul` `Real.instMax`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Set.insert_eq_of_mem` `Set.univ_inter` `HasFPowerSeriesWithinOnBall.image_sub_sub_deriv_le` `hasFPowerSeriesWithinOnBall_univ`
`isBigO_image_sub_image_sub_deriv_principal` 📖	mathematical	`HasFPowerSeriesOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder`	`Asymptotics.IsBigO` `Real` `NormedAddCommGroup.toNorm` `Real.norm` `Filter.principal` `Metric.eball` `Prod.pseudoEMetricSpaceMax` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DFunLike.coe` `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.funLike` `Real.instMul` `Norm.norm` `Prod.toNorm` `Prod.instSub`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Set.insert_eq_of_mem` `Set.univ_prod_univ` `Set.inter_univ` `HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal` `hasFPowerSeriesWithinOnBall_univ`
`mono` 📖	—	`HasFPowerSeriesOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `Preorder.toLE`	—	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `le_trans` `r_le` `hasSum` `Metric.eball_subset_eball`
`r_le` 📖	mathematical	`HasFPowerSeriesOnBall`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `FormalMultilinearSeries.radius`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`r_pos` 📖	mathematical	`HasFPowerSeriesOnBall`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`radius_pos` 📖	mathematical	`HasFPowerSeriesOnBall`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `FormalMultilinearSeries.radius`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `lt_of_lt_of_le` `r_pos` `r_le`
`sum` 📖	mathematical	`HasFPowerSeriesOnBall` `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` `hasSum`
`tendstoLocallyUniformlyOn` 📖	mathematical	`HasFPowerSeriesOnBall`	`TendstoLocallyUniformlyOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `FormalMultilinearSeries.partialSum` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `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` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Filter.atTop` `Nat.instPreorder` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Set.insert_eq_of_mem` `Set.univ_inter` `HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn` `hasFPowerSeriesWithinOnBall_univ`
`tendstoLocallyUniformlyOn'` 📖	mathematical	`HasFPowerSeriesOnBall`	`TendstoLocallyUniformlyOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `FormalMultilinearSeries.partialSum` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `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` `Filter.atTop` `Nat.instPreorder` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Set.insert_eq_of_mem` `Set.univ_inter` `HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn'` `hasFPowerSeriesWithinOnBall_univ`
`tendstoUniformlyOn` 📖	mathematical	`HasFPowerSeriesOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal`	`TendstoUniformlyOn` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `FormalMultilinearSeries.partialSum` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `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` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Filter.atTop` `Nat.instPreorder` `Metric.ball` `NNReal.toReal`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Set.insert_eq_of_mem` `Set.univ_inter` `HasFPowerSeriesWithinOnBall.tendstoUniformlyOn` `hasFPowerSeriesWithinOnBall_univ`
`tendstoUniformlyOn'` 📖	mathematical	`HasFPowerSeriesOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal`	`TendstoUniformlyOn` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `FormalMultilinearSeries.partialSum` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `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` `Filter.atTop` `Nat.instPreorder` `Metric.ball` `NNReal.toReal`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Set.insert_eq_of_mem` `Set.univ_inter` `HasFPowerSeriesWithinOnBall.tendstoUniformlyOn'` `hasFPowerSeriesWithinOnBall_univ`
`tendsto_partialSum` 📖	mathematical	`HasFPowerSeriesOnBall` `Set` `Set.instMembership` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`Filter.Tendsto` `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` `NormedSpace.toIsBoundedSMul` `Filter.atTop` `Nat.instPreorder` `nhds` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasSum.tendsto_sum_nat` `hasSum`
`tendsto_partialSum_prod` 📖	mathematical	`HasFPowerSeriesOnBall` `Set` `Set.instMembership` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`Filter.Tendsto` `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` `NormedSpace.toIsBoundedSMul` `SProd.sprod` `Filter` `Filter.instSProd` `Filter.atTop` `Nat.instPreorder` `nhds` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesWithinOnBall.tendsto_partialSum_prod` `hasFPowerSeriesWithinOnBall` `Set.insert_eq_of_mem`
`uniform_geometric_approx` 📖	mathematical	`HasFPowerSeriesOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal`	`Real` `Set` `Set.instMembership` `Set.Ioo` `Real.instPreorder` `Real.instZero` `Real.instOne` `Real.instLT` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `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` `FormalMultilinearSeries.partialSum` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule` `IsTopologicalAddGroup.toContinuousAdd` `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` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `dist_zero_right` `Set.insert_eq_of_mem` `HasFPowerSeriesWithinOnBall.uniform_geometric_approx` `hasFPowerSeriesWithinOnBall_univ`
`uniform_geometric_approx'` 📖	mathematical	`HasFPowerSeriesOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal`	`Real` `Set` `Set.instMembership` `Set.Ioo` `Real.instPreorder` `Real.instZero` `Real.instOne` `Real.instLT` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `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` `FormalMultilinearSeries.partialSum` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule` `IsTopologicalAddGroup.toContinuousAdd` `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` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `NNReal.toReal`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `dist_zero_right` `Set.insert_eq_of_mem` `HasFPowerSeriesWithinOnBall.uniform_geometric_approx'` `hasFPowerSeriesWithinOnBall_univ`
`unique` 📖	mathematical	`HasFPowerSeriesOnBall`	`Set.EqOn` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasSum.unique` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_sub`

HasFPowerSeriesWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticWithinAt` 📖	mathematical	`HasFPowerSeriesWithinAt`	`AnalyticWithinAt`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`coeff_zero` 📖	mathematical	`HasFPowerSeriesWithinAt`	`DFunLike.coe` `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.funLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesWithinOnBall.coeff_zero`
`comp_sub` 📖	mathematical	`HasFPowerSeriesWithinAt`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Set` `Set.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Set.instSingletonSet`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesWithinOnBall.comp_sub`
`continuousWithinAt` 📖	mathematical	`HasFPowerSeriesWithinAt`	`ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousWithinAt.mono` `continuousWithinAt_insert` `Set.subset_insert`
`continuousWithinAt_insert` 📖	mathematical	`HasFPowerSeriesWithinAt`	`ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instInsert`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesWithinOnBall.continuousWithinAt_insert`
`eventually` 📖	mathematical	`HasFPowerSeriesWithinAt`	`Filter.Eventually` `ENNReal` `HasFPowerSeriesWithinOnBall` `nhdsWithin` `ENNReal.instTopologicalSpace` `instZeroENNReal` `Set.Ioi` `PartialOrder.toPreorder` `ENNReal.instPartialOrder`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Filter.mem_of_superset` `Ioo_mem_nhdsGT` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `HasFPowerSeriesWithinOnBall.r_pos` `HasFPowerSeriesWithinOnBall.of_le` `LT.lt.le`
`isBigO_image_sub_norm_mul_norm_sub` 📖	mathematical	`HasFPowerSeriesWithinAt`	`Asymptotics.IsBigO` `Real` `NormedAddCommGroup.toNorm` `Real.norm` `nhdsWithin` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SProd.sprod` `Set` `Set.instSProd` `Set.instInsert` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.funLike` `Real.instMul` `Norm.norm` `Prod.toNorm` `Prod.instSub`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ENNReal.lt_iff_exists_nnreal_btwn` `HasFPowerSeriesWithinOnBall.r_pos` `Asymptotics.IsBigO.mono` `HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal` `Set.inter_comm` `Filter.le_principal_iff` `inter_mem_nhdsWithin` `Metric.eball_mem_nhds`
`isBigO_sub_partialSum_pow` 📖	mathematical	`HasFPowerSeriesWithinAt`	`Asymptotics.IsBigO` `Real` `NormedAddCommGroup.toNorm` `Real.norm` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Set.preimage` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Set` `Set.instInsert` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `FormalMultilinearSeries.partialSum` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule` `IsTopologicalAddGroup.toContinuousAdd` `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` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ENNReal.lt_iff_exists_nnreal_btwn` `HasFPowerSeriesWithinOnBall.r_pos` `HasFPowerSeriesWithinOnBall.uniform_geometric_approx'` `Asymptotics.isBigO_iff` `Nat.cast_zero` `Filter.mp_mem` `inter_mem_nhdsWithin` `Metric.ball_mem_nhds` `Filter.univ_mem'` `div_pow` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `norm_norm` `mul_assoc` `div_mul_eq_mul_div` `mul_div_assoc` `mul_pow` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`mono` 📖	—	`HasFPowerSeriesWithinAt` `Set` `Set.instHasSubset`	—	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesWithinOnBall.mono`
`mono_of_mem_nhdsWithin` 📖	—	`HasFPowerSeriesWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `EMetric.mem_nhdsWithin_iff` `HasFPowerSeriesWithinOnBall.of_le` `HasFPowerSeriesWithinOnBall.r_pos` `min_le_left` `HasFPowerSeriesWithinOnBall.r_le` `HasFPowerSeriesWithinOnBall.hasSum` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `add_zero` `Set.mem_insert_of_mem` `edist_eq_enorm_sub` `add_sub_cancel_left` `sub_zero`

HasFPowerSeriesWithinOnBall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticWithinAt` 📖	mathematical	`HasFPowerSeriesWithinOnBall`	`AnalyticWithinAt`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesWithinAt.analyticWithinAt` `hasFPowerSeriesWithinAt`
`coeff_zero` 📖	mathematical	`HasFPowerSeriesWithinOnBall`	`DFunLike.coe` `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.funLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Unique.instSubsingleton` `Fin.isEmpty'` `PseudoEMetricSpace.edist_self` `r_pos` `pos_iff_ne_zero` `Nat.instCanonicallyOrderedAdd` `ContinuousMultilinearMap.map_coord_zero` `HasSum.unique` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum` `add_zero` `hasSum_single` `SummationFilter.instLeAtTopUnconditional`
`comp_sub` 📖	mathematical	`HasFPowerSeriesWithinOnBall`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Set` `Set.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Set.instSingletonSet`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `r_le` `r_pos` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isInt_neg` `add_zero` `Mathlib.Tactic.Abel.zero_termg` `Mathlib.Tactic.Abel.termg_eq` `one_zsmul` `Set.add_singleton` `Set.image_add_right` `Mathlib.Tactic.Abel.unfold_sub` `hasSum`
`congr'` 📖	—	`HasFPowerSeriesWithinOnBall` `Set.EqOn` `Set` `Set.instInter` `Set.instInsert` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `r_le` `r_pos` `edist_eq_enorm_sub` `add_sub_cancel_left` `sub_zero` `hasSum`
`continuousOn` 📖	mathematical	`HasFPowerSeriesWithinOnBall`	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instInter` `Set.instInsert` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `TendstoLocallyUniformlyOn.continuousOn` `tendstoLocallyUniformlyOn'` `Filter.Frequently.of_forall` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Continuous.continuousOn` `Continuous.comp` `FormalMultilinearSeries.partialSum_continuous` `Continuous.sub` `IsTopologicalAddGroup.to_continuousSub` `continuous_id` `continuous_const`
`continuousWithinAt` 📖	mathematical	`HasFPowerSeriesWithinOnBall`	`ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousWithinAt.mono` `continuousWithinAt_insert` `Set.subset_insert`
`continuousWithinAt_insert` 📖	mathematical	`HasFPowerSeriesWithinOnBall`	`ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instInsert`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousWithinAt.mono_of_mem_nhdsWithin` `ContinuousOn.continuousWithinAt` `continuousOn` `PseudoEMetricSpace.edist_self` `r_pos` `inter_mem_nhdsWithin` `Metric.eball_mem_nhds`
`hasFPowerSeriesWithinAt` 📖	mathematical	`HasFPowerSeriesWithinOnBall`	`HasFPowerSeriesWithinAt`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`hasSum` 📖	mathematical	`HasFPowerSeriesWithinOnBall` `Set` `Set.instMembership` `Set.instInsert` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`HasSum` `DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule` `ContinuousMultilinearMap.funLike` `SummationFilter.unconditional`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`hasSum_sub` 📖	mathematical	`HasFPowerSeriesWithinOnBall` `Set` `Set.instMembership` `Set.instInter` `Set.instInsert` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule` `ContinuousMultilinearMap.funLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SummationFilter.unconditional`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `edist_eq_enorm_sub` `sub_zero` `add_sub_cancel` `hasSum`
`image_sub_sub_deriv_le` 📖	mathematical	`HasFPowerSeriesWithinOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder`	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DFunLike.coe` `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.funLike` `Real.instMul` `Real.instMax`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `isBigO_image_sub_image_sub_deriv_principal` `mul_assoc` `norm_mul` `NormedDivisionRing.toNormMulClass` `abs_norm`
`isBigO_image_sub_image_sub_deriv_principal` 📖	mathematical	`HasFPowerSeriesWithinOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder`	`Asymptotics.IsBigO` `Real` `NormedAddCommGroup.toNorm` `Real.norm` `Filter.principal` `Set` `Set.instInter` `Metric.eball` `Prod.pseudoEMetricSpaceMax` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `SProd.sprod` `Set.instSProd` `Set.instInsert` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DFunLike.coe` `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.funLike` `Real.instMul` `Norm.norm` `Prod.toNorm` `Prod.instSub`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `CanLift.prf` `ENNReal.canLift` `ne_top_of_lt` `LE.le.eq_or_lt` `zero_le` `NNReal.instCanonicallyOrderedAdd` `Metric.eball_zero` `Set.empty_inter` `Filter.principal_empty` `FormalMultilinearSeries.norm_mul_pow_le_mul_pow_of_lt_radius` `LT.lt.trans_le` `r_le` `Nat.instAtLeastTwoHAddOfNat` `Metric.eball_prod_same` `Metric.eball_subset_eball` `LT.lt.le` `Finset.sum_range_succ` `Finset.sum_range_one` `coeff_zero` `sub_self` `zero_add` `Subsingleton.pi_single_eq` `Pi.single.eq_1` `ContinuousMultilinearMap.map_update_sub` `sub_sub_sub_cancel_right` `hasSum_nat_add_iff'` `HasSum.sub` `hasSum_sub` `Fintype.card_fin` `pi_norm_const` `ContinuousMultilinearMap.norm_image_sub_le` `pow_succ` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `mul_le_mul` `IsOrderedRing.toPosMulMono` `le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instZeroLEOneClass` `NNReal.coe_pos` `pow_le_pow_left₀` `norm_nonneg` `enorm_lt_coe` `edist_eq_enorm_sub` `Metric.mem_eball` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `le_of_lt` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `mul_pos` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.nnreal_coe_pos` `mul_nonneg` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `Nat.instIsOrderedAddMonoid` `Nat.instCanonicallyOrderedAdd` `Mathlib.Meta.Positivity.pos_of_isNat` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_add` `pow_zero` `one_mul` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `Nat.cast_nonneg'` `Real.instNontrivial` `Mathlib.Meta.NormNum.instAtLeastTwo` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `HasSum.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `add_mul` `Distrib.rightDistribClass` `abs_of_pos` `div_eq_mul_inv` `HasSum.add` `IsTopologicalSemiring.toContinuousAdd` `hasSum_coe_mul_geometric_of_norm_lt_one` `hasSum_geometric_of_norm_lt_one` `HasSum.norm_le_of_bounded` `mul_right_comm` `Asymptotics.IsBigO.const_mul_left` `Asymptotics.isBigO_refl` `Asymptotics.IsBigO.trans` `Asymptotics.IsBigO.of_norm_eventuallyLE` `Filter.eventually_principal`
`mono` 📖	—	`HasFPowerSeriesWithinOnBall` `Set` `Set.instHasSubset`	—	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `r_le` `r_pos` `hasSum` `Set.insert_subset_insert`
`of_le` 📖	—	`HasFPowerSeriesWithinOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `Preorder.toLE`	—	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `le_trans` `r_le` `hasSum` `Metric.eball_subset_eball`
`r_le` 📖	mathematical	`HasFPowerSeriesWithinOnBall`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `FormalMultilinearSeries.radius`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`r_pos` 📖	mathematical	`HasFPowerSeriesWithinOnBall`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`radius_pos` 📖	mathematical	`HasFPowerSeriesWithinOnBall`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `FormalMultilinearSeries.radius`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `lt_of_lt_of_le` `r_pos` `r_le`
`sum` 📖	mathematical	`HasFPowerSeriesWithinOnBall` `Set` `Set.instMembership` `Set.instInsert` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`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` `hasSum`
`tendstoLocallyUniformlyOn` 📖	mathematical	`HasFPowerSeriesWithinOnBall`	`TendstoLocallyUniformlyOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `FormalMultilinearSeries.partialSum` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `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` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Filter.atTop` `Nat.instPreorder` `Set` `Set.instInter` `Set.preimage` `Set.instInsert` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ENNReal.lt_iff_exists_nnreal_btwn` `IsOpen.mem_nhds` `Metric.isOpen_eball` `nhdsWithin_inter_of_mem'` `mem_nhdsWithin_of_mem_nhds` `Filter.mem_of_superset` `Metric.eball_subset_eball` `LT.lt.le` `inter_mem_nhdsWithin` `Metric.eball_coe` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `dist_zero_right` `norm_zero` `add_zero` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `tendstoUniformlyOn`
`tendstoLocallyUniformlyOn'` 📖	mathematical	`HasFPowerSeriesWithinOnBall`	`TendstoLocallyUniformlyOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `FormalMultilinearSeries.partialSum` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `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` `Filter.atTop` `Nat.instPreorder` `Set` `Set.instInter` `Set.instInsert` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousOn.sub` `IsTopologicalAddGroup.to_continuousSub` `continuousOn_id'` `continuousOn_const` `add_sub_cancel` `TendstoLocallyUniformlyOn.comp` `tendstoLocallyUniformlyOn` `edist_eq_enorm_sub` `sub_zero`
`tendstoUniformlyOn` 📖	mathematical	`HasFPowerSeriesWithinOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal`	`TendstoUniformlyOn` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `FormalMultilinearSeries.partialSum` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `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` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Filter.atTop` `Nat.instPreorder` `Set` `Set.instInter` `Set.preimage` `Set.instInsert` `Metric.ball` `NNReal.toReal`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `uniform_geometric_approx` `Metric.tendstoUniformlyOn_iff` `Filter.Tendsto.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `tendsto_const_nhds` `tendsto_pow_atTop_nhds_zero_of_lt_one` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Real.instArchimedean` `instOrderTopologyReal` `LT.lt.le` `Filter.Eventually.mono` `Filter.Tendsto.eventually` `MulZeroClass.mul_zero` `gt_mem_nhds` `dist_eq_norm` `LE.le.trans_lt`
`tendstoUniformlyOn'` 📖	mathematical	`HasFPowerSeriesWithinOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal`	`TendstoUniformlyOn` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `FormalMultilinearSeries.partialSum` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `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` `Filter.atTop` `Nat.instPreorder` `Set` `Set.instInter` `Set.instInsert` `Metric.ball` `NNReal.toReal`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `add_sub_cancel` `Set.ext` `dist_eq_norm` `sub_zero` `TendstoUniformlyOn.comp` `tendstoUniformlyOn`
`tendsto_partialSum` 📖	mathematical	`HasFPowerSeriesWithinOnBall` `Set` `Set.instMembership` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Set.instInsert` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	`Filter.Tendsto` `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` `Filter.atTop` `Nat.instPreorder` `nhds`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasSum.tendsto_sum_nat` `hasSum`
`tendsto_partialSum_prod` 📖	mathematical	`HasFPowerSeriesWithinOnBall` `Set` `Set.instMembership` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Set.instInsert` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	`Filter.Tendsto` `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` `SProd.sprod` `Filter` `Filter.instSProd` `Filter.atTop` `Nat.instPreorder` `nhds`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Filter.Tendsto.comp` `tendsto_partialSum` `Filter.tendsto_fst` `Metric.tendsto_nhds` `ENNReal.lt_iff_exists_nnreal_btwn` `edist_zero_right` `FormalMultilinearSeries.summable_norm_mul_pow` `LT.lt.trans_le` `r_le` `Nat.instAtLeastTwoHAddOfNat` `tendsto_sum_nat_add` `instIsTopologicalAddGroupReal` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Filter.Eventually.exists` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `tendsto_order` `instOrderTopologyReal` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `CancelDenoms.sub_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Meta.NormNum.isNat_lt_true` `Continuous.continuousAt` `FormalMultilinearSeries.partialSum_continuous` `Filter.tendsto_snd` `ContinuousAt.tendsto` `IsOpen.mem_nhds` `Metric.isOpen_ball` `dist_zero_right` `Filter.mp_mem` `Filter.univ_mem'` `Filter.Ici_mem_atTop` `dist_eq_norm` `sub_zero` `Finset.sum_Ico_eq_sum_range` `add_comm` `norm_sum_le` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `LE.le.trans_eq` `ContinuousMultilinearMap.le_opNorm` `Finset.prod_const` `Fintype.card_fin` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `pow_le_pow_left₀` `IsOrderedRing.toMulPosMono` `norm_nonneg` `LT.lt.le` `Summable.sum_le_tsum` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `SummationFilter.instNeBotUnconditional` `SummationFilter.instLeAtTopUnconditional` `mul_nonneg` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `NNReal.coe_nonneg` `summable_nat_add_iff` `Finset.sum_range_add_sum_Ico` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `norm_add₃_le` `add_le_add` `covariant_swap_add_of_covariant_add` `le_of_lt` `norm_neg` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `CancelDenoms.add_subst` `add_sub_cancel` `Filter.Tendsto.add`
`uniform_geometric_approx` 📖	mathematical	`HasFPowerSeriesWithinOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal`	`Real` `Set` `Set.instMembership` `Set.Ioo` `Real.instPreorder` `Real.instZero` `Real.instOne` `Real.instLT` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `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` `FormalMultilinearSeries.partialSum` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule` `IsTopologicalAddGroup.toContinuousAdd` `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` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `uniform_geometric_approx'` `LE.le.trans` `ball_zero_eq` `LT.lt.le` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `pow_le_pow_left₀` `IsOrderedRing.toMulPosMono` `mul_nonneg` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_nonneg` `NNReal.coe_nonneg` `mul_le_of_le_one_right` `div_le_one_of_le₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instZeroLEOneClass` `le_of_lt`
`uniform_geometric_approx'` 📖	mathematical	`HasFPowerSeriesWithinOnBall` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal`	`Real` `Set` `Set.instMembership` `Set.Ioo` `Real.instPreorder` `Real.instZero` `Real.instOne` `Real.instLT` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `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` `FormalMultilinearSeries.partialSum` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule` `IsTopologicalAddGroup.toContinuousAdd` `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` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `NNReal.toReal`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `FormalMultilinearSeries.norm_mul_pow_le_mul_pow_of_lt_radius` `LT.lt.trans_le` `r_le` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `ball_zero_eq` `LE.le.trans_lt` `norm_nonneg` `mem_eball_zero_iff` `lt_trans` `norm_sub_rev` `mul_div_right_comm` `mul_le_of_le_one_right` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `LT.lt.le` `div_le_one_of_le₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instZeroLEOneClass` `NNReal.coe_nonneg` `norm_sub_le_of_geometric_bound_of_hasSum` `ContinuousMultilinearMap.le_opNorm` `Finset.prod_const` `Fintype.card_fin` `div_pow` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `mul_pow` `mul_assoc` `le_refl` `hasSum` `LE.le.trans` `div_le_div₀` `mul_nonneg` `le_of_lt` `sub_le_sub_left`
`unique` 📖	mathematical	`HasFPowerSeriesWithinOnBall`	`Set.EqOn` `Set` `Set.instInter` `Set.instInsert` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasSum.unique` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_sub`

(root)

Definitions

Name	Category	Theorems
`AnalyticAt` 📖	MathDef	83 math math: `MeromorphicAt.analyticAt`, `ContinuousMultilinearMap.analyticAt_uncurry_compContinuousLinearMap`, `Complex.analyticAt_cosh`, `ContinuousMultilinearMap.analyticAt_uncurry_of_linear`, `expNegInvGlue.not_analyticAt_zero`, `MeromorphicNFAt.meromorphicOrderAt_nonneg_iff_analyticAt`, `Real.analyticAt_cos`, `HarmonicAt.analyticAt_complex_partial`, `PeriodPair.analyticAt_weierstrassPExcept`, `analyticAt_rexp`, `Real.analyticAt_sinh`, `analyticAt_neg`, `meromorphicOrderAt_ne_top_iff`, `Complex.analyticAt_sin`, `Meromorphic.MeromorphicOn.countable_compl_analyticAt`, `ProbabilityTheory.analyticAt_mgf`, `ContinuousLinearMap.analyticAt`, `analyticOrderAt_ne_zero`, `Real.analyticAt_sin`, `analyticAt_smul`, `NormedSpace.analyticAt_exp_of_mem_ball`, `AnalyticOn.analyticAt`, `MeromorphicOn.analyticAt_mem_codiscreteWithin`, `ProbabilityTheory.analyticAt_complexMGF`, `AnalyticWithinAt.exists_analyticAt`, `analyticWithinAt_iff_exists_analyticAt'`, `Meromorphic.countable_compl_analyticAt`, `ContinuousMultilinearMap.analyticAt`, `ProbabilityTheory.analyticAt_cgf`, `MeromorphicAt.iff_eventuallyEq_zpow_smul_analyticAt`, `meromorphicOrderAt_eq_int_iff`, `meromorphicNFAt_iff_analyticAt_or`, `analyticAt_sigmoid`, `Function.FactorizedRational.analyticAt`, `Real.analyticAt_arcosh`, `analyticAt_const`, `analyticAt_id`, `LinearIsometryEquiv.analyticAt`, `HarmonicAt.analyticAt`, `MeromorphicAt.eventually_analyticAt`, `MeromorphicOn.eventually_codiscreteWithin_analyticAt`, `analyticAt_fst`, `HasFPowerSeriesOnBall.analyticAt_of_mem`, `Complex.analyticAt_sinh`, `AnalyticAt.of_meromorphicOrderAt_pos`, `MeromorphicOn.countable_compl_analyticAt_inter`, `HasFPowerSeriesOnBall.analyticAt`, `MeromorphicOn.eventually_analyticAt_or_mem_compl`, `CPolynomialAt.analyticAt`, `PeriodPair.analyticAt_derivWeierstrassPExcept`, `analyticAt_log`, `FormalMultilinearSeries.analyticAt_changeOrigin`, `isOpen_analyticAt`, `Real.analyticAt_arsinh`, `Real.analyticAt_cosh`, `analyticWithinAt_iff_exists_analyticAt`, `analyticWithinAt_univ`, `Complex.analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt`, `analyticOrderAt_eq_zero`, `analyticAt_mul`, `analyticAt_inv`, `ModularFormClass.analyticAt_cuspFunction_zero`, `ContDiffAt.analyticAt`, `analyticAt_clog`, `analyticAt_inverse_one_sub`, `analyticAt_inv_one_sub`, `analyticAt_congr`, `DifferentiableOn.analyticAt`, `Complex.analyticAt_cos`, `ContinuousLinearEquiv.analyticAt`, `MeromorphicOn.countable_compl_analyticAt`, `NormedSpace.exp_analytic`, `ContinuousLinearMap.analyticAt_bilinear`, `ProbabilityTheory.analyticAt_iteratedDeriv_mgf`, `MeromorphicOn.eventually_analyticAt`, `ContinuousLinearMap.analyticAt_uncurry_of_multilinear`, `analyticAt_pi_iff`, `analyticAt_inverse`, `Complex.analyticAt_iff_eventually_differentiableAt`, `HasFPowerSeriesAt.analyticAt`, `Differentiable.analyticAt`, `analyticAt_snd`, `analyticAt_cexp`
`AnalyticOn` 📖	MathDef	64 math math: `Real.analyticOn_cos`, `ProbabilityTheory.analyticOn_mgf`, `Real.analyticOn_cosh`, `Complex.analyticOn_sin`, `Complex.analyticOn_cosh`, `Complex.analyticOn_sinh`, `ContinuousLinearMap.analyticOn_bilinear`, `analyticOn_congr`, `analyticOn_empty`, `HasFPowerSeriesWithinOnBall.analyticOn`, `analyticOn_log`, `contDiffOn_omega_iff_analyticOn`, `contDiffWithinAt_iff_of_ne_infty`, `Real.analyticOn_arcosh`, `contDiffOn_succ_iff_fderiv_of_isOpen`, `ProbabilityTheory.analyticOn_cgf`, `contDiffWithinAt_succ_iff_hasFDerivWithinAt'`, `contDiffOn_succ_iff_hasFDerivWithinAt`, `ContinuousLinearEquiv.analyticOn`, `Complex.analyticOn_iff_differentiableOn`, `AnalyticOnNhd.analyticOn`, `LinearIsometryEquiv.analyticOn`, `Complex.analyticOn_cos`, `contDiffOn_succ_iff_deriv_of_isOpen`, `ContDiffOn.analyticOn`, `analyticOn_id`, `WithLp.analyticOn_toLp`, `Complex.analyticOn_univ_iff_differentiable`, `ContinuousMultilinearMap.analyticOn_uncurry_of_linear`, `PiLp.analyticOn_ofLp`, `PiLp.analyticOn_toLp`, `Real.analyticOn_sin`, `IsOpen.analyticOn_iff_analyticOnNhd`, `analyticOn_cexp`, `analyticOn_sigmoid`, `analyticOn_univ`, `analyticOn_pi_iff`, `AnalyticWithinAt.exists_mem_nhdsWithin_analyticOn`, `ContinuousLinearMap.analyticOn`, `ContinuousMultilinearMap.analyticOn`, `analyticOn_inv`, `contDiffOn_succ_iff_fderivWithin`, `LSeries_analyticOn`, `contDiffOn_succ_iff_fderiv_apply`, `contDiff_succ_iff_deriv`, `contDiffOn_succ_iff_derivWithin`, `ProbabilityTheory.analyticOn_complexMGF`, `contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn`, `ContinuousLinearMap.analyticOn_uncurry_of_multilinear`, `Real.analyticOn_arsinh`, `Real.analyticOn_sinh`, `AnalyticOn.eval_polynomial`, `analyticOn_const`, `CPolynomialOn.analyticOn`, `ContDiffWithinAt.analyticOn`, `ProbabilityTheory.analyticOn_iteratedDeriv_mgf`, `ContinuousMultilinearMap.analyticOn_uncurry_compContinuousLinearMap`, `analyticOn_rexp`, `analyticOn_snd`, `analyticOn_fst`, `WithLp.analyticOn_ofLp`, `contDiffWithinAt_succ_iff_hasFDerivWithinAt`, `AnalyticWithinAt.exists_hasFTaylorSeriesUpToOn`, `DifferentiableOn.analyticOn`
`AnalyticOnNhd` 📖	MathDef	65 math math: `LinearIsometryEquiv.analyticOnNhd`, `Real.analyticOnNhd_sin`, `analyticOnNhd_inverse`, `AnalyticOnNhd.eval_linearMap'`, `analyticOnNhd_circleMap`, `analyticOnNhd_pi_iff`, `Complex.analyticOnNhd_univ_iff_differentiable`, `analyticOnNhd_rexp`, `contDiff_succ_iff_fderiv`, `LSeries_analyticOnNhd`, `PeriodPair.analyticOnNhd_derivWeierstrassPExcept`, `analyticOnNhd_snd`, `analyticOnNhd_log`, `analyticOnNhd_sigmoid`, `Real.analyticOnNhd_cosh`, `ProbabilityTheory.analyticOnNhd_cgf`, `AnalyticOnNhd.eval_linearMap`, `CPolynomialOn.analyticOnNhd`, `AnalyticAt.exists_ball_analyticOnNhd`, `analyticOnNhd_congr`, `Complex.analyticOnNhd_sin`, `analyticOnNhd_id`, `analyticOnNhd_cexp`, `analyticOnNhd_const`, `ContinuousLinearMap.analyticOnNhd_bilinear`, `Real.analyticOnNhd_arsinh`, `contDiff_succ_iff_fderiv_apply`, `AnalyticOnNhd.eval_polynomial`, `MeromorphicNFOn.divisor_nonneg_iff_analyticOnNhd`, `HasFPowerSeriesOnBall.analyticOnNhd`, `Complex.analyticOnNhd_cosh`, `ContinuousLinearMap.analyticOnNhd_uncurry_of_multilinear`, `FormalMultilinearSeries.analyticOnNhd`, `IsOpen.analyticOn_iff_analyticOnNhd`, `harmonic_is_realOfHolomorphic`, `AnalyticAt.exists_mem_nhds_analyticOnNhd`, `analyticOn_univ`, `PeriodPair.analyticOnNhd_derivWeierstrassP`, `Real.analyticOnNhd_cos`, `analyticOnNhd_fst`, `ContinuousMultilinearMap.analyticOnNhd`, `MeromorphicOn.extract_zeros_poles`, `contDiff_omega_iff_analyticOnNhd`, `ProbabilityTheory.analyticOnNhd_mgf`, `DifferentiableOn.analyticOnNhd`, `ContinuousLinearEquiv.analyticOnNhd`, `Complex.analyticOnNhd_iff_differentiableOn`, `ContinuousMultilinearMap.analyticOnNhd_uncurry_compContinuousLinearMap`, `ContinuousLinearMap.analyticOnNhd`, `analyticOnNhd_empty`, `Real.analyticOnNhd_sinh`, `PeriodPair.analyticOnNhd_weierstrassPExcept`, `analyticOnNhd_inv`, `Complex.analyticOnNhd_cos`, `analyticOnNhd_congr'`, `ProbabilityTheory.analyticOnNhd_complexMGF`, `AnalyticOnNhd.eval_continuousLinearMap'`, `ContinuousMultilinearMap.analyticOnNhd_uncurry_of_linear`, `PeriodPair.analyticOnNhd_weierstrassP`, `Real.analyticOnNhd_arcosh`, `AnalyticOnNhd.eval_mvPolynomial`, `Complex.analyticOnNhd_sinh`, `AnalyticOnNhd.eval_continuousLinearMap`, `ContDiff.analyticOnNhd`, `ProbabilityTheory.analyticOnNhd_iteratedDeriv_mgf`
`AnalyticWithinAt` 📖	MathDef	38 math math: `ContinuousLinearMap.analyticWithinAt_bilinear`, `analyticWithinAt_id`, `ContinuousLinearMap.analyticWithinAt`, `analyticWithinAt_snd`, `analyticWithinAt_const`, `analyticWithinAt_pi_iff`, `Real.analyticWithinAt_sinh`, `Complex.analyticWithinAt_cosh`, `HasFPowerSeriesWithinAt.analyticWithinAt`, `HasFPowerSeriesWithinOnBall.analyticWithinAt_of_mem`, `ContinuousLinearMap.analyticWithinAt_uncurry_of_multilinear`, `analyticWithinAt_iff_exists_analyticAt'`, `contDiffWithinAt_omega_iff_analyticWithinAt`, `LinearIsometryEquiv.analyticWithinAt`, `CPolynomialAt.analyticWithinAt`, `analyticWithinAt_fst`, `Real.analyticWithinAt_cos`, `Complex.analyticWithinAt_sinh`, `analyticWithinAt_sigmoid`, `AnalyticAt.analyticWithinAt`, `analyticWithinAt_of_singleton_mem`, `ContinuousMultilinearMap.analyticWithinAt_uncurry_of_linear`, `ContinuousMultilinearMap.analyticWithinAt_uncurry_compContinuousLinearMap`, `analyticWithinAt_iff_exists_analyticAt`, `analyticWithinAt_univ`, `ContinuousMultilinearMap.analyticWithinAt`, `analyticWithinAt_rexp`, `Real.analyticWithinAt_sin`, `analyticWithinAt_insert`, `Complex.analyticWithinAt_sin`, `ContinuousLinearEquiv.analyticWithinAt`, `Real.analyticWithinAt_arcosh`, `Real.analyticWithinAt_arsinh`, `analyticWithinAt_cexp`, `Real.analyticWithinAt_cosh`, `HasFPowerSeriesWithinOnBall.analyticWithinAt`, `Complex.analyticWithinAt_cos`, `ContDiffWithinAt.analyticWithinAt`
`HasFPowerSeriesAt` 📖	MathDef	21 math math: `hasFPowerSeriesWithinAt_iff_of_nhds`, `hasFPowerSeriesWithinAt_iff_exists_hasFPowerSeriesAt`, `PeriodPair.hasFPowerSeriesAt_weierstrassPExcept`, `NormedSpace.hasFPowerSeriesAt_exp_zero_of_radius_pos`, `one_add_cpow_hasFPowerSeriesAt_zero`, `ContinuousLinearMap.hasFPowerSeriesAt`, `hasFPowerSeriesAt_const`, `hasFPowerSeriesWithinAt_univ`, `HasFiniteFPowerSeriesAt.hasFPowerSeriesAt`, `PeriodPair.hasFPowerSeriesAt_derivWeierstrassPExcept`, `Complex.one_add_cpow_hasFPowerSeriesAt_zero`, `ProbabilityTheory.hasFPowerSeriesAt_mgf`, `NormedSpace.exp_hasFPowerSeriesAt_zero`, `hasFPowerSeriesAt_pi_iff`, `ContinuousLinearMap.hasFPowerSeriesAt_bilinear`, `AnalyticAt.hasFPowerSeriesAt`, `Real.one_add_rpow_hasFPowerSeriesAt_zero`, `one_add_rpow_hasFPowerSeriesAt_zero`, `HasFPowerSeriesOnBall.hasFPowerSeriesAt`, `hasFPowerSeriesAt_iff'`, `hasFPowerSeriesAt_iff`
`HasFPowerSeriesOnBall` 📖	CompData	48 math math: `ContinuousLinearMap.hasFPowerSeriesOnBall`, `ModularFormClass.hasFPowerSeries_cuspFunction`, `hasFPowerSeriesOnBall_pi_iff`, `Real.hasFPowerSeriesOnBall_ofScalars_mul_add_zero`, `AnalyticOn.hasFPowerSeriesOnSubball`, `Real.one_add_rpow_hasFPowerSeriesOnBall_zero`, `NormedSpace.exp_hasFPowerSeriesOnBall`, `spectrum.hasFPowerSeriesOnBall_inverse_one_sub_smul`, `hasFPowerSeriesOnBall_const`, `hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall`, `Differentiable.hasFPowerSeriesOnBall`, `Real.one_div_one_sub_sq_hasFPowerSeriesOnBall_zero`, `Real.one_div_one_sub_hasFPowerSeriesOnBall_zero`, `NormedSpace.hasFPowerSeriesOnBall_exp_of_radius_pos`, `Real.one_div_sub_hasFPowerSeriesOnBall_zero`, `HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall`, `hasFPowerSeriesWithinOnBall_univ`, `ContinuousLinearMap.hasFPowerSeriesOnBall_bilinear`, `Complex.one_div_sub_sq_hasFPowerSeriesOnBall_zero`, `Complex.one_div_one_sub_pow_hasFPowerSeriesOnBall_zero`, `HasFPowerSeriesAt.eventually`, `Real.one_div_one_sub_rpow_hasFPowerSeriesOnBall_zero`, `Complex.one_div_sub_pow_hasFPowerSeriesOnBall_zero`, `hasFPowerSeriesOn_cauchy_integral`, `DifferentiableOn.hasFPowerSeriesOnBall`, `hasFPowerSeriesOnBall_inv_one_sub`, `hasFPowerSeriesOnBall_inverse_one_sub`, `PeriodPair.hasFPowerSeriesOnBall_weierstrassP`, `Real.hasFPowerSeriesOnBall_linear_zero`, `PeriodPair.hasFPowerSeriesOnBall_derivWeierstrassPExcept`, `hasFPowerSeriesOnBall_cuspFunction`, `Complex.one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero`, `one_add_cpow_hasFPowerSeriesOnBall_zero`, `Complex.one_div_one_sub_sq_hasFPowerSeriesOnBall_zero`, `PeriodPair.hasFPowerSeriesOnBall_weierstrassPExcept`, `AnalyticOn.hasFPowerSeriesOnBall`, `Real.one_div_sub_pow_hasFPowerSeriesOnBall_zero`, `Complex.hasFPowerSeriesOnBall_of_differentiable_off_countable`, `Complex.one_add_cpow_hasFPowerSeriesOnBall_zero`, `Complex.one_div_one_sub_hasFPowerSeriesOnBall_zero`, `DiffContOnCl.hasFPowerSeriesOnBall`, `Complex.one_div_sub_sq_sub_one_div_sq_hasFPowerSeriesOnBall_zero`, `Complex.hasFPowerSeriesOnBall_ofScalars_mul_add_zero`, `one_add_rpow_hasFPowerSeriesOnBall_zero`, `Real.one_div_sub_sq_hasFPowerSeriesOnBall_zero`, `FormalMultilinearSeries.hasFPowerSeriesOnBall_changeOrigin`, `FormalMultilinearSeries.hasFPowerSeriesOnBall`, `Complex.one_div_sub_hasFPowerSeriesOnBall_zero`
`HasFPowerSeriesWithinAt` 📖	MathDef	7 math math: `hasFPowerSeriesWithinAt_iff_of_nhds`, `hasFPowerSeriesWithinAt_iff_exists_hasFPowerSeriesAt`, `hasFPowerSeriesWithinAt_insert`, `hasFPowerSeriesWithinAt_univ`, `HasFPowerSeriesWithinOnBall.hasFPowerSeriesWithinAt`, `HasFPowerSeriesAt.hasFPowerSeriesWithinAt`, `hasFPowerSeriesWithinAt_pi_iff`
`HasFPowerSeriesWithinOnBall` 📖	CompData	6 math math: `HasFPowerSeriesWithinAt.eventually`, `hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall`, `hasFPowerSeriesWithinOnBall_univ`, `hasFPowerSeriesWithinOnBall_insert_self`, `hasFPowerSeriesWithinOnBall_pi_iff`, `HasFPowerSeriesOnBall.hasFPowerSeriesWithinOnBall`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticAt_congr` 📖	mathematical	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`AnalyticAt`	—	`AnalyticAt.congr` `Filter.EventuallyEq.symm`
`analyticOnNhd_congr` 📖	mathematical	`IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.EqOn`	`AnalyticOnNhd`	—	`AnalyticOnNhd.congr` `Set.EqOn.symm`
`analyticOnNhd_congr'` 📖	mathematical	`Filter.EventuallyEq` `nhdsSet` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`AnalyticOnNhd`	—	`AnalyticOnNhd.congr'` `Filter.EventuallyEq.symm`
`analyticOnNhd_empty` 📖	mathematical	—	`AnalyticOnNhd` `Set` `Set.instEmptyCollection`	—	`instIsEmptyFalse`
`analyticOn_congr` 📖	mathematical	`Set.EqOn`	`AnalyticOn`	—	`AnalyticOn.congr` `Set.EqOn.symm`
`analyticOn_empty` 📖	mathematical	—	`AnalyticOn` `Set` `Set.instEmptyCollection`	—	`instIsEmptyFalse`
`analyticOn_univ` 📖	mathematical	—	`AnalyticOn` `Set.univ` `AnalyticOnNhd`	—	—
`analyticWithinAt_insert` 📖	mathematical	—	`AnalyticWithinAt` `Set` `Set.instInsert`	—	—
`analyticWithinAt_univ` 📖	mathematical	—	`AnalyticWithinAt` `Set.univ` `AnalyticAt`	—	—
`hasFPowerSeriesAt_iff` 📖	mathematical	—	`HasFPowerSeriesAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `Filter.Eventually` `HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `NormedSpace.toModule` `Monoid.toNatPow` `FormalMultilinearSeries.coeff` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `SummationFilter.unconditional` `nhds` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Filter.eventually_of_mem` `Metric.eball_mem_nhds` `edist_zero_right` `FormalMultilinearSeries.apply_eq_prod_smul_coeff` `Finset.prod_const` `Fintype.card_fin` `GT.gt.lt` `NormedField.exists_norm_lt` `FormalMultilinearSeries.le_radius_of_tendsto` `FormalMultilinearSeries.norm_apply_eq_norm_coef` `mul_comm` `norm_smul` `NormedSpace.toNormSMulClass` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `Filter.Tendsto.comp` `tendsto_norm` `Summable.tendsto_atTop_zero` `HasSum.summable` `dist_zero_right` `lt_of_lt_of_le` `zero_lt_iff` `nnnorm_ne_zero_iff` `norm_pos_iff` `FormalMultilinearSeries.apply_eq_pow_smul_coeff` `nndist_eq_nnnorm` `sub_zero`
`hasFPowerSeriesAt_iff'` 📖	mathematical	—	`HasFPowerSeriesAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `Filter.Eventually` `HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `NormedSpace.toModule` `Monoid.toNatPow` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `FormalMultilinearSeries.coeff` `SummationFilter.unconditional` `nhds` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `map_add_left_nhds_zero` `Filter.eventually_map` `hasFPowerSeriesAt_iff` `add_sub_cancel_left`
`hasFPowerSeriesWithinAt_iff_of_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`HasFPowerSeriesWithinAt` `HasFPowerSeriesAt`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `hasFPowerSeriesWithinAt_univ` `HasFPowerSeriesWithinAt.mono_of_mem_nhdsWithin` `mem_nhdsWithin_of_mem_nhds` `HasFPowerSeriesWithinAt.mono` `Set.subset_univ`
`hasFPowerSeriesWithinAt_insert` 📖	mathematical	—	`HasFPowerSeriesWithinAt` `Set` `Set.instInsert`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `eq_or_ne` `HasFPowerSeriesWithinAt.mono` `Set.subset_insert` `HasFPowerSeriesWithinAt.mono_of_mem_nhdsWithin` `nhdsWithin_insert_of_ne` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `self_mem_nhdsWithin`
`hasFPowerSeriesWithinAt_univ` 📖	mathematical	—	`HasFPowerSeriesWithinAt` `Set.univ` `HasFPowerSeriesAt`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`hasFPowerSeriesWithinOnBall_insert_self` 📖	mathematical	—	`HasFPowerSeriesWithinOnBall` `Set` `Set.instInsert`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesWithinOnBall.r_le` `HasFPowerSeriesWithinOnBall.r_pos` `Set.insert_idem` `HasFPowerSeriesWithinOnBall.hasSum`
`hasFPowerSeriesWithinOnBall_univ` 📖	mathematical	—	`HasFPowerSeriesWithinOnBall` `Set.univ` `HasFPowerSeriesOnBall`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `HasFPowerSeriesWithinOnBall.r_le` `HasFPowerSeriesWithinOnBall.r_pos` `HasFPowerSeriesWithinOnBall.hasSum` `Set.insert_eq_of_mem` `HasFPowerSeriesOnBall.r_le` `HasFPowerSeriesOnBall.r_pos` `HasFPowerSeriesOnBall.hasSum`

---

← Back to Index