ConvergenceOnBall

📁 Source: Mathlib/Analysis/Calculus/IteratedDeriv/ConvergenceOnBall.lean

Statistics

Metric	Count
Definitions	0
Theorems hasFPowerSeriesOnBall, hasFPowerSeriesOnSubball	2
Total	2

AnalyticOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasFPowerSeriesOnBall 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal FormalMultilinearSeries.radius DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField NormedField.toNormedSpace NontriviallyNormedField.toNormedField FormalMultilinearSeries.ofScalars NormedField.toField NormedRing.toRing NormedCommRing.toNormedRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid iteratedDeriv AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.factorial AnalyticOn Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace	HasFPowerSeriesOnBall	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing hasFPowerSeriesOnSubball le_rfl
hasFPowerSeriesOnSubball 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal AnalyticOn DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField NormedField.toNormedSpace NontriviallyNormedField.toNormedField Metric.eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace Preorder.toLE FormalMultilinearSeries.radius FormalMultilinearSeries.ofScalars NormedField.toField NormedRing.toRing NormedCommRing.toNormedRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid iteratedDeriv AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.factorial	HasFPowerSeriesOnBall	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul zero_add HasFPowerSeriesOnBall.comp_sub FormalMultilinearSeries.hasFPowerSeriesOnBall RCLike.toCompleteSpace ne_of_lt le_antisymm le_trans le_of_lt le_refl Set.add_singleton Set.image_add_right Metric.preimage_add_right_eball NormedAddGroup.to_isIsometricVAdd_right sub_neg_eq_add AnalyticOnNhd.comp_sub FormalMultilinearSeries.analyticOnNhd AnalyticOnNhd.mono Metric.eball_subset_eball HasFPowerSeriesOnBall.congr HasFPowerSeriesOnBall.mono Set.EqOn.symm AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq IsOpen.analyticOn_iff_analyticOnNhd Metric.isOpen_eball IsConnected.isPreconnected Metric.isConnected_eball PseudoEMetricSpace.edist_self EMetric.mem_nhds_iff AnalyticAt.hasFPowerSeriesAt RCLike.charZero_rclike HasFPowerSeriesOnBall.r_pos HasFPowerSeriesOnBall.unique HasFPowerSeriesOnBall.r_le

---

← Back to Index