FTaylorSeries

📁 Source: Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean

Statistics

Metric	Count
Definitions termω, «term∞», HasFTaylorSeriesUpTo, HasFTaylorSeriesUpToOn, ftaylorSeries, ftaylorSeriesWithin, iteratedFDeriv, iteratedFDerivWithin	8
Theorems ftaylorSeries, ftaylorSeriesWithin, iteratedFDeriv, iteratedFDerivWithin, iteratedFDerivWithin', iteratedFDerivWithin_eq, iteratedFDeriv, cont, continuous, differentiable, eq_iteratedFDeriv, fderiv, fderiv_eq, hasFDerivAt, hasFTaylorSeriesUpToOn, of_le, tsupport_mono, tsupport_subset, zero_eq, zero_eq', congr_series, cont, continuousOn, differentiableAt, differentiableOn, eq_iteratedFDerivWithin_of_uniqueDiffOn, eventually_hasFDerivAt, fderivWithin, hasFDerivAt, hasFDerivWithinAt, mono, of_le, shift_of_succ, zero_eq, zero_eq', iteratedFDerivWithin, dist_iteratedFDerivWithin_one, dist_iteratedFDerivWithin_zero, fderivWithin_iteratedFDerivWithin, fderiv_iteratedFDeriv, ftaylorSeriesWithin_insert, ftaylorSeriesWithin_univ, hasFTaylorSeriesUpToOn_empty, hasFTaylorSeriesUpToOn_succ_iff_left, hasFTaylorSeriesUpToOn_succ_iff_right, hasFTaylorSeriesUpToOn_succ_nat_iff_right, hasFTaylorSeriesUpToOn_top_iff, hasFTaylorSeriesUpToOn_top_iff', hasFTaylorSeriesUpToOn_top_iff_add, hasFTaylorSeriesUpToOn_top_iff_right, hasFTaylorSeriesUpToOn_univ_iff, hasFTaylorSeriesUpToOn_zero_iff, hasFTaylorSeriesUpTo_succ_nat_iff_right, hasFTaylorSeriesUpTo_top_iff, hasFTaylorSeriesUpTo_top_iff', hasFTaylorSeriesUpTo_zero_iff, iteratedFDerivWithin_comp_add_left, iteratedFDerivWithin_comp_add_left', iteratedFDerivWithin_comp_add_right, iteratedFDerivWithin_comp_add_right', iteratedFDerivWithin_comp_sub, iteratedFDerivWithin_comp_sub', iteratedFDerivWithin_congr, iteratedFDerivWithin_congr_set, iteratedFDerivWithin_congr_set', iteratedFDerivWithin_eventually_congr_set, iteratedFDerivWithin_eventually_congr_set', iteratedFDerivWithin_insert, iteratedFDerivWithin_inter, iteratedFDerivWithin_inter', iteratedFDerivWithin_inter_open, iteratedFDerivWithin_of_isOpen, iteratedFDerivWithin_one_apply, iteratedFDerivWithin_succ_apply_left, iteratedFDerivWithin_succ_apply_right, iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_succ_eq_comp_right, iteratedFDerivWithin_two_apply, iteratedFDerivWithin_two_apply', iteratedFDerivWithin_univ, iteratedFDerivWithin_zero_apply, iteratedFDerivWithin_zero_eq, iteratedFDerivWithin_zero_eq_comp, iteratedFDeriv_comp_add_left, iteratedFDeriv_comp_add_left', iteratedFDeriv_comp_add_right, iteratedFDeriv_comp_add_right', iteratedFDeriv_comp_sub, iteratedFDeriv_comp_sub', iteratedFDeriv_one_apply, iteratedFDeriv_succ_apply_left, iteratedFDeriv_succ_apply_right, iteratedFDeriv_succ_eq_comp_left, iteratedFDeriv_succ_eq_comp_right, iteratedFDeriv_two_apply, iteratedFDeriv_zero_apply, iteratedFDeriv_zero_eq_comp, norm_fderivWithin_iteratedFDerivWithin, norm_fderiv_iteratedFDeriv, norm_iteratedFDerivWithin_fderivWithin, norm_iteratedFDerivWithin_one, norm_iteratedFDerivWithin_zero, norm_iteratedFDeriv_fderiv, norm_iteratedFDeriv_one, norm_iteratedFDeriv_zero, support_iteratedFDeriv_subset, tsupport_iteratedFDeriv_subset	107
Total	115

ContDiff

Definitions

Name	Category	Theorems
termω 📖	CompOp	—
«term∞» 📖	CompOp	—

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ftaylorSeries 📖	mathematical	Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	Filter.EventuallyEq 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 nhds ftaylorSeries	—	Filter.mp_mem IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul eventually_eventuallyEq_nhds Filter.univ_mem' FormalMultilinearSeries.ext eq_of_nhds iteratedFDeriv
ftaylorSeriesWithin 📖	mathematical	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	Filter.EventuallyEq 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 nhdsWithin ftaylorSeriesWithin	—	Filter.mp_mem IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul self_mem_nhdsWithin eventually_eventually_nhdsWithin Filter.univ_mem' FormalMultilinearSeries.ext eq_of_nhdsWithin iteratedFDerivWithin
iteratedFDeriv 📖	mathematical	Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	Filter.EventuallyEq 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 nhds iteratedFDeriv	—	—
iteratedFDerivWithin 📖	mathematical	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	Filter.EventuallyEq 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 nhdsWithin iteratedFDerivWithin	—	iteratedFDerivWithin' Set.Subset.rfl
iteratedFDerivWithin' 📖	mathematical	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set Set.instHasSubset	Filter.EventuallyEq 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 nhdsWithin iteratedFDerivWithin	—	Filter.Eventually.mono DFunLike.ext SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self fderivWithin' RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd RingHomIsometric.ids ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul
iteratedFDerivWithin_eq 📖	mathematical	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	iteratedFDerivWithin	—	nhdsWithin_insert Filter.Eventually.self_of_nhdsWithin iteratedFDerivWithin' Set.subset_insert Set.mem_insert

HasCompactSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iteratedFDeriv 📖	mathematical	HasCompactSupport UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	HasCompactSupport ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.instZero iteratedFDeriv	—	IsCompact.of_isClosed_subset isClosed_closure tsupport_iteratedFDeriv_subset

HasFTaylorSeriesUpTo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cont 📖	mathematical	HasFTaylorSeriesUpTo WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat WithTop.natCast ENat.instNatCast	Continuous 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.instTopologicalSpace NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
continuous 📖	mathematical	HasFTaylorSeriesUpTo	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul continuousOn_univ HasFTaylorSeriesUpToOn.continuousOn hasFTaylorSeriesUpToOn_univ_iff
differentiable 📖	mathematical	HasFTaylorSeriesUpTo	Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul HasFDerivAt.differentiableAt RingHomInvPair.ids RingHomIsometric.ids smulCommClass_self hasFDerivAt
eq_iteratedFDeriv 📖	mathematical	HasFTaylorSeriesUpTo WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat WithTop.natCast ENat.instNatCast	iteratedFDeriv	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul iteratedFDerivWithin_univ HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn hasFTaylorSeriesUpToOn_univ_iff uniqueDiffOn_univ NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul Set.mem_univ
fderiv 📖	mathematical	HasFTaylorSeriesUpTo WithTop ENat Preorder.toLT WithTop.instPreorder instPreorderENat WithTop.natCast ENat.instNatCast	HasFDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instModule IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup 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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.curryLeft	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
fderiv_eq 📖	mathematical	HasFTaylorSeriesUpTo WithTop ENat Preorder.toLT WithTop.instPreorder instPreorderENat WithTop.natCast ENat.instNatCast	fderiv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.curryLeft	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul HasFDerivAt.fderiv smulCommClass_self IsBoundedSMul.continuousSMul ContinuousMultilinearMap.instIsTopologicalAddGroup ContinuousMultilinearMap.instContinuousSMul ContinuousMultilinearMap.instT2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace fderiv
hasFDerivAt 📖	mathematical	HasFTaylorSeriesUpTo	HasFDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousMultilinearMap.instModule SeminormedAddCommGroup.toAddCommGroup 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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike continuousMultilinearCurryFin1	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomInvPair.ids RingHomIsometric.ids smulCommClass_self hasFDerivWithinAt_univ HasFTaylorSeriesUpToOn.hasFDerivWithinAt hasFTaylorSeriesUpToOn_univ_iff Set.mem_univ
hasFTaylorSeriesUpToOn 📖	mathematical	HasFTaylorSeriesUpTo	HasFTaylorSeriesUpToOn	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul HasFTaylorSeriesUpToOn.mono hasFTaylorSeriesUpToOn_univ_iff Set.subset_univ
of_le 📖	mathematical	HasFTaylorSeriesUpTo WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat	HasFTaylorSeriesUpTo	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul hasFTaylorSeriesUpToOn_univ_iff HasFTaylorSeriesUpToOn.of_le
tsupport_mono 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat WithTop.natCast ENat.instNatCast HasFTaylorSeriesUpTo	Set Set.instHasSubset tsupport ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.instZero	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul subset_refl Set.instReflSubset lt_of_lt_of_le WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass WithTop.charZero lt_add_one Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid Nat.instIsOrderedAddMonoid subset_trans Set.instIsTransSubset Eq.trans_subset smulCommClass_self fderiv_eq tsupport_comp_eq LinearIsometryEquiv.map_eq_zero_iff RingHomInvPair.ids RingHomIsometric.ids ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul tsupport_fderiv_subset LT.lt.le
tsupport_subset 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat WithTop.natCast ENat.instNatCast HasFTaylorSeriesUpTo	Set Set.instHasSubset tsupport ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul LE.le.trans_eq tsupport_mono zero_le Nat.instCanonicallyOrderedAdd zero_eq tsupport_comp_eq LinearIsometryEquiv.map_eq_zero_iff RingHomInvPair.ids smulCommClass_self
zero_eq 📖	mathematical	HasFTaylorSeriesUpTo	ContinuousMultilinearMap.curry0	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
zero_eq' 📖	mathematical	HasFTaylorSeriesUpTo	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype ContinuousMultilinearMap.instModule SeminormedAddCommGroup.toAddCommGroup 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 smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm continuousMultilinearCurryFin0	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomInvPair.ids smulCommClass_self zero_eq ContinuousMultilinearMap.uncurry0_curry0

HasFTaylorSeriesUpToOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_series 📖	mathematical	HasFTaylorSeriesUpToOn Set.EqOn 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	HasFTaylorSeriesUpToOn	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul zero_le WithTop.canonicallyOrderedAdd zero_eq HasFDerivWithinAt.congr_fderiv smulCommClass_self HasFDerivWithinAt.congr' fderivWithin Set.EqOn.symm LT.lt.le ENat.add_one_natCast_le_withTop_of_lt ContinuousOn.congr cont
cont 📖	mathematical	HasFTaylorSeriesUpToOn WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat WithTop.natCast ENat.instNatCast	ContinuousOn 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.instTopologicalSpace NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
continuousOn 📖	mathematical	HasFTaylorSeriesUpToOn	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomInvPair.ids smulCommClass_self ContinuousOn.congr cont bot_le zero_eq' LinearIsometryEquiv.comp_continuousOn_iff
differentiableAt 📖	mathematical	HasFTaylorSeriesUpToOn Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul HasFDerivAt.differentiableAt RingHomInvPair.ids RingHomIsometric.ids smulCommClass_self hasFDerivAt
differentiableOn 📖	mathematical	HasFTaylorSeriesUpToOn	DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul HasFDerivWithinAt.differentiableWithinAt RingHomInvPair.ids RingHomIsometric.ids smulCommClass_self hasFDerivWithinAt
eq_iteratedFDerivWithin_of_uniqueDiffOn 📖	mathematical	HasFTaylorSeriesUpToOn WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat WithTop.natCast ENat.instNatCast UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instMembership	iteratedFDerivWithin	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomInvPair.ids smulCommClass_self zero_eq' iteratedFDerivWithin_zero_eq_comp lt_of_lt_of_le WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass WithTop.charZero lt_add_one Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid Nat.instIsOrderedAddMonoid HasFDerivWithinAt.congr fderivWithin le_of_lt RingHomIsometric.ids ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul iteratedFDerivWithin_succ_eq_comp_left HasFDerivWithinAt.fderivWithin IsBoundedSMul.continuousSMul ContinuousMultilinearMap.instIsTopologicalAddGroup ContinuousMultilinearMap.instContinuousSMul ContinuousMultilinearMap.instT2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ContinuousMultilinearMap.uncurry_curryLeft
eventually_hasFDerivAt 📖	mathematical	HasFTaylorSeriesUpToOn Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	Filter.Eventually HasFDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousMultilinearMap.instModule SeminormedAddCommGroup.toAddCommGroup 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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike continuousMultilinearCurryFin1 nhds	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Filter.Eventually.mono RingHomInvPair.ids RingHomIsometric.ids smulCommClass_self eventually_eventually_nhds hasFDerivAt
fderivWithin 📖	mathematical	HasFTaylorSeriesUpToOn WithTop ENat Preorder.toLT WithTop.instPreorder instPreorderENat WithTop.natCast ENat.instNatCast Set Set.instMembership	HasFDerivWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instModule IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup 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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.curryLeft	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
hasFDerivAt 📖	mathematical	HasFTaylorSeriesUpToOn Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	HasFDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousMultilinearMap.instModule SeminormedAddCommGroup.toAddCommGroup 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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike continuousMultilinearCurryFin1	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul HasFDerivWithinAt.hasFDerivAt RingHomInvPair.ids RingHomIsometric.ids smulCommClass_self hasFDerivWithinAt mem_of_mem_nhds
hasFDerivWithinAt 📖	mathematical	HasFTaylorSeriesUpToOn Set Set.instMembership	HasFDerivWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousMultilinearMap.instModule SeminormedAddCommGroup.toAddCommGroup 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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike continuousMultilinearCurryFin1	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomInvPair.ids smulCommClass_self zero_eq RingHomIsometric.ids RingHomCompTriple.ids LinearIsometryEquiv.comp_hasFDerivWithinAt_iff' pos_iff_ne_zero WithTop.canonicallyOrderedAdd ContinuousLinearMap.ext ContinuousMultilinearMap.ext Unique.eq_default fderivWithin HasFDerivWithinAt.congr
mono 📖	mathematical	HasFTaylorSeriesUpToOn Set Set.instHasSubset	HasFTaylorSeriesUpToOn	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul zero_eq HasFDerivWithinAt.mono smulCommClass_self fderivWithin ContinuousOn.mono cont
of_le 📖	mathematical	HasFTaylorSeriesUpToOn WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat	HasFTaylorSeriesUpToOn	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul zero_eq fderivWithin lt_of_lt_of_le cont le_trans
shift_of_succ 📖	mathematical	HasFTaylorSeriesUpToOn WithTop ENat WithTop.natCast ENat.instNatCast	HasFTaylorSeriesUpToOn 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 ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing WithTop ENat WithTop.natCast ENat.instNatCast DFunLike.coe LinearIsometryEquiv RingHomInvPair.ids ContinuousMultilinearMap ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype ContinuousLinearMap.toSeminormedAddCommGroup ContinuousMultilinearMap.instModule SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace 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 ContinuousLinearMap.module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike continuousMultilinearCurryFin1 FormalMultilinearSeries.shift	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomIsometric.ids smulCommClass_self RingHomInvPair.ids Nat.cast_lt WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass WithTop.charZero ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.continuousConstSMul ContinuousLinearMap.smulCommClass RingHomCompTriple.ids LinearIsometryEquiv.comp_hasFDerivWithinAt_iff' ContinuousLinearMap.ext ContinuousMultilinearMap.ext Fin.cons_snoc_eq_snoc_cons Fin.snoc_init_self fderivWithin cont Nat.cast_le Continuous.comp_continuousOn LinearIsometryEquiv.continuous
zero_eq 📖	mathematical	HasFTaylorSeriesUpToOn Set Set.instMembership	ContinuousMultilinearMap.curry0	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
zero_eq' 📖	mathematical	HasFTaylorSeriesUpToOn Set Set.instMembership	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype ContinuousMultilinearMap.instModule SeminormedAddCommGroup.toAddCommGroup 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 smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm continuousMultilinearCurryFin0	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomInvPair.ids smulCommClass_self zero_eq ContinuousMultilinearMap.uncurry0_curry0

Set.EqOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iteratedFDerivWithin 📖	mathematical	Set.EqOn	Set.EqOn 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 iteratedFDerivWithin	—	iteratedFDerivWithin_congr

(root)

Definitions

Name	Category	Theorems
HasFTaylorSeriesUpTo 📖	CompData	11 math math: hasFTaylorSeriesUpToOn_univ_iff, hasFTaylorSeriesUpTo_zero_iff, ContinuousMultilinearMap.hasFTaylorSeriesUpTo_iteratedFDeriv, hasFTaylorSeriesUpTo_top_iff', hasFTaylorSeriesUpTo_succ_nat_iff_right, HasFTaylorSeriesUpTo.of_le, VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral', ContDiff.ftaylorSeries, contDiff_iff_ftaylorSeries, hasFTaylorSeriesUpTo_top_iff, VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral
HasFTaylorSeriesUpToOn 📖	CompData	33 math math: AnalyticOn.exists_hasFTaylorSeriesUpToOn, hasFTaylorSeriesUpToOn_top_iff_right, hasFTaylorSeriesUpToOn_univ_iff, hasFTaylorSeriesUpToOn_empty, HasFTaylorSeriesUpToOn.comp_continuousAffineMap, contDiffWithinAt_nat, HasFTaylorSeriesUpToOn.of_le, contDiffWithinAt_iff_of_ne_infty, hasFTaylorSeriesUpToOn_pi', HasFTaylorSeriesUpToOn.mono, hasFTaylorSeriesUpToOn_top_iff', hasFTaylorSeriesUpToOn_zero_iff, hasFTaylorSeriesUpToOn_succ_iff_right, HasFTaylorSeriesUpToOn.comp, HasFTaylorSeriesUpToOn.continuousLinearMap_comp, hasFTaylorSeriesUpToOn_top_iff, hasFTaylorSeriesUpToOn_succ_nat_iff_right, HasFTaylorSeriesUpToOn.congr, ContDiffWithinAt.eventually_hasFTaylorSeriesUpToOn, HasFTaylorSeriesUpToOn.shift_of_succ, HasFTaylorSeriesUpTo.hasFTaylorSeriesUpToOn, HasFTaylorSeriesUpToOn.compContinuousLinearMap, HasFTaylorSeriesUpToOn.add, HasFTaylorSeriesUpToOn.prodMk, hasFTaylorSeriesUpToOn_succ_iff_left, AnalyticOn.hasFTaylorSeriesUpToOn, AnalyticOnNhd.hasFTaylorSeriesUpToOn, HasFTaylorSeriesUpToOn.congr_series, ContDiffOn.ftaylorSeriesWithin, HasFTaylorSeriesUpToOn.restrictScalars, hasFTaylorSeriesUpToOn_top_iff_add, hasFTaylorSeriesUpToOn_pi, AnalyticWithinAt.exists_hasFTaylorSeriesUpToOn
ftaylorSeries 📖	CompOp	8 math math: iteratedFDeriv_comp, Filter.EventuallyEq.ftaylorSeries, ftaylorSeries_fun_zero, ContDiff.ftaylorSeries, contDiff_iff_ftaylorSeries, ftaylorSeries_zero, AnalyticOnNhd.hasFTaylorSeriesUpToOn, ftaylorSeriesWithin_univ
ftaylorSeriesWithin 📖	CompOp	10 math math: ftaylorSeriesWithin_insert, Filter.EventuallyEq.ftaylorSeriesWithin, ftaylorSeriesWithin_zero, ContDiffWithinAt.eventually_hasFTaylorSeriesUpToOn, iteratedFDerivWithin_comp, AnalyticOn.hasFTaylorSeriesUpToOn, iteratedFDerivWithin_comp_of_eventually_mem, ContDiffOn.ftaylorSeriesWithin, ftaylorSeriesWithin_univ, ftaylorSeriesWithin_fun_zero
iteratedFDeriv 📖	CompOp	157 math math: fderiv_iteratedFDeriv, iteratedFDeriv_comp, fun_iteratedFDeriv_add_apply, ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm, ContDiff.iteratedFDeriv_right, iteratedFDeriv_sum_apply, ContDiffMapSupportedIn.iteratedFDerivLM_apply, norm_iteratedFDeriv_comp_le', norm_iteratedFDeriv_mul_le, AnalyticOnNhd.iteratedFDeriv_of_isOpen, ContDiffMapSupportedIn.structureMapCLM_apply, bilinearIteratedFDerivTwo_eq_iteratedFDeriv, ContDiffPointwiseHolderAt.isBigO, SchwartzMap.decay', ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear_of_le_one, norm_iteratedFDeriv_clm_apply, tensorIteratedFDerivTwo_eq_iteratedFDeriv, AnalyticOnNhd.iteratedFDeriv, HasFPowerSeriesOnBall.hasSum_iteratedFDeriv, Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform_aux, iteratedFDerivWithin_eq_iteratedFDeriv, iteratedFDerivWithin_of_isOpen, MeasureTheory.iteratedFDeriv_charFun, Real.fourier_iteratedFDeriv, iteratedFDeriv_comp_const_smul, iteratedFDeriv_zero, iteratedFDeriv_add_apply, ContDiffMapSupportedIn.seminorm_le_iff, iteratedFDeriv_sum, VectorFourier.fourierIntegral_iteratedFDeriv, VectorFourier.norm_iteratedFDeriv_fourierPowSMulRight, Function.hasTemperateGrowth_iff_isBigO, iteratedFDeriv_comp_sub, iteratedFDeriv_const_smul_apply, iteratedFDeriv_succ_const, ContDiffAt.iteratedFDeriv_right, CPolynomialOn.iteratedFDeriv, iteratedFDeriv_const_smul_apply', ContDiff.differentiable_iteratedFDeriv, HasFTaylorSeriesUpTo.eq_iteratedFDeriv, VectorFourier.iteratedFDeriv_fourierIntegral, isSymmSndFDerivAt_iff_iteratedFDeriv, AnalyticOn.domDomCongr_iteratedFDeriv, SchwartzMap.norm_iteratedFDeriv_le_seminorm, fun_iteratedFDeriv_add, fun_iteratedFDeriv_sub, iteratedFDeriv_tsum, Real.pow_mul_norm_iteratedFDeriv_fourier_le, contDiff_iff_continuous_differentiable, iteratedFDeriv_comp_add_left, iteratedFDeriv_neg_apply, ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear, contDiffPointwiseHolderAt_iff, LinearIsometry.norm_iteratedFDeriv_comp_left, Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform, ContDiffMapSupportedIn.seminorm_top_le_iff, iteratedFDeriv_add, iteratedFDeriv_eq_equiv_comp, iteratedDeriv_vcomp_three, ContinuousMultilinearMap.iteratedFDeriv_eq, ContDiffAt.restrictScalars_iteratedFDeriv_eventuallyEq, ContDiffAt.restrictScalars_iteratedFDeriv, norm_fderiv_iteratedFDeriv, ContinuousMultilinearMap.iteratedFDeriv_comp_diagonal, iteratedDeriv_vcomp_eq_sum_orderedFinpartition, SchwartzMap.integral_pow_mul_iteratedFDeriv_le, iteratedDeriv_eq_equiv_comp, iteratedFDeriv_zero_apply, VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le, ContinuousLinearMap.norm_iteratedFDeriv_comp_left, ContDiff.continuous_iteratedFDeriv', SchwartzMap.le_seminorm, AnalyticOn.iteratedFDeriv_comp_perm, iteratedFDeriv_fun_sum_apply, iteratedFDeriv_one_apply, ContinuousLinearEquiv.iteratedFDeriv_comp_left, HasFPowerSeriesOnBall.factorial_smul, iteratedFDeriv_succ_apply_right, LinearIsometryEquiv.norm_iteratedFDeriv_comp_right, IsSymmSndFDerivAt.iteratedFDeriv_cons, ContDiffMapSupportedIn.iteratedFDeriv_zero_on_compl, ContinuousMultilinearMap.norm_iteratedFDeriv_le, ContDiffAt.domDomCongr_iteratedFDeriv, iteratedFDeriv_comp_sub', support_iteratedFDeriv_subset, InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, iteratedFDeriv_smul_const_apply, HasCompactSupport.iteratedFDeriv, iteratedFDeriv_succ_eq_comp_right, SchwartzMap.iteratedPDeriv_eq_iteratedFDeriv, tsupport_iteratedFDeriv_subset, Real.iteratedFDeriv_fourier, ContDiffMapSupportedIn.structureMapCLM_top_apply, ContDiff.continuous_iteratedFDeriv, iteratedFDeriv_comp_add_left', InnerProductSpace.laplacian_eq_iteratedFDeriv_complexPlane, ContDiff.iteratedFDeriv_right', iteratedFDerivWithin_zero_eq, ContDiffMapSupportedIn.structureMapLM_top_apply, norm_iteratedFDeriv_comp_le, norm_iteratedFDeriv_prod_le, contDiff_nat_iff_continuous_differentiable, SchwartzMap.iteratedLineDerivOp_eq_iteratedFDeriv, ContDiffAt.iteratedFDeriv_comp_perm, iteratedDeriv_eq_iteratedFDeriv, iteratedFDeriv_comp_add_right, iteratedFDeriv_zero_fun, fun_iteratedFDeriv_sub_apply, norm_iteratedFDeriv_one, Real.pow_mul_norm_iteratedFDeriv_fourierIntegral_le, iteratedFDeriv_zero_eq_comp, iteratedFDeriv_sub, iteratedFDeriv_fun_zero, SchwartzMap.decay, iteratedFDeriv_prodMk, InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis, Filter.EventuallyEq.iteratedFDeriv, HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum_of_completeSpace, Real.iteratedFDeriv_fourierIntegral, HasFPowerSeriesOnBall.iteratedFDeriv_zero_apply_diag, ContDiffMapSupportedIn.bounded_iteratedFDeriv, iteratedFDeriv_two_apply, iteratedFDeriv_comp_add_right', iteratedFDeriv_succ_eq_comp_left, VectorFourier.fourierPowSMulRight_iteratedFDeriv_fourierIntegral, ContDiffPointwiseHolderAt.iteratedFDeriv, ContDiffAt.continuousAt_iteratedFDeriv, iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod, iteratedFDeriv_sub_apply, norm_iteratedFDeriv_smul_le, ContDiffAt.differentiableAt_iteratedFDeriv, iteratedDeriv_vcomp_two, ContinuousOn.continuousOn_iteratedFDeriv, iteratedFDeriv_clm_apply_const_apply, ContinuousLinearMap.iteratedFDeriv_comp_right, norm_iteratedFDeriv_zero, norm_iteratedFDeriv_eq_norm_iteratedDeriv, ContinuousLinearMap.iteratedFDeriv_comp_left, LinearIsometryEquiv.norm_iteratedFDeriv_comp_left, iteratedFDeriv_tsum_apply, SchwartzMap.one_add_le_sup_seminorm_apply, ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm_top, VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, SchwartzMap.integrable_pow_mul_iteratedFDeriv, iteratedFDeriv_neg, Real.fourierIntegral_iteratedFDeriv, Function.HasTemperateGrowth.isBigO_uniform, ContDiffMapSupportedIn.structureMapLM_apply, iteratedFDerivWithin_univ, HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum, norm_iteratedFDeriv_fderiv, Function.HasTemperateGrowth.isBigO, iteratedFDeriv_add_apply', iteratedFDeriv_succ_apply_left, iteratedFDeriv_const_of_ne, ContDiffMapSupportedIn.iteratedFDerivLM_apply_of_le, norm_iteratedFDeriv_clm_apply_const
iteratedFDerivWithin 📖	CompOp	111 math math: AnalyticOn.domDomCongr_iteratedFDerivWithin, norm_iteratedFDerivWithin_smul_le, iteratedFDerivWithin_eventually_congr_set, norm_iteratedFDerivWithin_one, iteratedFDerivWithin_succ_eq_comp_right, iteratedDerivWithin_vcomp_two, norm_iteratedFDerivWithin_clm_apply, dist_iteratedFDerivWithin_one, norm_iteratedFDerivWithin_comp_le_aux, AnalyticOn.iteratedFDerivWithin, iteratedFDerivWithin_succ_eq_comp_left, contDiffOn_iff_continuousOn_differentiableOn, iteratedFDerivWithin_comp_add_right', AnalyticOn.iteratedFDerivWithin_comp_perm, iteratedFDerivWithin_succ_const, iteratedFDerivWithin_eq_iteratedFDeriv, norm_iteratedFDerivWithin_zero, iteratedFDerivWithin_of_isOpen, iteratedDerivWithin_eq_iteratedFDerivWithin, iteratedFDerivWithin_congr_set', ContinuousLinearMap.norm_iteratedFDerivWithin_comp_left, norm_iteratedFDerivWithin_clm_apply_const, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_complexPlane, ContDiffWithinAt.continuousWithinAt_iteratedFDerivWithin, tensorIteratedFDerivWithinTwo_eq_iteratedFDerivWithin, iteratedFDerivWithin_comp_add_left, iteratedFDerivWithin_const_smul_apply, iteratedFDerivWithin_neg_apply, iteratedFDerivWithin_succ_apply_right, ContDiffOn.continuousOn_iteratedFDerivWithin, iteratedFDerivWithin_inter', contDiffOn_nat_iff_continuousOn_differentiableOn, fun_iteratedFDerivWithin_add_apply, ContinuousLinearEquiv.iteratedFDerivWithin_comp_right, iteratedFDerivWithin_smul_const_apply, iteratedFDerivWithin_eq_equiv_comp, ContDiffWithinAt.restrictScalars_iteratedFDerivWithin_eventuallyEq, Filter.EventuallyEq.iteratedFDerivWithin, ContinuousLinearMap.iteratedFDerivWithin_comp_left, ContinuousLinearMap.iteratedFDerivWithin_comp_right, iteratedFDerivWithin_one_apply, ContDiffWithinAt.domDomCongr_iteratedFDerivWithin, iteratedFDerivWithin_comp_sub, dist_iteratedFDerivWithin_zero, norm_iteratedFDerivWithin_prod_le, fderivWithin_iteratedFDerivWithin, LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left, iteratedFDerivWithin_two_apply', Filter.EventuallyEq.iteratedFDerivWithin', ContinuousOn.continuousOn_iteratedFDerivWithin, iteratedFDerivWithin_succ_apply_left, iteratedFDerivWithin_add_apply, iteratedFDerivWithin_zero, iteratedFDerivWithin_prodMk, iteratedFDerivWithin_comp_add_right, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis, LinearIsometry.norm_iteratedFDerivWithin_comp_left, norm_fderivWithin_iteratedFDerivWithin, HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_zero, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis, fun_iteratedFDerivWithin_sub_apply, Set.EqOn.iteratedFDerivWithin, ContDiffWithinAt.differentiableWithinAt_iteratedFDerivWithin, ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear, norm_iteratedFDerivWithin_comp_le, bilinearIteratedFDerivWithinTwo_eq_iteratedFDeriv, iteratedFDerivWithin_zero_eq, LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_right, iteratedFDerivWithin_fun_sum_apply, iteratedFDerivWithin_insert, HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_completeSpace, iteratedFDerivWithin_comp, iteratedFDerivWithin_comp_add_left', iteratedFDerivWithin_eventually_congr_set', HasFPowerSeriesWithinOnBall.iteratedFDerivWithin, ContDiffWithinAt.iteratedFDerivWithin_right, iteratedFDerivWithin_sub_apply, iteratedDerivWithin_eq_equiv_comp, iteratedFDerivWithin_two_apply, iteratedFDerivWithin_fun_zero, ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one, iteratedFDerivWithin_zero_eq_comp, iteratedFDerivWithin_congr, HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn, iteratedFDerivWithin_comp_of_eventually_mem, iteratedFDerivWithin_inter, iteratedFDerivWithin_sum_apply, iteratedFDerivWithin_clm_apply_const_apply, isSymmSndFDerivWithinAt_iff_iteratedFDerivWithin, iteratedFDerivWithin_inter_open, ContDiffWithinAt.iteratedFDerivWithin_comp_perm, iteratedFDerivWithin_const_of_ne, norm_iteratedFDerivWithin_mul_le, iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition, iteratedFDerivWithin_zero_fun, Filter.EventuallyEq.iteratedFDerivWithin_eq, norm_iteratedFDerivWithin_fderivWithin, iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod, iteratedFDerivWithin_comp_sub', norm_iteratedFDerivWithin_eq_norm_iteratedDerivWithin, ContDiffOn.differentiableOn_iteratedFDerivWithin, ContinuousLinearEquiv.iteratedFDerivWithin_comp_left, HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum, iteratedFDerivWithin_subset, iteratedFDerivWithin_zero_apply, iteratedFDerivWithin_univ, iteratedFDerivWithin_congr_set, iteratedFDerivWithin_add_apply', IsSymmSndFDerivWithinAt.iteratedFDerivWithin_cons, iteratedDerivWithin_vcomp_three, ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_aux

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_iteratedFDerivWithin_one 📖	mathematical	UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Dist.dist 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 PseudoMetricSpace.toDist ContinuousMultilinearMap.instPseudoMetricSpace Fin.fintype iteratedFDerivWithin ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.toPseudoMetricSpace RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing fderivWithin	—	RingHomIsometric.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self RingHomCompTriple.ids RingHomInvPair.ids ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul LinearIsometryEquiv.comp_fderivWithin LinearIsometryEquiv.dist_map LinearIsometry.dist_map
dist_iteratedFDerivWithin_zero 📖	mathematical	—	Dist.dist 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 PseudoMetricSpace.toDist ContinuousMultilinearMap.instPseudoMetricSpace Fin.fintype iteratedFDerivWithin	—	LinearIsometryEquiv.dist_map RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self
fderivWithin_iteratedFDerivWithin 📖	mathematical	—	fderivWithin NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousMultilinearMap.instTopologicalSpace iteratedFDerivWithin ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup DFunLike.coe LinearIsometryEquiv RingHomInvPair.ids ContinuousMultilinearMap.seminormedAddCommGroup Fin.fintype ContinuousLinearMap.toSeminormedAddCommGroup ContinuousMultilinearMap.normedSpace RingHomIsometric.ids SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap.module ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul EquivLike.toFunLike LinearIsometryEquiv.instEquivLike continuousMultilinearCurryLeftEquiv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self
fderiv_iteratedFDeriv 📖	mathematical	—	fderiv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousMultilinearMap.instTopologicalSpace iteratedFDeriv ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup DFunLike.coe LinearIsometryEquiv RingHomInvPair.ids ContinuousMultilinearMap.seminormedAddCommGroup Fin.fintype ContinuousLinearMap.toSeminormedAddCommGroup ContinuousMultilinearMap.normedSpace RingHomIsometric.ids SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap.module ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul EquivLike.toFunLike LinearIsometryEquiv.instEquivLike continuousMultilinearCurryLeftEquiv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self
ftaylorSeriesWithin_insert 📖	mathematical	—	ftaylorSeriesWithin Set Set.instInsert	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul FormalMultilinearSeries.ext iteratedFDerivWithin_insert
ftaylorSeriesWithin_univ 📖	mathematical	—	ftaylorSeriesWithin Set.univ ftaylorSeries	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul FormalMultilinearSeries.ext iteratedFDerivWithin_univ
hasFTaylorSeriesUpToOn_empty 📖	mathematical	—	HasFTaylorSeriesUpToOn Set Set.instEmptyCollection	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Matrix.zero_empty instIsEmptyFalse smulCommClass_self
hasFTaylorSeriesUpToOn_succ_iff_left 📖	mathematical	—	HasFTaylorSeriesUpToOn WithTop ENat WithTop.add instAddENat WithTop.natCast ENat.instNatCast WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat HasFDerivWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instModule IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup 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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.curryLeft ContinuousOn	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self HasFTaylorSeriesUpToOn.of_le Nat.cast_one WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass WithTop.charZero HasFTaylorSeriesUpToOn.fderivWithin lt_add_one Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid Nat.instIsOrderedAddMonoid HasFTaylorSeriesUpToOn.cont le_rfl HasFTaylorSeriesUpToOn.zero_eq le_antisymm not_le
hasFTaylorSeriesUpToOn_succ_iff_right 📖	mathematical	—	HasFTaylorSeriesUpToOn WithTop ENat WithTop.add instAddENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat ContinuousMultilinearMap.curry0 HasFDerivWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instModule IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup 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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.curryLeft ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids ContinuousLinearMap.toNormedSpace DFunLike.coe LinearIsometryEquiv RingHomInvPair.ids ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype ContinuousLinearMap.toSeminormedAddCommGroup SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap.module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike continuousMultilinearCurryFin1 FormalMultilinearSeries.shift	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self RingHomIsometric.ids RingHomInvPair.ids hasFTaylorSeriesUpToOn_top_iff_right instReflLe hasFTaylorSeriesUpToOn_succ_nat_iff_right
hasFTaylorSeriesUpToOn_succ_nat_iff_right 📖	mathematical	—	HasFTaylorSeriesUpToOn WithTop ENat WithTop.natCast ENat.instNatCast ContinuousMultilinearMap.curry0 HasFDerivWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instModule IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup 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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.curryLeft ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids ContinuousLinearMap.toNormedSpace DFunLike.coe LinearIsometryEquiv RingHomInvPair.ids ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype ContinuousLinearMap.toSeminormedAddCommGroup SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap.module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike continuousMultilinearCurryFin1 FormalMultilinearSeries.shift	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self RingHomIsometric.ids RingHomInvPair.ids HasFTaylorSeriesUpToOn.zero_eq HasFTaylorSeriesUpToOn.fderivWithin Nat.cast_lt WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass WithTop.charZero HasFTaylorSeriesUpToOn.shift_of_succ ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.continuousConstSMul ContinuousLinearMap.smulCommClass RingHomCompTriple.ids ContinuousLinearMap.ext ContinuousMultilinearMap.ext Fin.cons_snoc_eq_snoc_cons Fin.snoc_init_self LinearIsometryEquiv.comp_hasFDerivWithinAt_iff' HasFDerivWithinAt.differentiableWithinAt DifferentiableOn.continuousOn IsBoundedSMul.continuousSMul ContinuousMultilinearMap.instIsTopologicalAddGroup ContinuousMultilinearMap.instContinuousSMul LinearIsometryEquiv.comp_continuousOn_iff HasFTaylorSeriesUpToOn.cont Nat.cast_le
hasFTaylorSeriesUpToOn_top_iff 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat WithTop.some Top.top instTopENat	HasFTaylorSeriesUpToOn WithTop ENat WithTop.natCast ENat.instNatCast	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul add_zero hasFTaylorSeriesUpToOn_top_iff_add
hasFTaylorSeriesUpToOn_top_iff' 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat WithTop.some Top.top instTopENat	HasFTaylorSeriesUpToOn ContinuousMultilinearMap.curry0 HasFDerivWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instModule IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup 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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.curryLeft	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self HasFTaylorSeriesUpToOn.zero_eq HasFTaylorSeriesUpToOn.fderivWithin ENat.natCast_lt_of_coe_top_le_withTop HasFDerivWithinAt.continuousWithinAt IsBoundedSMul.continuousSMul ContinuousMultilinearMap.instIsTopologicalAddGroup ContinuousMultilinearMap.instContinuousSMul
hasFTaylorSeriesUpToOn_top_iff_add 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat WithTop.some Top.top instTopENat	HasFTaylorSeriesUpToOn WithTop ENat WithTop.natCast ENat.instNatCast	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul HasFTaylorSeriesUpToOn.of_le ENat.natCast_le_of_coe_top_le_withTop HasFTaylorSeriesUpToOn.zero_eq HasFTaylorSeriesUpToOn.fderivWithin WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass WithTop.charZero HasFTaylorSeriesUpToOn.cont Nat.cast_add WithTop.canonicallyOrderedAdd
hasFTaylorSeriesUpToOn_top_iff_right 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat WithTop.some Top.top instTopENat	HasFTaylorSeriesUpToOn ContinuousMultilinearMap.curry0 HasFDerivWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instModule IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup 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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.curryLeft ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids ContinuousLinearMap.toNormedSpace DFunLike.coe LinearIsometryEquiv RingHomInvPair.ids ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype ContinuousLinearMap.toSeminormedAddCommGroup SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap.module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike continuousMultilinearCurryFin1 FormalMultilinearSeries.shift	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self RingHomIsometric.ids RingHomInvPair.ids hasFTaylorSeriesUpToOn_top_iff hasFTaylorSeriesUpToOn_succ_nat_iff_right hasFTaylorSeriesUpToOn_top_iff_add HasFTaylorSeriesUpToOn.of_le ENat.natCast_le_of_coe_top_le_withTop
hasFTaylorSeriesUpToOn_univ_iff 📖	mathematical	—	HasFTaylorSeriesUpToOn Set.univ HasFTaylorSeriesUpTo	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul HasFTaylorSeriesUpToOn.zero_eq Set.mem_univ smulCommClass_self hasFDerivWithinAt_univ HasFTaylorSeriesUpToOn.fderivWithin continuousOn_univ HasFTaylorSeriesUpToOn.cont HasFTaylorSeriesUpTo.zero_eq HasFTaylorSeriesUpTo.fderiv HasFTaylorSeriesUpTo.cont
hasFTaylorSeriesUpToOn_zero_iff 📖	mathematical	—	HasFTaylorSeriesUpToOn WithTop ENat WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ContinuousMultilinearMap.curry0	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul HasFTaylorSeriesUpToOn.continuousOn HasFTaylorSeriesUpToOn.zero_eq smulCommClass_self not_le bot_le RingHomInvPair.ids LinearEquiv.eq_symm_apply continuousOn_congr LinearIsometryEquiv.comp_continuousOn_iff Nat.cast_zero WithTop.charZero LE.le.antisymm zero_le WithTop.canonicallyOrderedAdd
hasFTaylorSeriesUpTo_succ_nat_iff_right 📖	mathematical	—	HasFTaylorSeriesUpTo WithTop ENat WithTop.natCast ENat.instNatCast ContinuousMultilinearMap.curry0 HasFDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instModule IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup 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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.curryLeft ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids ContinuousLinearMap.toNormedSpace DFunLike.coe LinearIsometryEquiv RingHomInvPair.ids ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype ContinuousLinearMap.toSeminormedAddCommGroup SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap.module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike continuousMultilinearCurryFin1 FormalMultilinearSeries.shift	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self RingHomIsometric.ids RingHomInvPair.ids
hasFTaylorSeriesUpTo_top_iff 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat WithTop.some Top.top instTopENat	HasFTaylorSeriesUpTo WithTop ENat WithTop.natCast ENat.instNatCast	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul hasFTaylorSeriesUpToOn_top_iff
hasFTaylorSeriesUpTo_top_iff' 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat WithTop.some Top.top instTopENat	HasFTaylorSeriesUpTo ContinuousMultilinearMap.curry0 HasFDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instModule IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup 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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.curryLeft	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self hasFTaylorSeriesUpToOn_top_iff'
hasFTaylorSeriesUpTo_zero_iff 📖	mathematical	—	HasFTaylorSeriesUpTo WithTop ENat WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ContinuousMultilinearMap.curry0	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul hasFTaylorSeriesUpToOn_univ_iff Matrix.zero_empty
iteratedFDerivWithin_comp_add_left 📖	mathematical	—	iteratedFDerivWithin AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup addGroupIsAddTorsor	—	iteratedFDerivWithin_comp_add_left'
iteratedFDerivWithin_comp_add_left' 📖	mathematical	—	iteratedFDerivWithin AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup addGroupIsAddTorsor	—	ContinuousMultilinearMap.ext SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self RingHomInvPair.ids RingHomIsometric.ids ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul iteratedFDerivWithin_succ_eq_comp_left fderivWithin_comp_add_left
iteratedFDerivWithin_comp_add_right 📖	mathematical	—	iteratedFDerivWithin AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup addGroupIsAddTorsor	—	iteratedFDerivWithin_comp_add_right'
iteratedFDerivWithin_comp_add_right' 📖	mathematical	—	iteratedFDerivWithin AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup addGroupIsAddTorsor	—	add_comm iteratedFDerivWithin_comp_add_left'
iteratedFDerivWithin_comp_sub 📖	mathematical	—	iteratedFDerivWithin SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction addGroupIsAddTorsor NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	iteratedFDerivWithin_comp_sub'
iteratedFDerivWithin_comp_sub' 📖	mathematical	—	iteratedFDerivWithin SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction addGroupIsAddTorsor NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	sub_eq_add_neg iteratedFDerivWithin_comp_add_right'
iteratedFDerivWithin_congr 📖	mathematical	Set.EqOn Set Set.instMembership	iteratedFDerivWithin	—	Filter.EventuallyEq.iteratedFDerivWithin_eq Filter.EventuallyEq.filter_mono Set.EqOn.eventuallyEq inf_le_right
iteratedFDerivWithin_congr_set 📖	mathematical	Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	iteratedFDerivWithin	—	Filter.Eventually.self_of_nhds iteratedFDerivWithin_eventually_congr_set
iteratedFDerivWithin_congr_set' 📖	mathematical	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Compl.compl Set Set.instCompl Set.instSingletonSet	iteratedFDerivWithin	—	Filter.Eventually.self_of_nhds iteratedFDerivWithin_eventually_congr_set'
iteratedFDerivWithin_eventually_congr_set 📖	mathematical	Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	Filter.EventuallyEq 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 nhds iteratedFDerivWithin	—	iteratedFDerivWithin_eventually_congr_set' Filter.EventuallyEq.filter_mono inf_le_left
iteratedFDerivWithin_eventually_congr_set' 📖	mathematical	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Compl.compl Set Set.instCompl Set.instSingletonSet	Filter.EventuallyEq 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 nhds iteratedFDerivWithin	—	Filter.EventuallyEq.refl Filter.Eventually.mono eventually_nhds_nhdsWithin RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self RingHomIsometric.ids ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul Filter.EventuallyEq.fderivWithin_eq_of_nhds fderivWithin_congr_set' T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
iteratedFDerivWithin_insert 📖	mathematical	—	iteratedFDerivWithin Set Set.instInsert	—	iteratedFDerivWithin_congr_set' Filter.Eventually.set_eq Filter.Eventually.mono eventually_mem_nhdsWithin
iteratedFDerivWithin_inter 📖	mathematical	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	iteratedFDerivWithin Set Set.instInter	—	iteratedFDerivWithin_inter' mem_nhdsWithin_of_mem_nhds
iteratedFDerivWithin_inter' 📖	mathematical	Set Filter Filter.instMembership nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	iteratedFDerivWithin Set Set.instInter	—	iteratedFDerivWithin_congr_set nhdsWithin_eq_iff_eventuallyEq nhdsWithin_inter_of_mem'
iteratedFDerivWithin_inter_open 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set Set.instMembership	iteratedFDerivWithin Set Set.instInter	—	iteratedFDerivWithin_inter IsOpen.mem_nhds
iteratedFDerivWithin_of_isOpen 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	Set.EqOn 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 iteratedFDerivWithin iteratedFDeriv	—	ContinuousMultilinearMap.ext SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self RingHomInvPair.ids RingHomIsometric.ids ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul iteratedFDeriv_succ_eq_comp_left iteratedFDerivWithin_succ_eq_comp_left fderivWithin_of_isOpen Filter.EventuallyEq.fderiv_eq Filter.mp_mem IsOpen.mem_nhds Filter.univ_mem'
iteratedFDerivWithin_one_apply 📖	mathematical	UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	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 iteratedFDerivWithin ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.funLike fderivWithin	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self RingHomCompTriple.ids RingHomInvPair.ids LinearIsometryEquiv.comp_fderivWithin
iteratedFDerivWithin_succ_apply_left 📖	mathematical	—	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 iteratedFDerivWithin ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousMultilinearMap.instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing ContinuousMultilinearMap.instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.funLike fderivWithin Fin.tail	—	—
iteratedFDerivWithin_succ_apply_right 📖	mathematical	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instMembership	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 iteratedFDerivWithin ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.funLike ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing fderivWithin Fin.init	—	RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomInvPair.ids ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul iteratedFDerivWithin_succ_eq_comp_left iteratedFDerivWithin_zero_eq_comp iteratedFDerivWithin_zero_apply RingHomCompTriple.ids LinearIsometryEquiv.comp_fderivWithin ContinuousLinearMap.continuousConstSMul ContinuousLinearMap.smulCommClass ContinuousMultilinearMap.ext ContinuousLinearMap.topologicalAddGroup SeminormedAddCommGroup.to_isUniformAddGroup fderivWithin_congr iteratedFDerivWithin_succ_apply_left Fin.tail_init_eq_init_tail
iteratedFDerivWithin_succ_eq_comp_left 📖	mathematical	—	iteratedFDerivWithin 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 ContinuousMultilinearMap NormedSpace.toModule ContinuousMultilinearMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousMultilinearMap.instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing DFunLike.coe LinearIsometryEquiv RingHomInvPair.ids ContinuousLinearMap.toSeminormedAddCommGroup ContinuousMultilinearMap.seminormedAddCommGroup Fin.fintype ContinuousMultilinearMap.normedSpace RingHomIsometric.ids ContinuousLinearMap.module ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul SeminormedAddCommGroup.toAddCommGroup EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm continuousMultilinearCurryLeftEquiv fderivWithin ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing	—	—
iteratedFDerivWithin_succ_eq_comp_right 📖	mathematical	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instMembership	iteratedFDerivWithin ContinuousMultilinearMap 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 ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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 ContinuousLinearMap.topologicalSpace DFunLike.coe LinearIsometryEquiv RingHomInvPair.ids ContinuousMultilinearMap.seminormedAddCommGroup' ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids ContinuousLinearMap.toNormedSpace Fin.fintype ContinuousMultilinearMap.instModule SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap.continuousConstSMul ContinuousLinearMap.smulCommClass EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm continuousMultilinearCurryRightEquiv' ContinuousLinearMap.toNormedAddCommGroup fderivWithin	—	ContinuousMultilinearMap.ext IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomInvPair.ids RingHomIsometric.ids ContinuousLinearMap.continuousConstSMul ContinuousLinearMap.smulCommClass iteratedFDerivWithin_succ_apply_right
iteratedFDerivWithin_two_apply 📖	mathematical	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instMembership	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 iteratedFDerivWithin ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.funLike ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul fderivWithin	—	SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomIsometric.ids iteratedFDerivWithin_succ_apply_right
iteratedFDerivWithin_two_apply' 📖	mathematical	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instMembership	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 iteratedFDerivWithin Matrix.vecCons Matrix.vecEmpty ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.funLike ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul fderivWithin	—	iteratedFDerivWithin_two_apply
iteratedFDerivWithin_univ 📖	mathematical	—	iteratedFDerivWithin Set.univ iteratedFDeriv	—	ContinuousMultilinearMap.ext SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self iteratedFDeriv_succ_apply_left iteratedFDerivWithin_succ_apply_left fderivWithin_univ
iteratedFDerivWithin_zero_apply 📖	mathematical	—	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 iteratedFDerivWithin	—	—
iteratedFDerivWithin_zero_eq 📖	mathematical	—	iteratedFDerivWithin iteratedFDeriv	—	—
iteratedFDerivWithin_zero_eq_comp 📖	mathematical	—	iteratedFDerivWithin 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 DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype ContinuousMultilinearMap.instModule SeminormedAddCommGroup.toAddCommGroup 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 smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm continuousMultilinearCurryFin0	—	—
iteratedFDeriv_comp_add_left 📖	mathematical	—	iteratedFDeriv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	iteratedFDeriv_comp_add_left'
iteratedFDeriv_comp_add_left' 📖	mathematical	—	iteratedFDeriv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Set.vadd_set_univ iteratedFDerivWithin_comp_add_left'
iteratedFDeriv_comp_add_right 📖	mathematical	—	iteratedFDeriv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	iteratedFDeriv_comp_add_right'
iteratedFDeriv_comp_add_right' 📖	mathematical	—	iteratedFDeriv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	add_comm iteratedFDeriv_comp_add_left'
iteratedFDeriv_comp_sub 📖	mathematical	—	iteratedFDeriv SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	iteratedFDeriv_comp_sub'
iteratedFDeriv_comp_sub' 📖	mathematical	—	iteratedFDeriv SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	sub_eq_add_neg iteratedFDeriv_comp_add_right'
iteratedFDeriv_one_apply 📖	mathematical	—	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 iteratedFDeriv ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.funLike fderiv	—	RingHomIsometric.ids smulCommClass_self iteratedFDeriv_succ_apply_right iteratedFDeriv_zero_apply
iteratedFDeriv_succ_apply_left 📖	mathematical	—	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 iteratedFDeriv ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousMultilinearMap.instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing ContinuousMultilinearMap.instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.funLike fderiv Fin.tail	—	—
iteratedFDeriv_succ_apply_right 📖	mathematical	—	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 iteratedFDeriv ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.funLike ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing fderiv Fin.init	—	RingHomIsometric.ids smulCommClass_self iteratedFDerivWithin_univ fderivWithin_univ iteratedFDerivWithin_succ_apply_right uniqueDiffOn_univ NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Set.mem_univ
iteratedFDeriv_succ_eq_comp_left 📖	mathematical	—	iteratedFDeriv 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 ContinuousMultilinearMap NormedSpace.toModule ContinuousMultilinearMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousMultilinearMap.instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing DFunLike.coe LinearIsometryEquiv RingHomInvPair.ids ContinuousLinearMap.toSeminormedAddCommGroup ContinuousMultilinearMap.seminormedAddCommGroup Fin.fintype ContinuousMultilinearMap.normedSpace RingHomIsometric.ids ContinuousLinearMap.module ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul SeminormedAddCommGroup.toAddCommGroup EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm continuousMultilinearCurryLeftEquiv fderiv ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing	—	—
iteratedFDeriv_succ_eq_comp_right 📖	mathematical	—	iteratedFDeriv ContinuousMultilinearMap 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 ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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 ContinuousLinearMap.topologicalSpace DFunLike.coe LinearIsometryEquiv RingHomInvPair.ids ContinuousMultilinearMap.seminormedAddCommGroup' ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids ContinuousLinearMap.toNormedSpace Fin.fintype ContinuousMultilinearMap.instModule SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap.continuousConstSMul ContinuousLinearMap.smulCommClass EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm continuousMultilinearCurryRightEquiv' ContinuousLinearMap.toNormedAddCommGroup fderiv	—	ContinuousMultilinearMap.ext IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomInvPair.ids RingHomIsometric.ids ContinuousLinearMap.continuousConstSMul ContinuousLinearMap.smulCommClass iteratedFDeriv_succ_apply_right continuousMultilinearCurryRightEquiv_symm_apply'
iteratedFDeriv_two_apply 📖	mathematical	—	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 iteratedFDeriv ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.funLike ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul fderiv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomIsometric.ids iteratedFDeriv_succ_apply_right
iteratedFDeriv_zero_apply 📖	mathematical	—	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 iteratedFDeriv	—	—
iteratedFDeriv_zero_eq_comp 📖	mathematical	—	iteratedFDeriv 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 DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype ContinuousMultilinearMap.instModule SeminormedAddCommGroup.toAddCommGroup 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 smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm continuousMultilinearCurryFin0	—	—
norm_fderivWithin_iteratedFDerivWithin 📖	mathematical	—	Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousMultilinearMap ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing ContinuousMultilinearMap.instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.hasOpNorm ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype ContinuousMultilinearMap.normedSpace' fderivWithin iteratedFDerivWithin ContinuousMultilinearMap.hasOpNorm'	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self IsTopologicalAddGroup.toContinuousAdd RingHomInvPair.ids RingHomIsometric.ids ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul iteratedFDerivWithin_succ_eq_comp_left LinearIsometryEquiv.norm_map
norm_fderiv_iteratedFDeriv 📖	mathematical	—	Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousMultilinearMap ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing ContinuousMultilinearMap.instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.hasOpNorm ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype ContinuousMultilinearMap.normedSpace' fderiv iteratedFDeriv ContinuousMultilinearMap.hasOpNorm'	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self IsTopologicalAddGroup.toContinuousAdd RingHomInvPair.ids RingHomIsometric.ids ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul iteratedFDeriv_succ_eq_comp_left LinearIsometryEquiv.norm_map
norm_iteratedFDerivWithin_fderivWithin 📖	mathematical	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instMembership	Norm.norm ContinuousMultilinearMap ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing ContinuousMultilinearMap.hasOpNorm' ContinuousLinearMap.toSeminormedAddCommGroup Fin.fintype iteratedFDerivWithin fderivWithin	—	RingHomIsometric.ids smulCommClass_self IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomInvPair.ids ContinuousLinearMap.continuousConstSMul ContinuousLinearMap.smulCommClass iteratedFDerivWithin_succ_eq_comp_right LinearIsometryEquiv.norm_map
norm_iteratedFDerivWithin_one 📖	mathematical	UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Norm.norm 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.hasOpNorm' Fin.fintype iteratedFDerivWithin ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.hasOpNorm fderivWithin	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self RingHomCompTriple.ids RingHomInvPair.ids LinearIsometryEquiv.comp_fderivWithin LinearIsometry.norm_toContinuousLinearMap_comp RingHomIsometric.ids
norm_iteratedFDerivWithin_zero 📖	mathematical	—	Norm.norm 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.hasOpNorm' Fin.fintype iteratedFDerivWithin NormedAddCommGroup.toNorm	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self iteratedFDerivWithin_zero_eq_comp LinearIsometryEquiv.norm_map
norm_iteratedFDeriv_fderiv 📖	mathematical	—	Norm.norm ContinuousMultilinearMap ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing ContinuousMultilinearMap.hasOpNorm' ContinuousLinearMap.toSeminormedAddCommGroup Fin.fintype iteratedFDeriv fderiv	—	RingHomIsometric.ids smulCommClass_self IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomInvPair.ids ContinuousLinearMap.continuousConstSMul ContinuousLinearMap.smulCommClass iteratedFDeriv_succ_eq_comp_right LinearIsometryEquiv.norm_map
norm_iteratedFDeriv_one 📖	mathematical	—	Norm.norm 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.hasOpNorm' Fin.fintype iteratedFDeriv ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.hasOpNorm fderiv	—	iteratedFDerivWithin_univ fderivWithin_univ norm_iteratedFDerivWithin_one uniqueDiffWithinAt_univ NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul
norm_iteratedFDeriv_zero 📖	mathematical	—	Norm.norm 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.hasOpNorm' Fin.fintype iteratedFDeriv NormedAddCommGroup.toNorm	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self iteratedFDeriv_zero_eq_comp LinearIsometryEquiv.norm_map
support_iteratedFDeriv_subset 📖	mathematical	—	Set Set.instHasSubset Function.support ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.instZero iteratedFDeriv tsupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	HasSubset.Subset.trans Set.instIsTransSubset subset_closure tsupport_iteratedFDeriv_subset
tsupport_iteratedFDeriv_subset 📖	mathematical	—	Set Set.instHasSubset tsupport ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.instZero iteratedFDeriv NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self iteratedFDeriv_zero_eq_comp closure_minimal HasSubset.Subset.trans Set.instIsTransSubset Function.support_comp_subset map_zero AddMonoidHomClass.toZeroHomClass IsTopologicalAddGroup.toContinuousAdd DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearIsometryClass.toSemilinearMapClass SemilinearIsometryEquivClass.toSemilinearIsometryClass LinearIsometryEquiv.instSemilinearIsometryEquivClass subset_closure isClosed_closure RingHomIsometric.ids ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul iteratedFDeriv_succ_eq_comp_left ContinuousMultilinearMap.instIsTopologicalAddGroup support_fderiv_subset

---

← Back to Index