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	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	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 📖	mathematical	AnalyticOn Set Set.instHasSubset	AnalyticOn	—	AnalyticWithinAt.mono

AnalyticOnNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticOn 📖	mathematical	AnalyticOnNhd	AnalyticOn	—	AnalyticAt.analyticWithinAt
comp_sub 📖	mathematical	AnalyticOnNhd	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' 📖	mathematical	AnalyticOnNhd Filter.EventuallyEq nhdsSet UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	AnalyticOnNhd	—	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 📖	mathematical	AnalyticOnNhd Set Set.instHasSubset	AnalyticOnNhd	—	—

AnalyticWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_sub 📖	mathematical	AnalyticWithinAt	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 📖	mathematical	AnalyticWithinAt Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	AnalyticWithinAt	—	HasFPowerSeriesWithinAt.congr
congr_of_eventuallyEq_insert 📖	mathematical	AnalyticWithinAt Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set Set.instInsert	AnalyticWithinAt	—	congr_of_eventuallyEq nhdsWithin_mono Set.subset_insert mem_of_mem_nhdsWithin Set.mem_insert
congr_set 📖	mathematical	AnalyticWithinAt Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	AnalyticWithinAt	—	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 📖	mathematical	AnalyticWithinAt Set Set.instHasSubset	AnalyticWithinAt	—	HasFPowerSeriesWithinAt.mono
mono_of_mem_nhdsWithin 📖	mathematical	AnalyticWithinAt Set Filter Filter.instMembership nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	AnalyticWithinAt	—	HasFPowerSeriesWithinAt.mono_of_mem_nhdsWithin

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_analyticOn 📖	mathematical	AnalyticOn	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	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	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	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 radius	—	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	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	Filter.Eventually NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	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.toPow 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	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	Filter.Eventually NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	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 📖	mathematical	HasFPowerSeriesOnBall ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Preorder.toLE	HasFPowerSeriesOnBall	—	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 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 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 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 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 NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup 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.toPow 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.toPow 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	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.toPow 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 📖	mathematical	HasFPowerSeriesWithinAt Set Set.instHasSubset	HasFPowerSeriesWithinAt	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul HasFPowerSeriesWithinOnBall.mono
mono_of_mem_nhdsWithin 📖	mathematical	HasFPowerSeriesWithinAt Set Filter Filter.instMembership nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	HasFPowerSeriesWithinAt	—	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	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' 📖	mathematical	HasFPowerSeriesWithinOnBall Set.EqOn Set Set.instInter Set.instInsert Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	HasFPowerSeriesWithinOnBall	—	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 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	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 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 IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing 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 📖	mathematical	HasFPowerSeriesWithinOnBall Set Set.instHasSubset	HasFPowerSeriesWithinOnBall	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul r_le r_pos hasSum Set.insert_subset_insert
of_le 📖	mathematical	HasFPowerSeriesWithinOnBall ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Preorder.toLE	HasFPowerSeriesWithinOnBall	—	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	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 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 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 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 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 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 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 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 Mathlib.Tactic.CancelDenoms.sub_subst Mathlib.Tactic.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 Mathlib.Tactic.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.toPow 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.toPow 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 instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add 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	159 math math: MeromorphicAt.analyticAt, ContinuousMultilinearMap.analyticAt_uncurry_compContinuousLinearMap, Complex.analyticAt_cosh, ContinuousMultilinearMap.analyticAt_uncurry_of_linear, Finset.analyticAt_fun_sum, UpperHalfPlane.analyticAt_smul, expNegInvGlue.not_analyticAt_zero, AnalyticAt.fun_const_smul, MeromorphicNFAt.meromorphicOrderAt_nonneg_iff_analyticAt, analyticAt_iff_analytic_mul, Real.analyticAt_cos, AnalyticAt.curry_right, HarmonicAt.analyticAt_complex_partial, AnalyticAt.rexp, PeriodPair.analyticAt_weierstrassPExcept, analyticAt_rexp, AnalyticAt.sigmoid', Real.analyticAt_sinh, analyticAt_neg, meromorphicOrderAt_ne_top_iff, AnalyticAt.exists_eventuallyEq_sum_add_pow_mul, Complex.analyticAt_sin, AnalyticAt.deriv, AnalyticAt.log, Meromorphic.MeromorphicOn.countable_compl_analyticAt, ProbabilityTheory.analyticAt_mgf, AnalyticAt.clog, AnalyticAt.smul, ContinuousLinearMap.analyticAt, AnalyticAt.rexp', analyticOrderAt_ne_zero, Real.analyticAt_sin, analyticAt_smul, NormedSpace.analyticAt_exp_of_mem_ball, AnalyticOn.analyticAt, MeromorphicOn.analyticAt_mem_codiscreteWithin, OpenPartialHomeomorph.analyticAt_symm, AnalyticAt.comp', ProbabilityTheory.analyticAt_complexMGF, AnalyticAt.fun_smul, AnalyticAt.prod, AnalyticWithinAt.exists_analyticAt, analyticAt_iff_analytic_fun_mul, analyticWithinAt_iff_exists_analyticAt', Meromorphic.countable_compl_analyticAt, natCast_le_analyticOrderAt, ContinuousMultilinearMap.analyticAt, ProbabilityTheory.analyticAt_cgf, MeromorphicAt.iff_eventuallyEq_zpow_smul_analyticAt, AnalyticAt.along_snd, meromorphicOrderAt_eq_int_iff, meromorphicNFAt_iff_analyticAt_or, analyticAt_sigmoid, AnalyticAt.restrictScalars, AnalyticAt.fun_zpow, AnalyticAt.analyticOrderAt_eq_natCast, Function.FactorizedRational.analyticAt, AnalyticAt.analyticOrderNatAt_eq_iff, Real.analyticAt_arcosh, analyticAt_const, analyticAt_iff_analytic_fun_smul, AnalyticAt.sub, analyticAt_id, LinearIsometryEquiv.analyticAt, OpenPartialHomeomorph.analyticAt_symm', HarmonicAt.analyticAt, MeromorphicAt.eventually_analyticAt, AnalyticAt.aeval_polynomial, MeromorphicOn.eventually_codiscreteWithin_analyticAt, AnalyticAt.sigmoid, analyticAt_fst, AnalyticAt.add, AnalyticAt.comp_of_eq, HasFPowerSeriesOnBall.analyticAt_of_mem, AnalyticAt.fun_mul, Complex.analyticAt_sinh, AnalyticAt.of_meromorphicOrderAt_pos, AnalyticAt.iterated_deriv, MeromorphicOn.countable_compl_analyticAt_inter, AnalyticAt.comp_sub, analyticAt_iff_analytic_smul, HasFPowerSeriesOnBall.analyticAt, AnalyticAt.fun_add, AnalyticAt.fun_pow, AnalyticAt.exists_eq_sum_add_pow_mul, AnalyticAt.cpow, analyticAt_comp_iff_of_deriv_ne_zero, MeromorphicOn.eventually_analyticAt_or_mem_compl, AnalyticAt.fun_neg, AnalyticAt.analyticOrderAt_ne_top, AnalyticAt.const_smul, AnalyticAt.neg, Finset.analyticAt_prod, CPolynomialAt.analyticAt, PeriodPair.analyticAt_derivWeierstrassPExcept, analyticAt_log, AnalyticAt.zpow_nonneg, FormalMultilinearSeries.analyticAt_changeOrigin, AnalyticAt.analyticAt_localInverse, isOpen_analyticAt, Real.analyticAt_arsinh, Finset.analyticAt_sum, AnalyticAt.fun_inv, Real.analyticAt_cosh, analyticWithinAt_iff_exists_analyticAt, AnalyticAt.fun_div, analyticWithinAt_univ, AnalyticAt.re_ofReal, AnalyticAt.congr, AnalyticAt.comp₂, analyticAt_finprod, Complex.analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt, AnalyticAt.div_const, analyticOrderAt_eq_zero, analyticAt_mul, analyticAt_inv, ModularFormClass.analyticAt_cuspFunction_zero, AnalyticAt.aeval_mvPolynomial, ContDiffAt.analyticAt, AnalyticAt.compContinuousLinearMap, analyticAt_clog, AnalyticAt.along_fst, AnalyticAt.eventually_analyticAt, AnalyticAt.pi, analyticAt_inverse_one_sub, analyticAt_inv_one_sub, AnalyticAt.mul, AnalyticAt.div, analyticAt_congr, AnalyticAt.exists_eventuallyEq_pow_smul_nonzero_iff, DifferentiableOn.analyticAt, AnalyticAt.fun_sub, AnalyticAt.curry_left, AnalyticAt.fun_zpow_nonneg, AnalyticAt.fderiv, Complex.analyticAt_cos, ContinuousLinearEquiv.analyticAt, AnalyticAt.pow, MeromorphicOn.countable_compl_analyticAt, NormedSpace.exp_analytic, AnalyticAt.inv, ContinuousLinearMap.analyticAt_bilinear, AnalyticAt.cexp', ProbabilityTheory.analyticAt_iteratedDeriv_mgf, MeromorphicOn.eventually_analyticAt, ContinuousLinearMap.analyticAt_uncurry_of_multilinear, AnalyticAt.comp, analyticAt_pi_iff, analyticAt_inverse, Complex.analyticAt_iff_eventually_differentiableAt, AnalyticAt.zpow, Finset.analyticAt_fun_prod, HasFPowerSeriesAt.analyticAt, AnalyticAt.cexp, Differentiable.analyticAt, analyticAt_snd, AnalyticAt.im_ofReal, analyticAt_cexp, AnalyticAt.comp_of_eq'
AnalyticOn 📖	MathDef	113 math math: AnalyticOn.exists_hasFTaylorSeriesUpToOn, AnalyticOn.aeval_polynomial, Real.analyticOn_cos, ProbabilityTheory.analyticOn_mgf, AnalyticOn.im_ofReal, AnalyticOn.cpow, Real.analyticOn_cosh, Complex.analyticOn_sin, AnalyticOn.comp_sub, AnalyticOn.iteratedFDerivWithin, AnalyticOn.fun_inv, AnalyticOn.rexp, AnalyticOn.sub, AnalyticOn.sigmoid, Complex.analyticOn_cosh, AnalyticOn.pow, AnalyticOn.neg, Complex.analyticOn_sinh, ContinuousLinearMap.analyticOn_bilinear, analyticOn_congr, analyticOn_empty, HasFPowerSeriesWithinOnBall.analyticOn, AnalyticOn.fun_zpow, AnalyticOn.fderivWithin, analyticOn_log, AnalyticOn.compContinuousLinearMap, contDiffOn_omega_iff_analyticOn, contDiffWithinAt_iff_of_ne_infty, AnalyticOn.congr, AnalyticOn.clog, AnalyticOn.pi, Real.analyticOn_arcosh, contDiffOn_succ_iff_fderiv_of_isOpen, ProbabilityTheory.analyticOn_cgf, AnalyticOn.zpow_nonneg, AnalyticOn.const_smul, Finset.analyticOn_fun_sum, AnalyticOn.comp₂, AnalyticOn.smul, contDiffWithinAt_succ_iff_hasFDerivWithinAt', contDiffOn_succ_iff_hasFDerivWithinAt, ContinuousLinearEquiv.analyticOn, analyticOn_taylorComp, Complex.analyticOn_iff_differentiableOn, AnalyticOnNhd.analyticOn, LinearIsometryEquiv.analyticOn, Complex.analyticOn_cos, contDiffOn_succ_iff_deriv_of_isOpen, AnalyticOnNhd.comp_analyticOn, AnalyticOn.inv, ContDiffOn.analyticOn, analyticOn_id, WithLp.analyticOn_toLp, Complex.analyticOn_univ_iff_differentiable, ContinuousMultilinearMap.analyticOn_uncurry_of_linear, AnalyticOn.add, PiLp.analyticOn_ofLp, AnalyticOn.zpow, ContinuousLinearMap.comp_analyticOn, PiLp.analyticOn_toLp, Real.analyticOn_sin, IsOpen.analyticOn_iff_analyticOnNhd, analyticOn_cexp, analyticOn_sigmoid, analyticOn_univ, analyticOn_pi_iff, AnalyticWithinAt.exists_mem_nhdsWithin_analyticOn, AnalyticOn.restrictScalars, ContinuousLinearMap.analyticOn, ContinuousMultilinearMap.analyticOn, analyticOn_inv, AnalyticOn.div, Finset.analyticOn_fun_prod, AnalyticOn.comp, AnalyticOn.fun_zpow_nonneg, contDiffOn_succ_iff_fderivWithin, AnalyticOn.curry_left, Finset.analyticOn_sum, LSeries_analyticOn, contDiffOn_succ_iff_fderiv_apply, contDiff_succ_iff_deriv, contDiffOn_succ_iff_derivWithin, ProbabilityTheory.analyticOn_complexMGF, AnalyticOn.fun_const_smul, contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn, ContinuousLinearMap.analyticOn_uncurry_of_multilinear, Real.analyticOn_arsinh, Real.analyticOn_sinh, AnalyticOn.re_ofReal, AnalyticOn.eval_polynomial, AnalyticOn.div_const, AnalyticOn.prod, analyticOn_const, CPolynomialOn.analyticOn, ContDiffWithinAt.analyticOn, HasFTaylorSeriesUpToOn.analyticOn, AnalyticOn.fun_pow, AnalyticOn.mul, ProbabilityTheory.analyticOn_iteratedDeriv_mgf, ContinuousMultilinearMap.analyticOn_uncurry_compContinuousLinearMap, analyticOn_rexp, analyticOn_of_locally_analyticOn, AnalyticOn.log, AnalyticOn.curry_right, analyticOn_snd, AnalyticOn.mono, analyticOn_fst, Finset.analyticOn_prod, WithLp.analyticOn_ofLp, contDiffWithinAt_succ_iff_hasFDerivWithinAt, AnalyticWithinAt.exists_hasFTaylorSeriesUpToOn, AnalyticOn.cexp, DifferentiableOn.analyticOn
AnalyticOnNhd 📖	MathDef	124 math math: AnalyticOnNhd.smul, LinearIsometryEquiv.analyticOnNhd, Finset.analyticOnNhd_prod, AnalyticOnNhd.curry_left, Real.analyticOnNhd_sin, AnalyticOnNhd.compContinuousLinearMap, AnalyticOnNhd.re_ofReal, analyticOnNhd_inverse, AnalyticOnNhd.iteratedFDeriv_of_isOpen, AnalyticOnNhd.eval_linearMap', analyticOnNhd_circleMap, AnalyticOnNhd.iteratedFDeriv, AnalyticOnNhd.rexp, analyticOnNhd_pi_iff, Complex.analyticOnNhd_univ_iff_differentiable, analyticOnNhd_rexp, contDiff_succ_iff_fderiv, LSeries_analyticOnNhd, AnalyticOnNhd.cpow, PeriodPair.analyticOnNhd_derivWeierstrassPExcept, analyticOnNhd_snd, analyticOnNhd_log, AnalyticOnNhd.fderiv_of_isOpen, analyticOnNhd_sigmoid, Real.analyticOnNhd_cosh, ProbabilityTheory.analyticOnNhd_cgf, AnalyticOnNhd.eval_linearMap, CPolynomialOn.analyticOnNhd, AnalyticAt.exists_ball_analyticOnNhd, AnalyticOnNhd.clog, analyticOnNhd_congr, AnalyticOnNhd.comp', Complex.analyticOnNhd_sin, AnalyticOnNhd.comp_sub, analyticOnNhd_id, AnalyticOnNhd.aeval_mvPolynomial, AnalyticOnNhd.cexp, analyticOnNhd_cexp, analyticOnNhd_const, AnalyticOnNhd.comp₂, ContinuousLinearMap.analyticOnNhd_bilinear, Real.analyticOnNhd_arsinh, AnalyticOnNhd.congr, AnalyticOnNhd.along_snd, contDiff_succ_iff_fderiv_apply, AnalyticOnNhd.comp, AnalyticOnNhd.eval_polynomial, AnalyticOnNhd.deriv_of_isOpen, MeromorphicNFOn.divisor_nonneg_iff_analyticOnNhd, AnalyticOnNhd.mul, AnalyticOnNhd.fun_zpow, HasFPowerSeriesOnBall.analyticOnNhd, Complex.analyticOnNhd_cosh, ContinuousLinearMap.analyticOnNhd_uncurry_of_multilinear, FormalMultilinearSeries.analyticOnNhd, AnalyticOnNhd.zpow, AnalyticOnNhd.deriv, AnalyticOnNhd.along_fst, IsOpen.analyticOn_iff_analyticOnNhd, harmonic_is_realOfHolomorphic, AnalyticOnNhd.fderiv, AnalyticAt.exists_mem_nhds_analyticOnNhd, analyticOn_univ, Finset.analyticOnNhd_sum, PeriodPair.analyticOnNhd_derivWeierstrassP, AnalyticOnNhd.add, AnalyticOnNhd.zpow_nonneg, AnalyticOnNhd.fun_pow, Complex.analyticOnNhd_canonicalFactor, Real.analyticOnNhd_cos, Finset.analyticOnNhd_fun_sum, analyticOnNhd_fst, ContinuousMultilinearMap.analyticOnNhd, AnalyticOnNhd.div, MeromorphicOn.extract_zeros_poles, contDiff_omega_iff_analyticOnNhd, AnalyticOnNhd.pi, ProbabilityTheory.analyticOnNhd_mgf, AnalyticOnNhd.div_const, DifferentiableOn.analyticOnNhd, ContinuousLinearEquiv.analyticOnNhd, AnalyticOnNhd.restrictScalars, InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_univ_re_eq, Complex.analyticOnNhd_iff_differentiableOn, AnalyticOnNhd.curry_right, AnalyticOnNhd.mono, AnalyticOnNhd.aeval_polynomial, InnerProductSpace.harmonic_is_realOfHolomorphic_univ, AnalyticOnNhd.fun_zpow_nonneg, ContinuousMultilinearMap.analyticOnNhd_uncurry_compContinuousLinearMap, ContinuousLinearMap.analyticOnNhd, analyticOnNhd_empty, AnalyticOnNhd.sigmoid, Real.analyticOnNhd_sinh, PeriodPair.analyticOnNhd_weierstrassPExcept, analyticOnNhd_inv, Complex.analyticOnNhd_cos, ContinuousLinearMap.comp_analyticOnNhd, AnalyticOnNhd.pow, InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq, AnalyticOnNhd.fun_const_smul, analyticOnNhd_congr', ProbabilityTheory.analyticOnNhd_complexMGF, AnalyticOnNhd.log, AnalyticOnNhd.const_smul, AnalyticOnNhd.eval_continuousLinearMap', AnalyticOnNhd.iterated_deriv, ContinuousMultilinearMap.analyticOnNhd_uncurry_of_linear, PeriodPair.analyticOnNhd_weierstrassP, AnalyticOnNhd.neg, ValueDistribution.logCounting_isBigO_one_iff_analyticOnNhd, Real.analyticOnNhd_arcosh, AnalyticOnNhd.eval_mvPolynomial, AnalyticOnNhd.fun_inv, AnalyticOnNhd.im_ofReal, Complex.analyticOnNhd_sinh, AnalyticOnNhd.eval_continuousLinearMap, AnalyticOnNhd.sub, ContDiff.analyticOnNhd, Finset.analyticOnNhd_fun_prod, AnalyticOnNhd.inv, AnalyticOnNhd.congr', AnalyticOnNhd.prod, ProbabilityTheory.analyticOnNhd_iteratedDeriv_mgf
AnalyticWithinAt 📖	MathDef	87 math math: AnalyticWithinAt.const_smul, ContinuousLinearMap.analyticWithinAt_bilinear, AnalyticAt.comp_analyticWithinAt, analyticWithinAt_id, ContinuousLinearMap.analyticWithinAt, AnalyticWithinAt.sub, AnalyticAtWithin.compContinuousLinearMap, analyticWithinAt_snd, AnalyticWithinAt.fun_zpow, analyticWithinAt_const, analyticWithinAt_pi_iff, Real.analyticWithinAt_sinh, AnalyticWithinAt.cpow, Complex.analyticWithinAt_cosh, HasFPowerSeriesWithinAt.analyticWithinAt, AnalyticWithinAt.restrictScalars, AnalyticWithinAt.cexp, AnalyticWithinAt.congr_of_eventuallyEq_insert, HasFPowerSeriesWithinOnBall.analyticWithinAt_of_mem, AnalyticWithinAt.prod, Finset.analyticWithinAt_fun_prod, AnalyticWithinAt.curry_right, AnalyticWithinAt.curry_left, AnalyticWithinAt.inv, Finset.analyticWithinAt_prod, ContinuousLinearMap.analyticWithinAt_uncurry_of_multilinear, AnalyticWithinAt.add, AnalyticWithinAt.eventually_analyticWithinAt, analyticWithinAt_iff_exists_analyticAt', AnalyticWithinAt.neg, AnalyticWithinAt.aeval_polynomial, contDiffWithinAt_omega_iff_analyticWithinAt, AnalyticWithinAt.fun_inv, AnalyticAt.comp₂_analyticWithinAt, LinearIsometryEquiv.analyticWithinAt, CPolynomialAt.analyticWithinAt, AnalyticWithinAt.pi, AnalyticWithinAt.re_ofReal, analyticWithinAt_fst, Real.analyticWithinAt_cos, AnalyticWithinAt.im_ofReal, AnalyticWithinAt.div_const, AnalyticWithinAt.comp_sub, AnalyticWithinAt.pow, AnalyticWithinAt.fun_zpow_nonneg, Complex.analyticWithinAt_sinh, AnalyticWithinAt.rexp, AnalyticWithinAt.congr_of_eventuallyEq, AnalyticWithinAt.mono, AnalyticWithinAt.congr, analyticWithinAt_sigmoid, AnalyticAt.analyticWithinAt, AnalyticWithinAt.div, AnalyticWithinAt.fun_pow, AnalyticWithinAt.congr_set, analyticWithinAt_of_singleton_mem, AnalyticWithinAt.zpow_nonneg, AnalyticWithinAt.comp₂, ContinuousMultilinearMap.analyticWithinAt_uncurry_of_linear, AnalyticWithinAt.sigmoid, AnalyticWithinAt.zpow, ContinuousMultilinearMap.analyticWithinAt_uncurry_compContinuousLinearMap, analyticWithinAt_iff_exists_analyticAt, analyticWithinAt_univ, ContinuousMultilinearMap.analyticWithinAt, analyticWithinAt_rexp, Real.analyticWithinAt_sin, AnalyticWithinAt.mono_of_mem_nhdsWithin, analyticWithinAt_insert, Complex.analyticWithinAt_sin, ContinuousLinearEquiv.analyticWithinAt, Real.analyticWithinAt_arcosh, Finset.analyticWithinAt_sum, Real.analyticWithinAt_arsinh, AnalyticWithinAt.clog, analyticWithinAt_cexp, Real.analyticWithinAt_cosh, HasFPowerSeriesWithinOnBall.analyticWithinAt, AnalyticAt.comp_analyticWithinAt_of_eq, Finset.analyticWithinAt_fun_sum, AnalyticWithinAt.log, AnalyticWithinAt.comp, AnalyticWithinAt.comp_of_eq, Complex.analyticWithinAt_cos, ContDiffWithinAt.analyticWithinAt, AnalyticWithinAt.mul, AnalyticWithinAt.smul
HasFPowerSeriesAt 📖	MathDef	35 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, HasFPowerSeriesAt.neg, HasFPowerSeriesAt.add, HasFPowerSeriesAt.comp, ContinuousLinearMap.hasFPowerSeriesAt, HasFPowerSeriesAt.congr, hasFPowerSeriesAt_const, hasFPowerSeriesWithinAt_univ, HasFiniteFPowerSeriesAt.hasFPowerSeriesAt, PeriodPair.hasFPowerSeriesAt_derivWeierstrassPExcept, HasFPowerSeriesAt.comp_sub, Complex.one_add_cpow_hasFPowerSeriesAt_zero, ProbabilityTheory.hasFPowerSeriesAt_mgf, HasFPowerSeriesAt.restrictScalars, NormedSpace.exp_hasFPowerSeriesAt_zero, HasFPowerSeriesAt.has_fpower_series_iterate_dslope_fslope, hasFPowerSeriesAt_pi_iff, OpenPartialHomeomorph.hasFPowerSeriesAt_symm, ContinuousLinearMap.hasFPowerSeriesAt_bilinear, AnalyticAt.hasFPowerSeriesAt, HasFPowerSeriesAt.const_smul, Real.one_add_rpow_hasFPowerSeriesAt_zero, HasFPowerSeriesAt.sub, one_add_rpow_hasFPowerSeriesAt_zero, HasFPowerSeriesAt.pi, HasFPowerSeriesAt.prod, HasFPowerSeriesOnBall.hasFPowerSeriesAt, HasFPowerSeriesAt.has_fpower_series_dslope_fslope, HasFPowerSeriesAt.compContinuousLinearMap, hasFPowerSeriesAt_iff', hasFPowerSeriesAt_iff
HasFPowerSeriesOnBall 📖	CompData	65 math math: ContinuousLinearMap.hasFPowerSeriesOnBall, HasFPowerSeriesOnBall.congr, ModularFormClass.hasFPowerSeries_cuspFunction, HasFPowerSeriesOnBall.add, hasFPowerSeriesOnBall_pi_iff, HasFPowerSeriesOnBall.unshift, HasFPowerSeriesOnBall.restrictScalars, Real.hasFPowerSeriesOnBall_ofScalars_mul_add_zero, AnalyticOn.hasFPowerSeriesOnSubball, HasFPowerSeriesOnBall.const_smul, Real.one_add_rpow_hasFPowerSeriesOnBall_zero, NormedSpace.exp_hasFPowerSeriesOnBall, spectrum.hasFPowerSeriesOnBall_inverse_one_sub_smul, hasFPowerSeriesOnBall_const, hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall, Differentiable.hasFPowerSeriesOnBall, HasFPowerSeriesOnBall.comp_sub, Real.one_div_one_sub_sq_hasFPowerSeriesOnBall_zero, HasFPowerSeriesOnBall.fderiv, HasFPowerSeriesOnBall.compContinuousLinearMap, 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, HasFPowerSeriesOnBall.neg, HasFPowerSeriesAt.eventually, Real.one_div_one_sub_rpow_hasFPowerSeriesOnBall_zero, Complex.one_div_sub_pow_hasFPowerSeriesOnBall_zero, HasFPowerSeriesOnBall.sub, hasFPowerSeriesOn_cauchy_integral, DifferentiableOn.hasFPowerSeriesOnBall, hasFPowerSeriesOnBall_inv_one_sub, hasFPowerSeriesOnBall_inverse_one_sub, PeriodPair.hasFPowerSeriesOnBall_weierstrassP, HasFPowerSeriesOnBall.r_eq_top_of_exists, Real.hasFPowerSeriesOnBall_linear_zero, PeriodPair.hasFPowerSeriesOnBall_derivWeierstrassPExcept, HasFPowerSeriesOnBall.pi, hasFPowerSeriesOnBall_cuspFunction, Complex.one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero, HasFPowerSeriesOnBall.prod, one_add_cpow_hasFPowerSeriesOnBall_zero, ContinuousLinearMap.comp_hasFPowerSeriesOnBall, 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, HasFPowerSeriesOnBall.changeOrigin, 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, HasFPowerSeriesOnBall.mono, Complex.hasFPowerSeriesOnBall_ofScalars_mul_add_zero, one_add_rpow_hasFPowerSeriesOnBall_zero, Real.one_div_sub_sq_hasFPowerSeriesOnBall_zero, FormalMultilinearSeries.hasFPowerSeriesOnBall_changeOrigin, HasFPowerSeriesOnBall.exchange_radius, FormalMultilinearSeries.hasFPowerSeriesOnBall, Complex.one_div_sub_hasFPowerSeriesOnBall_zero
HasFPowerSeriesWithinAt 📖	MathDef	21 math math: hasFPowerSeriesWithinAt_iff_of_nhds, hasFPowerSeriesWithinAt_iff_exists_hasFPowerSeriesAt, HasFPowerSeriesWithinAt.comp_sub, HasFPowerSeriesWithinAt.const_smul, hasFPowerSeriesWithinAt_insert, hasFPowerSeriesWithinAt_univ, HasFPowerSeriesWithinAt.mono, HasFPowerSeriesWithinOnBall.hasFPowerSeriesWithinAt, HasFPowerSeriesAt.hasFPowerSeriesWithinAt, HasFPowerSeriesWithinAt.pi, HasFPowerSeriesWithinAt.sub, HasFPowerSeriesWithinAt.mono_of_mem_nhdsWithin, HasFPowerSeriesWithinAt.prod, HasFPowerSeriesWithinAt.restrictScalars, HasFPowerSeriesWithinAt.congr, hasFPowerSeriesWithinAt_pi_iff, HasFPowerSeriesWithinAt.neg, HasFPowerSeriesWithinAt.unshift, HasFPowerSeriesWithinAt.add, HasFPowerSeriesWithinAt.compContinuousLinearMap, HasFPowerSeriesWithinAt.comp
HasFPowerSeriesWithinOnBall 📖	CompData	26 math math: HasFPowerSeriesWithinOnBall.restrictScalars, HasFPowerSeriesWithinAt.eventually, HasFPowerSeriesWithinOnBall.fderivWithin, hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall, HasFPowerSeriesWithinOnBall.prod, HasFPowerSeriesWithinOnBall.unshift, HasFPowerSeriesWithinOnBall.sub, hasFPowerSeriesWithinOnBall_univ, ContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall, hasFPowerSeriesWithinOnBall_insert_self, HasFPowerSeriesWithinOnBall.const_smul, HasFPowerSeriesWithinOnBall.comp_sub, HasFPowerSeriesWithinOnBall.compContinuousLinearMap, HasFPowerSeriesWithinOnBall.changeOrigin, HasFPowerSeriesWithinOnBall.fderivWithin_of_mem, HasFPowerSeriesWithinOnBall.congr, HasFPowerSeriesWithinOnBall.congr', HasFPowerSeriesWithinOnBall.iteratedFDerivWithin, HasFPowerSeriesWithinOnBall.neg, hasFPowerSeriesWithinOnBall_pi_iff, HasFPowerSeriesWithinOnBall.add, HasFPowerSeriesWithinOnBall.mono, HasFPowerSeriesWithinOnBall.pi, HasFPowerSeriesWithinOnBall.fderivWithin_of_mem_of_analyticOn, HasFPowerSeriesWithinOnBall.of_le, 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.toPow 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	—	IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul 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.toPow SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup FormalMultilinearSeries.coeff SummationFilter.unconditional nhds SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	—	IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul 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