Defs

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

Statistics

Metric	Count
Definitions ContDiffAt, ContDiffOn, ContDiffWithinAt	3
Theorems contDiffAt, contDiff, contDiffOn, contDiffOn_of_completeSpace, contDiff, contDiffOn, contDiffOn_of_completeSpace, contDiffWithinAt, analyticOnNhd, contDiffAt, contDiffOn, contDiffWithinAt, continuous, continuous_fderiv, continuous_fderiv_apply, continuous_iteratedFDeriv, continuous_iteratedFDeriv', continuous_zero, differentiable, differentiable_iteratedFDeriv, differentiable_one, ftaylorSeries, of_le, of_succ, one_of_succ, analyticAt, congr_of_eventuallyEq, contDiffOn, contDiffWithinAt, continuousAt, differentiableAt, differentiableAt_iteratedFDeriv, differentiableAt_one, eventually, of_le, analyticOn, congr_mono, contDiffAt, contDiffWithinAt, continuousOn, continuousOn_fderivWithin, continuousOn_fderiv_of_isOpen, continuousOn_iteratedFDerivWithin, continuousOn_zero, differentiableOn, differentiableOn_iteratedFDerivWithin, differentiableOn_one, fderivWithin, fderiv_of_isOpen, ftaylorSeriesWithin, mono, of_le, of_succ, one_of_succ, analyticOn, analyticWithinAt, congr_mono, congr_of_eventuallyEq, congr_of_eventuallyEq_insert, congr_of_eventuallyEq_of_mem, congr_of_insert, congr_of_mem, congr_set, contDiffAt, contDiffOn, contDiffOn', continuousWithinAt, differentiableWithinAt, differentiableWithinAt', differentiableWithinAt_iteratedFDerivWithin, eventually, eventually_hasFTaylorSeriesUpToOn, insert, insert', mono, mono_of_mem_nhdsWithin, of_insert, of_le, congr_contDiffWithinAt, congr_contDiffWithinAt_of_insert, congr_contDiffWithinAt_of_mem, contDiff, analyticOn, contDiffOn, contDiffOn_iff, contDiffAt_infty, contDiffAt_one_iff, contDiffAt_succ_iff_hasFDerivAt, contDiffAt_zero, contDiffOn_all_iff_nat, contDiffOn_congr, contDiffOn_empty, contDiffOn_iff_continuousOn_differentiableOn, contDiffOn_iff_forall_nat_le, contDiffOn_infty, contDiffOn_infty_iff_fderivWithin, contDiffOn_infty_iff_fderiv_of_isOpen, contDiffOn_nat_iff_continuousOn_differentiableOn, contDiffOn_of_analyticOn_iteratedFDerivWithin, contDiffOn_of_analyticOn_of_fderivWithin, contDiffOn_of_continuousOn_differentiableOn, contDiffOn_of_differentiableOn, contDiffOn_of_locally_contDiffOn, contDiffOn_omega_iff_analyticOn, contDiffOn_succ_iff_fderivWithin, contDiffOn_succ_iff_fderiv_of_isOpen, contDiffOn_succ_iff_hasFDerivWithinAt, contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn, contDiffOn_succ_of_fderivWithin, contDiffOn_univ, contDiffOn_zero, contDiffWithinAt_compl_self, contDiffWithinAt_congr, contDiffWithinAt_congr_of_insert, contDiffWithinAt_congr_of_mem, contDiffWithinAt_congr_set, contDiffWithinAt_diff_singleton, contDiffWithinAt_iff_contDiffAt, contDiffWithinAt_iff_contDiffOn_nhds, contDiffWithinAt_iff_forall_nat_le, contDiffWithinAt_iff_of_ne_infty, contDiffWithinAt_infty, contDiffWithinAt_insert, contDiffWithinAt_insert_self, contDiffWithinAt_inter, contDiffWithinAt_inter', contDiffWithinAt_nat, contDiffWithinAt_omega_iff_analyticWithinAt, contDiffWithinAt_succ_iff_hasFDerivWithinAt, contDiffWithinAt_succ_iff_hasFDerivWithinAt', contDiffWithinAt_univ, contDiffWithinAt_zero, contDiff_all_iff_nat, contDiff_iff_contDiffAt, contDiff_iff_continuous_differentiable, contDiff_iff_forall_nat_le, contDiff_iff_ftaylorSeries, contDiff_infty, contDiff_infty_iff_fderiv, contDiff_nat_iff_continuous_differentiable, contDiff_of_differentiable_iteratedFDeriv, contDiff_omega_iff_analyticOnNhd, contDiff_one_iff_fderiv, contDiff_one_iff_hasFDerivAt, contDiff_succ_iff_fderiv, contDiff_succ_iff_hasFDerivAt, contDiff_zero, iteratedFDerivWithin_eq_iteratedFDeriv, iteratedFDerivWithin_subset	149
Total	152

AnalyticAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffAt 📖	mathematical	AnalyticAt	ContDiffAt	—	contDiffWithinAt_univ AnalyticWithinAt.contDiffWithinAt analyticWithinAt_univ

AnalyticOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiff 📖	mathematical	AnalyticOn Set.univ	ContDiff	—	contDiffOn_univ contDiffOn uniqueDiffOn_univ NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul
contDiffOn 📖	mathematical	AnalyticOn UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	ContDiffOn	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self exists_hasFTaylorSeriesUpToOn Set.insert_eq_of_mem self_mem_nhdsWithin ContDiffOn.of_le le_top
contDiffOn_of_completeSpace 📖	mathematical	AnalyticOn	ContDiffOn	—	AnalyticWithinAt.contDiffWithinAt

AnalyticOnNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiff 📖	mathematical	AnalyticOnNhd Set.univ	ContDiff	—	AnalyticOn.contDiff analyticOn
contDiffOn 📖	mathematical	AnalyticOnNhd UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	ContDiffOn	—	AnalyticOn.contDiffOn analyticOn
contDiffOn_of_completeSpace 📖	mathematical	AnalyticOnNhd	ContDiffOn	—	AnalyticOn.contDiffOn_of_completeSpace analyticOn

AnalyticWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffWithinAt 📖	mathematical	AnalyticWithinAt	ContDiffWithinAt	—	ContDiffWithinAt.of_le contDiffWithinAt_omega_iff_analyticWithinAt le_top

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticOnNhd 📖	mathematical	ContDiff Top.top WithTop ENat WithTop.top	AnalyticOnNhd	—	ContDiffOn.analyticOn contDiffOn_univ AnalyticOnNhd.mono analyticOn_univ Set.subset_univ
contDiffAt 📖	mathematical	ContDiff	ContDiffAt	—	contDiff_iff_contDiffAt
contDiffOn 📖	mathematical	ContDiff	ContDiffOn	—	ContDiffOn.mono contDiffOn_univ Set.subset_univ
contDiffWithinAt 📖	mathematical	ContDiff	ContDiffWithinAt	—	ContDiffAt.contDiffWithinAt contDiffAt
continuous 📖	mathematical	ContDiff	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	contDiff_zero of_le bot_le
continuous_fderiv 📖	mathematical	ContDiff	Continuous 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 ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup fderiv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup contDiff_one_iff_fderiv of_le ENat.one_le_iff_ne_zero_withTop
continuous_fderiv_apply 📖	mathematical	ContDiff	Continuous instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousLinearMap.funLike fderiv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedBilinearMap.continuous RingHomIsometric.ids smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul isBoundedBilinearMap_apply Continuous.prodMk Continuous.comp continuous_fderiv continuous_fst continuous_snd
continuous_iteratedFDeriv 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat WithTop.natCast ENat.instNatCast ContDiff	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 iteratedFDeriv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self contDiff_iff_continuous_differentiable of_le le_rfl
continuous_iteratedFDeriv' 📖	mathematical	ContDiff WithTop ENat 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 iteratedFDeriv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self contDiff_iff_continuous_differentiable le_rfl
continuous_zero 📖	mathematical	ContDiff WithTop ENat WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	contDiff_zero of_le bot_le
differentiable 📖	mathematical	ContDiff	Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	differentiableOn_univ ContDiffOn.differentiableOn contDiffOn_univ
differentiable_iteratedFDeriv 📖	mathematical	WithTop ENat Preorder.toLT WithTop.instPreorder instPreorderENat WithTop.natCast ENat.instNatCast ContDiff	Differentiable 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	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self contDiff_iff_continuous_differentiable of_le ENat.add_one_natCast_le_withTop_of_lt IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid lt_add_one Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid Nat.instIsOrderedAddMonoid
differentiable_one 📖	mathematical	ContDiff WithTop ENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	differentiableOn_univ ContDiffOn.differentiableOn contDiffOn_univ one_ne_zero NeZero.charZero_one WithTop.charZero
ftaylorSeries 📖	mathematical	ContDiff	HasFTaylorSeriesUpTo ftaylorSeries	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContDiffOn.ftaylorSeriesWithin uniqueDiffOn_univ NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul
of_le 📖	mathematical	ContDiff WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat	ContDiff	—	contDiffOn_univ ContDiffOn.of_le
of_succ 📖	mathematical	ContDiff WithTop ENat WithTop.add instAddENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	ContDiff	—	of_le le_self_add WithTop.canonicallyOrderedAdd
one_of_succ 📖	mathematical	ContDiff WithTop ENat WithTop.add instAddENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	ContDiff WithTop ENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	of_le le_add_self WithTop.canonicallyOrderedAdd

ContDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticAt 📖	mathematical	ContDiffAt Top.top WithTop ENat WithTop.top	AnalyticAt	—	analyticWithinAt_univ ContDiffWithinAt.analyticWithinAt contDiffWithinAt_univ
congr_of_eventuallyEq 📖	mathematical	ContDiffAt Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	ContDiffAt	—	ContDiffWithinAt.congr_of_eventuallyEq_of_mem nhdsWithin_univ Set.mem_univ
contDiffOn 📖	mathematical	ContDiffAt WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat Top.top WithTop.top	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ContDiffOn	—	Set.insert_eq_of_mem nhdsWithin_univ ContDiffWithinAt.contDiffOn
contDiffWithinAt 📖	mathematical	ContDiffAt	ContDiffWithinAt	—	ContDiffWithinAt.mono Set.subset_univ
continuousAt 📖	mathematical	ContDiffAt	ContinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	ContDiffWithinAt.continuousWithinAt
differentiableAt 📖	mathematical	ContDiffAt	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	ContDiffWithinAt.differentiableWithinAt
differentiableAt_iteratedFDeriv 📖	mathematical	ContDiffAt WithTop ENat Preorder.toLT WithTop.instPreorder instPreorderENat WithTop.natCast ENat.instNatCast	DifferentiableAt 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	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self differentiableWithinAt_univ iteratedFDerivWithin_univ ContDiffWithinAt.differentiableWithinAt_iteratedFDerivWithin Set.insert_eq_of_mem NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul
differentiableAt_one 📖	mathematical	ContDiffAt WithTop ENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	NeZero.charZero_one WithTop.charZero ContDiffWithinAt.differentiableWithinAt
eventually 📖	mathematical	ContDiffAt	Filter.Eventually ContDiffAt nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	Set.insert_eq_of_mem nhdsWithin_univ ContDiffWithinAt.eventually
of_le 📖	mathematical	ContDiffAt WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat	ContDiffAt	—	ContDiffWithinAt.of_le

ContDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticOn 📖	mathematical	ContDiffOn Top.top WithTop ENat WithTop.top	AnalyticOn	—	ContDiffWithinAt.analyticWithinAt
congr_mono 📖	mathematical	ContDiffOn Set Set.instHasSubset	ContDiffOn	—	congr mono
contDiffAt 📖	mathematical	ContDiffOn Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	ContDiffAt	—	ContDiffWithinAt.contDiffAt mem_of_mem_nhds
contDiffWithinAt 📖	mathematical	ContDiffOn Set Set.instMembership	ContDiffWithinAt	—	—
continuousOn 📖	mathematical	ContDiffOn	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	ContDiffWithinAt.continuousWithinAt
continuousOn_fderivWithin 📖	mathematical	ContDiffOn UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	ContinuousOn 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 ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup fderivWithin	—	continuousOn RingHomIsometric.ids smulCommClass_self contDiffOn_succ_iff_fderivWithin of_le
continuousOn_fderiv_of_isOpen 📖	mathematical	ContDiffOn IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	ContinuousOn 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 ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup fderiv	—	continuousOn RingHomIsometric.ids smulCommClass_self contDiffOn_succ_iff_fderiv_of_isOpen of_le
continuousOn_iteratedFDerivWithin 📖	mathematical	ContDiffOn 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	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 iteratedFDerivWithin	—	HasFTaylorSeriesUpToOn.cont ftaylorSeriesWithin of_le le_rfl
continuousOn_zero 📖	mathematical	ContDiffOn WithTop ENat WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	ContDiffWithinAt.continuousWithinAt
differentiableOn 📖	mathematical	ContDiffOn	DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	ContDiffWithinAt.differentiableWithinAt
differentiableOn_iteratedFDerivWithin 📖	mathematical	ContDiffOn WithTop ENat Preorder.toLT 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	DifferentiableOn 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	—	ENat.add_one_natCast_le_withTop_of_lt HasFDerivWithinAt.differentiableWithinAt SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self HasFTaylorSeriesUpToOn.fderivWithin ftaylorSeriesWithin 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
differentiableOn_one 📖	mathematical	ContDiffOn WithTop ENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	ContDiffWithinAt.differentiableWithinAt one_ne_zero NeZero.charZero_one WithTop.charZero
fderivWithin 📖	mathematical	ContDiffOn UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat WithTop.add instAddENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	ContDiffOn 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 ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing fderivWithin	—	RingHomIsometric.ids smulCommClass_self contDiffOn_succ_iff_fderivWithin of_le
fderiv_of_isOpen 📖	mathematical	ContDiffOn IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat WithTop.add instAddENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	ContDiffOn 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 ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing fderiv	—	congr RingHomIsometric.ids smulCommClass_self fderivWithin IsOpen.uniqueDiffOn NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup fderivWithin_of_isOpen
ftaylorSeriesWithin 📖	mathematical	ContDiffOn UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	HasFTaylorSeriesUpToOn ftaylorSeriesWithin	—	ENat.add_one_natCast_le_withTop_of_lt SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self ContDiffWithinAt.of_le le_rfl mem_nhdsWithin Set.insert_eq_of_mem iteratedFDerivWithin_inter_open HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn HasFTaylorSeriesUpToOn.mono Set.inter_comm UniqueDiffOn.inter hasFDerivWithinAt_inter IsOpen.mem_nhds WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass WithTop.charZero HasFDerivWithinAt.congr HasFTaylorSeriesUpToOn.fderivWithin lt_add_one Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid Nat.instIsOrderedAddMonoid continuousOn_of_locally_continuousOn ContinuousOn.congr HasFTaylorSeriesUpToOn.cont
mono 📖	mathematical	ContDiffOn Set Set.instHasSubset	ContDiffOn	—	ContDiffWithinAt.mono
of_le 📖	mathematical	ContDiffOn WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat	ContDiffOn	—	ContDiffWithinAt.of_le
of_succ 📖	mathematical	ContDiffOn WithTop ENat WithTop.add instAddENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	ContDiffOn	—	of_le le_self_add WithTop.canonicallyOrderedAdd
one_of_succ 📖	mathematical	ContDiffOn WithTop ENat WithTop.add instAddENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	ContDiffOn WithTop ENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	of_le le_add_self WithTop.canonicallyOrderedAdd

ContDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticOn 📖	mathematical	ContDiffWithinAt Top.top WithTop ENat WithTop.top	Set Filter Filter.instMembership nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.instInsert AnalyticOn	—	HasFTaylorSeriesUpToOn.analyticOn
analyticWithinAt 📖	mathematical	ContDiffWithinAt Top.top WithTop ENat WithTop.top	AnalyticWithinAt	—	analyticOn mem_of_mem_nhdsWithin AnalyticWithinAt.mono_of_mem_nhdsWithin nhdsWithin_mono Set.subset_insert
congr_mono 📖	mathematical	ContDiffWithinAt Set.EqOn Set Set.instHasSubset	ContDiffWithinAt	—	congr mono
congr_of_eventuallyEq 📖	mathematical	ContDiffWithinAt Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	ContDiffWithinAt	—	Filter.inter_mem mem_nhdsWithin_insert HasFTaylorSeriesUpToOn.congr HasFTaylorSeriesUpToOn.mono Set.sep_subset AnalyticOn.mono
congr_of_eventuallyEq_insert 📖	mathematical	ContDiffWithinAt Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set Set.instInsert	ContDiffWithinAt	—	congr_of_eventuallyEq nhdsWithin_mono Set.subset_insert mem_of_mem_nhdsWithin Set.mem_insert
congr_of_eventuallyEq_of_mem 📖	mathematical	ContDiffWithinAt Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set Set.instMembership	ContDiffWithinAt	—	congr_of_eventuallyEq Filter.Eventually.self_of_nhdsWithin
congr_of_insert 📖	mathematical	ContDiffWithinAt	ContDiffWithinAt	—	congr Set.mem_insert_of_mem Set.mem_insert
congr_of_mem 📖	mathematical	ContDiffWithinAt Set Set.instMembership	ContDiffWithinAt	—	congr
congr_set 📖	mathematical	ContDiffWithinAt Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	ContDiffWithinAt	—	mono_of_mem_nhdsWithin self_mem_nhdsWithin nhdsWithin_eq_iff_eventuallyEq
contDiffAt 📖	mathematical	ContDiffWithinAt Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	ContDiffAt	—	ContDiffAt.eq_1 contDiffWithinAt_inter Set.univ_inter
contDiffOn 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat Top.top WithTop.top ContDiffWithinAt	Set Filter Filter.instMembership nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.instInsert Set.instHasSubset ContDiffOn	—	contDiffOn' inter_mem_nhdsWithin IsOpen.mem_nhds Set.inter_subset_left
contDiffOn' 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat Top.top WithTop.top ContDiffWithinAt	Set IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.instMembership ContDiffOn Set.instInter Set.instInsert	—	eq_or_ne mem_nhdsWithin Set.insert_eq_of_mem HasFTaylorSeriesUpToOn.mono Set.inter_comm AnalyticOn.mono ContDiffOn.of_le le_top IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul contDiffWithinAt_nat of_le HasFTaylorSeriesUpToOn.contDiffOn
continuousWithinAt 📖	mathematical	ContDiffWithinAt	ContinuousWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	of_le zero_le WithTop.canonicallyOrderedAdd IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul CharP.cast_eq_zero CharP.ofCharZero WithTop.charZero ContinuousWithinAt.mono_of_mem_nhdsWithin ContinuousOn.continuousWithinAt HasFTaylorSeriesUpToOn.continuousOn mem_nhdsWithin_insert
differentiableWithinAt 📖	mathematical	ContDiffWithinAt	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	DifferentiableWithinAt.mono differentiableWithinAt' Set.subset_insert
differentiableWithinAt' 📖	mathematical	ContDiffWithinAt	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instInsert	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul contDiffWithinAt_nat of_le ENat.one_le_iff_ne_zero_withTop mem_nhdsWithin differentiableWithinAt_inter IsOpen.mem_nhds HasFTaylorSeriesUpToOn.differentiableOn HasFTaylorSeriesUpToOn.mono Set.inter_comm one_ne_zero NeZero.charZero_one WithTop.charZero Set.mem_insert
differentiableWithinAt_iteratedFDerivWithin 📖	mathematical	ContDiffWithinAt WithTop ENat Preorder.toLT 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.instInsert	DifferentiableWithinAt 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	—	instLawfulBCmpCompare_mathlib SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self contDiffOn' ENat.add_one_natCast_le_withTop_of_lt Nat.cast_add Nat.cast_one instIsEmptyFalse Set.inter_assoc nhdsWithin_inter_of_mem' mem_nhdsWithin_of_mem_nhds IsOpen.mem_nhds Set.diff_eq_compl_inter Set.insert_diff_of_mem iteratedFDerivWithin_eventually_congr_set' Filter.EventuallyEq.symm ContDiffOn.differentiableOn_iteratedFDerivWithin Nat.cast_lt WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass WithTop.charZero UniqueDiffOn.inter IsTopologicalAddGroup.toContinuousAdd Set.mem_insert DifferentiableWithinAt.congr_of_eventuallyEq differentiableWithinAt_congr_set' T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Filter.EventuallyEq.filter_mono inf_le_left Filter.Eventually.self_of_nhds
eventually 📖	mathematical	ContDiffWithinAt	Filter.Eventually ContDiffWithinAt nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set Set.instInsert	—	contDiffOn le_rfl instIsEmptyFalse Filter.Eventually.and eventually_eventually_nhdsWithin Filter.Eventually.mono mono_of_mem_nhdsWithin nhdsWithin_mono Set.subset_insert
eventually_hasFTaylorSeriesUpToOn 📖	mathematical	ContDiffWithinAt 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 WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat WithTop.natCast ENat.instNatCast	Filter.Eventually Set HasFTaylorSeriesUpToOn WithTop ENat WithTop.natCast ENat.instNatCast ftaylorSeriesWithin Filter.smallSets nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	contDiffOn' instIsEmptyFalse Filter.eventually_smallSets_subset inter_mem_nhdsWithin IsOpen.mem_nhds Filter.Eventually.mono HasFTaylorSeriesUpToOn.mono HasFTaylorSeriesUpToOn.congr_series ContDiffOn.ftaylorSeriesWithin Set.insert_eq_of_mem UniqueDiffOn.inter IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup iteratedFDerivWithin_inter_open
insert 📖	mathematical	ContDiffWithinAt	ContDiffWithinAt Set Set.instInsert	—	insert'
insert' 📖	mathematical	ContDiffWithinAt	ContDiffWithinAt Set Set.instInsert	—	contDiffWithinAt_insert
mono 📖	mathematical	ContDiffWithinAt Set Set.instHasSubset	ContDiffWithinAt	—	mono_of_mem_nhdsWithin Filter.mem_of_superset self_mem_nhdsWithin
mono_of_mem_nhdsWithin 📖	mathematical	ContDiffWithinAt Set Filter Filter.instMembership nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	ContDiffWithinAt	—	nhdsWithin_le_of_mem insert_mem_nhdsWithin_insert
of_insert 📖	mathematical	ContDiffWithinAt Set Set.instInsert	ContDiffWithinAt	—	contDiffWithinAt_insert
of_le 📖	mathematical	ContDiffWithinAt WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat	ContDiffWithinAt	—	HasFTaylorSeriesUpToOn.of_le le_top le_trans

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_contDiffWithinAt 📖	mathematical	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	ContDiffWithinAt	—	ContDiffWithinAt.congr_of_eventuallyEq symm
congr_contDiffWithinAt_of_insert 📖	mathematical	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set Set.instInsert	ContDiffWithinAt	—	ContDiffWithinAt.congr_of_eventuallyEq_insert symm
congr_contDiffWithinAt_of_mem 📖	mathematical	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set Set.instMembership	ContDiffWithinAt	—	ContDiffWithinAt.congr_of_eventuallyEq_of_mem symm

HasFTaylorSeriesUpTo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiff 📖	mathematical	HasFTaylorSeriesUpTo WithTop.some ENat	ContDiff WithTop.some ENat	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul

HasFTaylorSeriesUpToOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticOn 📖	mathematical	HasFTaylorSeriesUpToOn Top.top WithTop ENat WithTop.top AnalyticOn 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.normedAddCommGroup' Fin.fintype ContinuousMultilinearMap.normedSpace' smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing	AnalyticOn	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self RingHomInvPair.ids AnalyticOnNhd.comp_analyticOn LinearIsometryEquiv.analyticOnNhd Set.mapsTo_univ AnalyticOn.congr zero_eq
contDiffOn 📖	mathematical	HasFTaylorSeriesUpToOn WithTop.some ENat	ContDiffOn WithTop.some ENat	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Set.insert_eq_of_mem of_le

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffOn_iff 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	ContDiffOn ContDiffAt	—	contDiffWithinAt_iff_contDiffAt mem_nhds

(root)

Definitions

Name	Category	Theorems
ContDiffAt 📖	MathDef	149 math math: contDiffAt_snd, ContDiffAt.csin, contDiffAt_prod', Real.contDiffAt_arcosh, contDiffAt_norm_smul_iff, ContDiffAt.clm_apply, ContDiffAt.fderiv_right_succ, ContinuousMultilinearMap.contDiffAt, Real.contDiffAt_tan, OpenPartialHomeomorph.contDiffAt_symm_deriv, Real.contDiffAt_rpow_const_of_le, ContDiffAt.fderiv_succ, ContinuousLinearEquiv.contDiffAt_comp_iff, ContDiffAt.add, ContDiffAt.arsinh, contDiffWithinAt_univ, contDiffAt_pi', ContDiffAt.prodMap, contDiffWithinAt_compl_self, ContDiffAt.inv, ContDiffAt.fst'', contDiffAt_piLp_apply, Real.contDiffAt_sqrt, Real.deriv_sqrt_aux, ContDiffAt.sinh, contDiffAt_one_iff, ContDiffAt.div_const, ContDiffAt.restrict_scalars, ContDiffAt.pow, SmoothPartitionOfUnity.contDiffAt_finsum, Real.smoothTransition.contDiffAt, contDiffAt_map_inverse, ContDiffAt.fderiv_right, ContDiffAt.iteratedFDeriv_right, ContDiffAt.contDiffAt_norm_smul, ContDiffAt.inversion, Complex.contDiffAt_log, ContDiffAt.rpow, Real.contDiffAt_log, ContDiffAt.const_smul, ContDiffAt.cosh, contDiffAt_piLp', contDiffPointwiseHolderAt_iff, ContDiffAt.div, ContDiff.comp_contDiffAt, ContDiffAt.rpow_const_of_ne, contDiffAt_euclidean, ContDiffAt.derivWithin, Real.contDiffAt_arcsin_iff, ContDiffWithinAt.contDiffAt, ContDiffAt.arctan, OpenPartialHomeomorph.restrContDiff_target, contDiffAt_norm, OpenPartialHomeomorph.contDiffAt_symm, ContDiffAt.log, contDiffAt_inv, ContDiffAt.real_of_complex, SchwartzMap.contDiffAt, contDiffAt_prod, ContDiffAt.contDiffAt_implicitFunction, ContDiffAt.ccosh, OpenPartialHomeomorph.restrContDiff_source, contDiffAt_apply, ContDiffAt.norm_sq, ContDiffAt.snd', contDiffAt_succ_iff_hasFDerivAt, ContDiffAt.lieBracket_vectorField, ContDiffAt.rpow_const_of_le, Real.contDiffAt_rpow_const, contDiffWithinAt_iff_contDiffAt, ImplicitFunctionData.contDiffAt_implicitFunction, Complex.contDiffAt_tan, contDiffAt_inner, ContDiff.comp₂_contDiffAt, contDiffAt_of_subsingleton, ContinuousLinearMap.IsInvertible.contDiffAt_map_inverse, ContDiffBump.contDiffAt, ContDiffAt.ccos, contMDiffAt_vectorSpace_iff_contDiffAt, ContDiffAt.comp₂, ContDiffAt.smul_const, ContDiffAt.contDiffAt_norm_of_smul, ContDiffAt.prodMap', contDiffAt_infty, ContDiffAt.norm, IsContDiffImplicitAt.contDiffAt, ContDiffAt.continuousLinearMap_comp, contDiffAt_id, ContDiffAt.dist, IsOpen.contDiffOn_iff, ContDiffAt.clm_comp, ContDiffAt.fst', ContDiffAt.fderiv, ContDiffOn.contDiffAt, CPolynomialAt.contDiffAt, ContDiffPointwiseHolderAt.contDiffAt, ContMDiffAt.contDiffAt, Real.contDiffAt_rpow_const_of_ne, IsContDiffImplicitAt.contDiffAt_implicitFunction, contDiffAt_prod_iff, contDiffAt_zero, ContDiffAt.fun_smul, ContDiffAt.of_le, Real.contDiffAt_arccos, ContDiffAt.cexp, ContDiffAt.sum, UpperHalfPlane.contMDiffAt_iff, ContDiffAt.fst, ContDiffAt.csinh, AnalyticAt.contDiffAt, ContDiffAt.sin, ContDiffAt.comp, contDiffAt_ringInverse, contDiffAt_const, ContDiffAt.sub, ContDiffAt.abs, ContDiffAt.fun_comp, ContDiffAt.cos, ContDiffAt.inner, ContDiffAt.smul, contDiffAt_pi, contDiffAt_fun_id, ContDiffAt.to_localInverse, Real.deriv_arcsin_aux, contDiffAt_piLp, ContDiffPointwiseHolderAt.zero_exponent_iff, ContinuousLinearEquiv.comp_contDiffAt_iff, ContDiffAt.prodMk, exists_continuousLinearEquiv_fderiv_symm_eq, Real.contDiffAt_arcsin, contDiffAt_fst, contDiff_iff_contDiffAt, ContDiffAt.exp, ContDiffPointwiseHolderAt.zero_order_iff, ContDiffAt.smulRight, Real.contDiffAt_arccos_iff, ContDiffAt.snd'', ContDiffAt.congr_of_eventuallyEq, Real.contDiffAt_rpow_of_ne, ContDiffAt.eventually, InnerProductSpace.HarmonicContOnCl.contDiffAt, contMDiffAt_iff_contDiffAt, ContDiffAt.sqrt, ContDiffAt.contDiffBump, contDiffAt_abs, ContDiffAt.mul, ContDiffAt.snd, ContDiffAt.neg, ContDiff.contDiffAt
ContDiffOn 📖	MathDef	174 math math: ContDiffOn.congr, contDiffOn_nat_succ_iff_contDiffOn_one_iteratedDerivWithin, ContDiff.comp_contDiffOn, ContDiffOn.cos, contDiffOn_iUnion_iff_of_isOpen, ContDiffOn.rpow_const_of_le, Real.contDiffOn_log, ContDiff.fun_comp_contDiffOn, MeasureTheory.contDiffOn_convolution_left_with_param, contDiffOn_piLp', ContDiffOn.smul_const, ContDiffOn.lieBracketWithin_vectorField, ContDiffBumpBase.smooth, ContDiffOn.ccosh, ContDiffOn.cosh, ContDiffOn.add, ContDiffOn.clm_apply, ContDiffOn.inner, contDiffOn_iff_continuousOn_differentiableOn, ContDiffOn.sqrt, ContDiff.contDiffOn, CPolynomialOn.contDiffOn, ContDiffOn.comp, contDiffOn_nat_iff_continuousOn_differentiableOn_deriv, ContDiffOn.rpow, contDiffOn_of_continuousOn_differentiableOn, ContDiffOn.pow, contDiffOn_infty, contDiffOn_congr, contMDiffOn_iff_contDiffOn, AnalyticOnNhd.contDiffOn_of_completeSpace, ContDiffOn.sum, contDiffOn_one_iff_derivWithin, contDiffWithinAt_iff_contDiffOn_nhds, contDiffOn_prod', DifferentiableOn.contDiffOn, MeasureTheory.contDiffOn_convolution_right_with_param, ContDiffOn.const_smul, MeasureTheory.contDiffOn_convolution_left_with_param_comp, contDiffOn_succ_of_fderivWithin, ContDiffOn.mono, ContDiffOn.rpow_const_of_ne, contDiffOn_omega_iff_analyticOn, ContDiffOn.fderiv_of_isOpen, contDiffOn_fst, ODE.contDiffOn_nat_picard_Icc, contDiffOn_infty_iff_fderivWithin, contDiffOn_prod, contDiffOn_stereoToFun, contDiffOn_nat_iff_continuousOn_differentiableOn, ContDiffOn.csin, ContDiffOn.fst, OpenPartialHomeomorph.contDiffOn_extend_coord_change, contDiffOn_abs, ContDiffOn.ccos, ContDiffOn.inversion, ContDiffOn.restrict_scalars, contDiffOn_succ_iff_fderiv_of_isOpen, ContDiffOn.abs, contDiffOn_of_analyticOn_iteratedFDerivWithin, AnalyticOn.contDiffOn, HasFTaylorSeriesUpToOn.contDiffOn, ContDiffWithinAt.contDiffOn, AnalyticOnNhd.contDiffOn, contMDiffOn_iff_of_mem_maximalAtlas', ContDiffOn.derivWithin, contDiffOn_zero, ContDiffOn.congr_mono, contDiffOn_euclidean, ContDiffOn.log, OpenPartialHomeomorph.contDiffOn_univUnitBall_symm, InnerProductSpace.HarmonicOnNhd.contDiffOn, contDiffOn_of_differentiableOn, contMDiffOn_iff_of_subset_source', contDiffOn_succ_iff_hasFDerivWithinAt, contDiffOn_prod_iff, ContDiffOn.comp_inter, ContDiffOn.sin, contDiffOn_infty_iff_fderiv_of_isOpen, contDiffOn_all_iff_nat, contDiffOn_succ_iff_deriv_of_isOpen, ContDiffOn.clm_comp, contDiffOn_fun_id, ContDiffOn.div, contDiffOn_fderiv_coord_change, ContDiffOn.fun_div, contDiffOn_iff_forall_nat_le, MeasureTheory.contDiffOn_convolution_right_with_param_comp, OpenPartialHomeomorph.contDiffOn_restrContDiff_source, contDiffOn_piLp, contDiffOn_tsum_cexp, ContDiffOn.of_le, ODE.contDiffOn_comp, ContDiffWithinAt.contDiffOn', contDiffOn_inv, ContDiffOn.arctan, ODE.contDiffOn_enat_picard_Icc, contDiffOn_clm_apply, ODE.contDiffOn_enat_Icc_of_hasDerivWithinAt, ContDiffOn.continuousLinearMap_comp, contMDiffOn_iff, ContDiffOn.norm_sq, contMDiff_iff, contDiffOn_union_iff_of_isOpen, ContDiff.comp₂_contDiffOn, contDiffOn_ext_coord_change, Real.contDiffOn_arccos, ContDiffOn.fderivWithin, contDiffOn_piLp_apply, ContDiffAt.contDiffOn, contDiffOn_of_differentiableOn_deriv, ExistsContDiffBumpBase.y_smooth, ContDiffOn.one_of_succ, OpenPartialHomeomorph.contDiffOn_restrContDiff_target, IsOpen.contDiffOn_iff, ContDiffOn.iUnion_of_isOpen, ContDiffOn.union_of_isOpen, contMDiffOn_iff_of_mem_maximalAtlas, ContinuousLinearEquiv.comp_contDiffOn_iff, contDiffOn_of_analyticOn_of_fderivWithin, ContDiffOn.exp, ContDiffOn.smul, contDiffOn_of_continuousOn_differentiableOn_deriv, ContinuousLinearEquiv.contDiffOn_comp_iff, contDiffOn_succ_iff_fderivWithin, Real.contDiffOn_arcosh, contMDiffOn_iff_of_subset_source, ContDiffOn.of_succ, contDiffOn_snd, contDiffOn_succ_iff_fderiv_apply, ContMDiffOn.contDiffOn, contDiffOn_succ_iff_derivWithin, contDiffOn_pi, ContDiffOn.div_const, contDiffOn_of_subsingleton, OpenPartialHomeomorph.contDiffOn_univBall_symm, contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn, contDiffOn_empty, ContDiffOn.inv, ModelWithCorners.contDiffOn_extendCoordChange_symm, ContDiffOn.comp_continuousLinearMap, ContDiffOn.image_comp_contDiff, contDiffOn_succ_of_fderiv_apply, ContDiffOn.sub, ContDiffOn.prodMk, ContDiffOn.smulRight, contDiffOn_infty_iff_deriv_of_isOpen, ContDiffOn.deriv_of_isOpen, ContDiffOn.snd, contDiffOn_fderivWithin_apply, contDiffOn_univ, contMDiffOn_vectorSpace_iff_contDiffOn, ContDiffOn.norm, ContDiffOn.prodMap, ContDiffOn.fun_smul, ContDiffOn.mul, contDiffOn_infty_iff_derivWithin, ContDiffOn.cexp, contDiffOn_iff_continuousOn_differentiableOn_deriv, ContDiffOn.csinh, MeasureTheory.contDiffOn_convolution_right_with_param_aux, ContDiff.comp₃_contDiffOn, Real.contDiffOn_arcsin, ModelWithCorners.contDiffOn_extendCoordChange, contDiffOn_of_locally_contDiffOn, ContDiffOn.neg, contDiffOn_apply, ContDiffOn.dist, contDiffOn_const, ContDiffOn.sinh, ContDiffOn.arsinh, AnalyticOn.contDiffOn_of_completeSpace, contDiffOn_id, contDiffOn_pi'
ContDiffWithinAt 📖	MathDef	154 math math: ContDiff.comp_contDiffWithinAt, ContDiffWithinAt.sub, contDiffWithinAt_const, AnalyticWithinAt.contDiffWithinAt, contMDiffAt_iff_of_mem_source, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, ContDiffWithinAt.cexp, contDiffWithinAtProp_self, ContDiffWithinAt.add, contDiffWithinAt_fst, ContDiffWithinAt.clm_apply, ContDiffWithinAt.eventually, contMDiffWithinAt_iff_image, ContDiffWithinAt.fun_smul, ContDiffWithinAt.cosh, ContDiff.comp₂_contDiffWithinAt, ContDiffAt.comp₂_contDiffWithinAt, ContDiffWithinAt.of_le, ContDiffWithinAt.snd, contDiffWithinAt_univ, contDiffWithinAt_nat, contDiffWithinAt_compl_self, contDiffWithinAt_euclidean, ContDiffWithinAt.mono_of_mem_nhdsWithin, ContDiffWithinAt.hasFDerivWithinAt_nhds, Filter.EventuallyEq.congr_contDiffWithinAt_of_mem, contDiffWithinAt_inter', ContDiffWithinAt.comp_of_preimage_mem_nhdsWithin, ContDiffAt.comp_contDiffWithinAt_of_eq, ModelWithCorners.contDiffWithinAt_extendCoordChange, contDiffWithinAt_iff_contDiffOn_nhds, contDiffWithinAt_congr_of_mem, contDiffWithinAt_prod', ContDiffWithinAt.congr_of_eventuallyEq_of_mem, contDiffWithinAt_zero, ContDiffWithinAt.prodMap, ContDiffWithinAt.lieBracketWithin_vectorField, contDiffWithinAt_iff_of_ne_infty, ContDiffWithinAt.insert, ContDiffWithinAt.congr_of_eventuallyEq_insert, contDiffWithinAt_congr_set, ContDiffWithinAt.const_smul, ContDiffWithinAt.arctan, ContDiffWithinAt.congr_set, ContDiffWithinAt.fderivWithin'', ContDiffWithinAt.continuousLinearMap_comp, contDiffWithinAt_fun_id, ContDiffWithinAt.mul, ContDiffWithinAt.norm_sq, OpenPartialHomeomorph.contDiffWithinAt_extend_coord_change', contMDiffWithinAt_iff_of_mem_source', contDiffWithinAtProp_self_source, ContDiffWithinAt.comp, ContDiffWithinAt.smul, ContDiffWithinAt.ccos, ContDiffWithinAt.clm_comp, ContDiffWithinAt.inv, contMDiffAt_iff, ContDiffWithinAt.prodMap', contDiffWithinAt_omega_iff_analyticWithinAt, contDiffWithinAt_singleton, ContMDiffWithinAt.contDiffWithinAt, ContDiffWithinAt.sum, ContDiffWithinAt.comp_of_preimage_mem_nhdsWithin_of_eq, ContDiffWithinAt.sinh, ContDiffWithinAt.dist, ContDiffWithinAt.derivWithin, contDiffWithinAt_succ_iff_hasFDerivWithinAt', contMDiffWithinAt_iff, OpenPartialHomeomorph.contDiffWithinAt_extend_coord_change, ContDiffWithinAt.congr, ContDiffWithinAt.restrict_scalars, ContDiffWithinAt.comp_continuousLinearMap, ContDiffWithinAt.rpow, ContDiffWithinAt.fst, ContDiffWithinAt.ccosh, ContDiffWithinAt.fderivWithin', contDiffWithinAt_infty, ContDiffAt.comp_contDiffWithinAt, cot_pi_mul_contDiffWithinAt, contDiffWithinAtProp_self_target, contDiffWithinAt_iff_contDiffAt, contMDiffWithinAt_iff', ContDiffWithinAt.congr_mono, Filter.EventuallyEq.congr_contDiffWithinAt, ContinuousLinearEquiv.contDiffWithinAt_comp_iff, ContDiffWithinAt.csin, ContDiffWithinAt.cos, ModelWithCorners.contDiffWithinAt_extendCoordChange', ContDiffWithinAt.abs, contMDiffWithinAt_iff_contDiffWithinAt, ContDiff.contDiffWithinAt, contDiffWithinAt_congr_of_insert, contDiffWithinAt_of_subsingleton, ContDiffWithinAt.congr_of_insert, ContinuousLinearEquiv.comp_contDiffWithinAt_iff, contDiffWithinAt_iff_forall_nat_le, ContDiffWithinAt.exp, ContDiffWithinAt.comp_of_mem_nhdsWithin_image, ContDiffWithinAt.rpow_const_of_ne, Filter.EventuallyEq.congr_contDiffWithinAt_of_insert, ContDiffWithinAt.congr_of_eventuallyEq, ContDiffWithinAt.rpow_const_of_le, ContDiffWithinAt.div, ContDiffWithinAt.neg, contDiffWithinAt_insert, contDiffWithinAt_prod, contDiffWithinAt_pi, ContDiffWithinAt.iteratedFDerivWithin_right, contDiffWithinAt_piLp, ContDiffWithinAt.fderivWithin, ContDiffWithinAt.of_insert, contMDiffWithinAt_iff_of_mem_maximalAtlas, ContDiffWithinAt.inner, ContDiffWithinAt.smul_const, ContDiffWithinAt.smulRight, contDiffWithinAt_ext_coord_change, ContDiffWithinAt.pow, contDiffWithinAt_abs, contDiffWithinAt_id, ContDiffWithinAt.arsinh, ContDiffWithinAt.fderivWithin_right_apply, ContDiffWithinAt.inversion, ContDiffWithinAt.congr_of_mem, ContDiffWithinAt.insert', contDiffWithinAt_inter, ContDiffWithinAt.csinh, ContDiffWithinAt.contDiffBump, contDiffWithinAt_diff_singleton, ContDiffWithinAt.comp_inter, contDiffWithinAt_snd, contDiffWithinAt_prod_iff, ContDiffOn.contDiffWithinAt, ContDiffWithinAt.prodMk, contDiffWithinAt_congr, ContDiffWithinAt.sin, ContDiffWithinAt.comp_of_mem_nhdsWithin_image_of_eq, ContDiffWithinAt.norm, exists_continuousLinearEquiv_fderivWithin_symm_eq, contDiffWithinAt_piLp', ContDiffWithinAt.log, contDiffWithinAt_piLp_apply, ContDiffWithinAt.comp_inter_of_eq, ContDiffBump.contDiffWithinAt, contDiffWithinAt_insert_self, ContDiffWithinAt.div_const, ContDiffWithinAt.sqrt, ContDiffAt.contDiffWithinAt, contMDiffWithinAt_iff_of_mem_source, ContDiffWithinAt.fderivWithin_right, contDiffWithinAt_succ_iff_hasFDerivWithinAt, ContDiffWithinAt.comp_of_eq, ContDiffWithinAt.fderivWithin_apply, ContDiffWithinAt.mono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffAt_infty 📖	mathematical	—	ContDiffAt WithTop.some ENat Top.top instTopENat WithTop WithTop.natCast ENat.instNatCast	—	—
contDiffAt_one_iff 📖	mathematical	—	ContDiffAt WithTop ENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ContinuousOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.topologicalSpace NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup HasFDerivAt	—	SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomIsometric.ids smulCommClass_self Filter.exists_mem_and_iff Set.antitone_bforall antitone_continuousOn
contDiffAt_succ_iff_hasFDerivAt 📖	mathematical	—	ContDiffAt WithTop ENat WithTop.add instAddENat WithTop.natCast ENat.instNatCast WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup HasFDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring 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	—	RingHomIsometric.ids smulCommClass_self contDiffWithinAt_univ contDiffWithinAt_succ_iff_hasFDerivWithinAt Set.insert_eq_of_mem nhdsWithin_univ mem_nhds_iff Set.Subset.rfl HasFDerivWithinAt.hasFDerivAt ContDiffWithinAt.contDiffAt instIsEmptyFalse HasFDerivAt.hasFDerivWithinAt ContDiffAt.contDiffWithinAt
contDiffAt_zero 📖	mathematical	—	ContDiffAt WithTop ENat WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ContinuousOn	—	contDiffWithinAt_univ nhdsWithin_univ Set.univ_inter
contDiffOn_all_iff_nat 📖	mathematical	—	ContDiffOn WithTop.some ENat WithTop WithTop.natCast ENat.instNatCast	—	contDiffOn_infty
contDiffOn_congr 📖	mathematical	—	ContDiffOn	—	ContDiffOn.congr
contDiffOn_empty 📖	mathematical	—	ContDiffOn Set Set.instEmptyCollection	—	—
contDiffOn_iff_continuousOn_differentiableOn 📖	mathematical	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	ContDiffOn WithTop.some ENat 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 iteratedFDerivWithin DifferentiableOn 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	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self ContDiffOn.continuousOn_iteratedFDerivWithin ContDiffOn.differentiableOn_iteratedFDerivWithin contDiffOn_of_continuousOn_differentiableOn
contDiffOn_iff_forall_nat_le 📖	mathematical	—	ContDiffOn WithTop.some ENat WithTop WithTop.natCast ENat.instNatCast	—	ContDiffOn.of_le le_rfl
contDiffOn_infty 📖	mathematical	—	ContDiffOn WithTop.some ENat Top.top instTopENat WithTop WithTop.natCast ENat.instNatCast	—	contDiffOn_iff_forall_nat_le
contDiffOn_infty_iff_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	ContDiffOn WithTop.some ENat Top.top instTopENat DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing fderivWithin	—	RingHomIsometric.ids smulCommClass_self ENat.coe_top_add_one contDiffOn_succ_iff_fderivWithin instIsEmptyFalse
contDiffOn_infty_iff_fderiv_of_isOpen 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	ContDiffOn WithTop.some ENat Top.top instTopENat DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing fderiv	—	RingHomIsometric.ids smulCommClass_self ENat.coe_top_add_one contDiffOn_succ_iff_fderiv_of_isOpen instIsEmptyFalse
contDiffOn_nat_iff_continuousOn_differentiableOn 📖	mathematical	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	ContDiffOn WithTop ENat 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 iteratedFDerivWithin DifferentiableOn 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	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self WithTop.coe_natCast contDiffOn_iff_continuousOn_differentiableOn IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid
contDiffOn_of_analyticOn_iteratedFDerivWithin 📖	mathematical	AnalyticOn 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.normedAddCommGroup' Fin.fintype ContinuousMultilinearMap.normedSpace' smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing iteratedFDerivWithin	ContDiffOn	—	smulCommClass_self self_mem_nhdsWithin Set.insert_eq_of_mem DifferentiableWithinAt.hasFDerivWithinAt AnalyticOn.differentiableOn AnalyticOn.continuousOn ContDiffOn.of_le le_top
contDiffOn_of_analyticOn_of_fderivWithin 📖	mathematical	AnalyticOn ContDiffOn 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 ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Top.top WithTop ENat WithTop.top fderivWithin	ContDiffOn	—	RingHomIsometric.ids smulCommClass_self contDiffOn_succ_of_fderivWithin AnalyticOn.differentiableOn ContDiffOn.of_le le_top
contDiffOn_of_continuousOn_differentiableOn 📖	mathematical	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 iteratedFDerivWithin DifferentiableOn 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	ContDiffOn WithTop.some ENat	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self Set.insert_eq_of_mem self_mem_nhdsWithin IsTopologicalAddGroup.toContinuousAdd DifferentiableWithinAt.hasFDerivWithinAt lt_of_lt_of_le WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass WithTop.charZero le_trans
contDiffOn_of_differentiableOn 📖	mathematical	DifferentiableOn 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	ContDiffOn WithTop.some ENat	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self contDiffOn_of_continuousOn_differentiableOn DifferentiableOn.continuousOn IsTopologicalAddGroup.toContinuousAdd IsBoundedSMul.continuousSMul ContinuousMultilinearMap.instIsTopologicalAddGroup ContinuousMultilinearMap.instContinuousSMul le_of_lt
contDiffOn_of_locally_contDiffOn 📖	mathematical	Set IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.instMembership ContDiffOn Set.instInter	ContDiffOn	—	contDiffWithinAt_inter IsOpen.mem_nhds
contDiffOn_omega_iff_analyticOn 📖	mathematical	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	ContDiffOn Top.top WithTop ENat WithTop.top AnalyticOn	—	ContDiffOn.analyticOn AnalyticOn.contDiffOn
contDiffOn_succ_iff_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	ContDiffOn WithTop ENat WithTop.add instAddENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AnalyticOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing fderivWithin	—	RingHomIsometric.ids smulCommClass_self ContDiffOn.differentiableOn Unique.instSubsingleton WithTop.canonicallyOrderedAdd NeZero.charZero_one WithTop.charZero ContDiffOn.analyticOn contDiffWithinAt_succ_iff_hasFDerivWithinAt instLawfulBCmpCompare_mathlib ContDiffOn.of_le add_le_add_left WithTop.addRightMono covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid mem_nhdsWithin ContDiffWithinAt.mono Set.insert_eq_of_mem Set.inter_comm ContDiffWithinAt.congr_of_eventuallyEq_of_mem contDiffWithinAt_inter' mem_nhdsWithin_of_mem_nhds IsOpen.mem_nhds Set.Subset.refl Filter.eventuallyEq_of_mem HasFDerivWithinAt.fderivWithin IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace HasFDerivWithinAt.mono UniqueDiffOn.inter fderivWithin_inter AnalyticOn.contDiffOn AnalyticOn.fderivWithin contDiffWithinAt_infty le_top le_rfl contDiffOn_succ_of_fderivWithin
contDiffOn_succ_iff_fderiv_of_isOpen 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	ContDiffOn WithTop ENat WithTop.add instAddENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AnalyticOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing fderiv	—	RingHomIsometric.ids smulCommClass_self contDiffOn_succ_iff_fderivWithin IsOpen.uniqueDiffOn NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup contDiffOn_congr fderivWithin_of_isOpen
contDiffOn_succ_iff_hasFDerivWithinAt 📖	mathematical	—	ContDiffOn WithTop ENat WithTop.add instAddENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat Set Filter Filter.instMembership nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.instInsert AnalyticOn HasFDerivWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring 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	—	RingHomIsometric.ids smulCommClass_self contDiffWithinAt_succ_iff_hasFDerivWithinAt ContDiffWithinAt.contDiffOn le_rfl instIsEmptyFalse Set.insert_eq_of_mem mem_of_mem_nhdsWithin nhdsWithin_le_of_mem AnalyticOn.mono HasFDerivWithinAt.mono Set.mem_insert
contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn 📖	mathematical	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	ContDiffOn WithTop ENat WithTop.add instAddENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat AnalyticOn 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 HasFDerivWithinAt NormedAddCommGroup.toAddCommGroup	—	RingHomIsometric.ids smulCommClass_self contDiffOn_succ_iff_fderivWithin DifferentiableWithinAt.hasFDerivWithinAt HasFDerivWithinAt.differentiableWithinAt ContDiffWithinAt.congr_of_mem HasFDerivWithinAt.fderivWithin IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
contDiffOn_succ_of_fderivWithin 📖	mathematical	DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AnalyticOn ContDiffOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing fderivWithin	ContDiffOn WithTop ENat WithTop.add instAddENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	RingHomIsometric.ids smulCommClass_self eq_or_ne ENat.coe_top_add_one contDiffOn_infty ContDiffWithinAt.of_le contDiffWithinAt_succ_iff_hasFDerivWithinAt Set.insert_eq_of_mem self_mem_nhdsWithin instIsEmptyFalse DifferentiableWithinAt.hasFDerivWithinAt le_top le_self_add WithTop.canonicallyOrderedAdd
contDiffOn_univ 📖	mathematical	—	ContDiffOn Set.univ ContDiff	—	hasFTaylorSeriesUpToOn_univ_iff ContDiffOn.ftaylorSeriesWithin uniqueDiffOn_univ NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul analyticOn_univ AnalyticOn.iteratedFDerivWithin ContDiffOn.analyticOn Filter.univ_sets HasFTaylorSeriesUpToOn.of_le HasFTaylorSeriesUpTo.hasFTaylorSeriesUpToOn le_top AnalyticOnNhd.analyticOn
contDiffOn_zero 📖	mathematical	—	ContDiffOn WithTop ENat WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	ContDiffOn.continuousOn le_antisymm Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.addLeftMono WithTop.zeroLEOneClass WithTop.charZero bot_le self_mem_nhdsWithin hasFTaylorSeriesUpToOn_zero_iff Set.insert_eq_of_mem Matrix.zero_empty
contDiffWithinAt_compl_self 📖	mathematical	—	ContDiffWithinAt Compl.compl Set Set.instCompl Set.instSingletonSet ContDiffAt	—	Set.compl_eq_univ_diff contDiffWithinAt_diff_singleton contDiffWithinAt_univ
contDiffWithinAt_congr 📖	mathematical	—	ContDiffWithinAt	—	ContDiffWithinAt.congr
contDiffWithinAt_congr_of_insert 📖	mathematical	—	ContDiffWithinAt	—	contDiffWithinAt_congr Set.mem_insert_of_mem Set.mem_insert
contDiffWithinAt_congr_of_mem 📖	mathematical	Set Set.instMembership	ContDiffWithinAt	—	contDiffWithinAt_congr
contDiffWithinAt_congr_set 📖	mathematical	Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	ContDiffWithinAt	—	ContDiffWithinAt.congr_set Filter.EventuallyEq.symm
contDiffWithinAt_diff_singleton 📖	mathematical	—	ContDiffWithinAt Set Set.instSDiff Set.instSingletonSet	—	contDiffWithinAt_insert Set.insert_diff_singleton
contDiffWithinAt_iff_contDiffAt 📖	mathematical	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	ContDiffWithinAt ContDiffAt	—	Set.univ_inter contDiffWithinAt_inter contDiffWithinAt_univ
contDiffWithinAt_iff_contDiffOn_nhds 📖	mathematical	—	ContDiffWithinAt Set Filter Filter.instMembership nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.instInsert ContDiffOn	—	ContDiffWithinAt.contDiffOn le_rfl instIsEmptyFalse mem_of_mem_nhdsWithin Set.mem_insert ContDiffWithinAt.mono_of_mem_nhdsWithin nhdsWithin_mono Set.subset_insert
contDiffWithinAt_iff_forall_nat_le 📖	mathematical	—	ContDiffWithinAt WithTop.some ENat WithTop WithTop.natCast ENat.instNatCast	—	ContDiffWithinAt.of_le le_rfl
contDiffWithinAt_iff_of_ne_infty 📖	mathematical	—	ContDiffWithinAt Set Filter Filter.instMembership nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.instInsert HasFTaylorSeriesUpToOn AnalyticOn ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.normedAddCommGroup' Fin.fintype ContinuousMultilinearMap.normedSpace' smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self nhdsWithin_insert instIsEmptyFalse
contDiffWithinAt_infty 📖	mathematical	—	ContDiffWithinAt WithTop.some ENat Top.top instTopENat WithTop WithTop.natCast ENat.instNatCast	—	contDiffWithinAt_iff_forall_nat_le
contDiffWithinAt_insert 📖	mathematical	—	ContDiffWithinAt Set Set.instInsert	—	eq_or_ne contDiffWithinAt_insert_self ContDiffWithinAt.mono Set.subset_insert ContDiffWithinAt.mono_of_mem_nhdsWithin nhdsWithin_insert_of_ne T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
contDiffWithinAt_insert_self 📖	mathematical	—	ContDiffWithinAt Set Set.instInsert	—	Set.insert_eq_of_mem nhdsWithin_insert Set.insert_idem
contDiffWithinAt_inter 📖	mathematical	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	ContDiffWithinAt Set Set.instInter	—	contDiffWithinAt_inter' mem_nhdsWithin_of_mem_nhds
contDiffWithinAt_inter' 📖	mathematical	Set Filter Filter.instMembership nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	ContDiffWithinAt Set Set.instInter	—	contDiffWithinAt_congr_set Filter.EventuallyEq.symm mem_nhdsWithin_iff_eventuallyEq
contDiffWithinAt_nat 📖	mathematical	—	ContDiffWithinAt WithTop ENat WithTop.natCast ENat.instNatCast Set Filter Filter.instMembership nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.instInsert HasFTaylorSeriesUpToOn	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul le_rfl HasFTaylorSeriesUpToOn.of_le IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.addLeftMono WithTop.zeroLEOneClass WithTop.charZero
contDiffWithinAt_omega_iff_analyticWithinAt 📖	mathematical	—	ContDiffWithinAt Top.top WithTop ENat WithTop.top AnalyticWithinAt	—	ContDiffWithinAt.analyticWithinAt IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self AnalyticWithinAt.exists_hasFTaylorSeriesUpToOn HasFTaylorSeriesUpToOn.of_le le_top
contDiffWithinAt_succ_iff_hasFDerivWithinAt 📖	mathematical	—	ContDiffWithinAt WithTop ENat WithTop.add instAddENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat Set Filter Filter.instMembership nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.instInsert AnalyticOn HasFDerivWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring 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	—	RingHomIsometric.ids smulCommClass_self IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul contDiffWithinAt_iff_of_ne_infty HasFTaylorSeriesUpToOn.analyticOn RingHomInvPair.ids HasFTaylorSeriesUpToOn.hasFDerivWithinAt Unique.instSubsingleton WithTop.canonicallyOrderedAdd NeZero.charZero_one WithTop.charZero Set.insert_eq_of_mem mem_of_mem_nhdsWithin self_mem_nhdsWithin hasFTaylorSeriesUpToOn_succ_iff_right AnalyticOnNhd.comp_analyticOn ContinuousLinearMap.smulCommClass LinearIsometryEquiv.analyticOnNhd Set.mapsTo_univ Filter.inter_mem nhdsWithin_le_of_mem nhdsWithin_mono Set.subset_insert RingHomCompTriple.ids LinearIsometryEquiv.comp_hasFDerivWithinAt_iff' HasFTaylorSeriesUpToOn.zero_eq ContinuousLinearMap.ext Fin.isEmpty' HasFDerivWithinAt.mono Set.inter_subset_right Fin.init_snoc ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.continuousConstSMul FormalMultilinearSeries.ext ContinuousMultilinearMap.ext Fin.snoc_last HasFTaylorSeriesUpToOn.congr HasFTaylorSeriesUpToOn.mono Set.inter_subset_left AnalyticOn.mono
contDiffWithinAt_succ_iff_hasFDerivWithinAt' 📖	mathematical	—	ContDiffWithinAt WithTop ENat WithTop.add instAddENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat Set Filter Filter.instMembership nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.instInsert Set.instHasSubset AnalyticOn HasFDerivWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring 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	—	RingHomIsometric.ids smulCommClass_self contDiffWithinAt_succ_iff_hasFDerivWithinAt mem_nhdsWithin inter_mem_nhdsWithin IsOpen.mem_nhds Set.inter_subset_left AnalyticOn.mono Set.inter_comm HasFDerivWithinAt.mono_of_mem_nhdsWithin HasFDerivWithinAt.mono Set.inter_subset_inter Set.subset_insert subset_refl Set.instReflSubset ContDiffWithinAt.mono_of_mem_nhdsWithin nhdsWithin_mono contDiffWithinAt_insert Set.insert_eq_of_mem Set.mem_insert HasFDerivWithinAt.insert' T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ContDiffWithinAt.mono ContDiffWithinAt.insert
contDiffWithinAt_univ 📖	mathematical	—	ContDiffWithinAt Set.univ ContDiffAt	—	—
contDiffWithinAt_zero 📖	mathematical	Set Set.instMembership	ContDiffWithinAt WithTop ENat WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Set Filter Filter.instMembership nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ContinuousOn Set.instInter	—	le_rfl Set.insert_eq_of_mem ContinuousOn.mono IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Nat.cast_zero Set.inter_subset_right contDiffWithinAt_inter' mem_of_mem_nhdsWithin ContDiffOn.contDiffWithinAt contDiffOn_zero
contDiff_all_iff_nat 📖	mathematical	—	ContDiff WithTop.some ENat WithTop WithTop.natCast ENat.instNatCast	—	—
contDiff_iff_contDiffAt 📖	mathematical	—	ContDiff ContDiffAt	—	—
contDiff_iff_continuous_differentiable 📖	mathematical	—	ContDiff WithTop.some ENat 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 iteratedFDeriv Differentiable 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	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self contDiffOn_univ contDiffOn_iff_continuousOn_differentiableOn uniqueDiffOn_univ NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul iteratedFDerivWithin_univ differentiableOn_univ
contDiff_iff_forall_nat_le 📖	mathematical	—	ContDiff WithTop.some ENat WithTop WithTop.natCast ENat.instNatCast	—	contDiffOn_iff_forall_nat_le
contDiff_iff_ftaylorSeries 📖	mathematical	—	ContDiff WithTop.some ENat HasFTaylorSeriesUpTo ftaylorSeries	—	contDiffOn_univ hasFTaylorSeriesUpToOn_univ_iff IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ftaylorSeriesWithin_univ ContDiffOn.ftaylorSeriesWithin uniqueDiffOn_univ NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul
contDiff_infty 📖	mathematical	—	ContDiff WithTop.some ENat Top.top instTopENat WithTop WithTop.natCast ENat.instNatCast	—	contDiffOn_univ
contDiff_infty_iff_fderiv 📖	mathematical	—	ContDiff WithTop.some ENat Top.top instTopENat Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing fderiv	—	RingHomIsometric.ids smulCommClass_self ENat.coe_top_add_one contDiff_succ_iff_fderiv instIsEmptyFalse
contDiff_nat_iff_continuous_differentiable 📖	mathematical	—	ContDiff WithTop ENat 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 iteratedFDeriv Differentiable 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	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self WithTop.coe_natCast contDiff_iff_continuous_differentiable IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid
contDiff_of_differentiable_iteratedFDeriv 📖	mathematical	Differentiable 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	ContDiff WithTop.some ENat	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self contDiff_iff_continuous_differentiable Differentiable.continuous IsTopologicalAddGroup.toContinuousAdd IsBoundedSMul.continuousSMul ContinuousMultilinearMap.instIsTopologicalAddGroup ContinuousMultilinearMap.instContinuousSMul le_of_lt
contDiff_omega_iff_analyticOnNhd 📖	mathematical	—	ContDiff Top.top WithTop ENat WithTop.top AnalyticOnNhd Set.univ	—	ContDiff.analyticOnNhd AnalyticOnNhd.contDiff
contDiff_one_iff_fderiv 📖	mathematical	—	ContDiff WithTop ENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Continuous ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup fderiv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup zero_add RingHomIsometric.ids smulCommClass_self contDiff_succ_iff_fderiv instIsEmptyFalse
contDiff_one_iff_hasFDerivAt 📖	mathematical	—	ContDiff WithTop ENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat Continuous 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.topologicalSpace NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup HasFDerivAt	—	SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomIsometric.ids smulCommClass_self CharP.cast_eq_zero CharP.ofCharZero WithTop.charZero contDiff_succ_iff_hasFDerivAt
contDiff_succ_iff_fderiv 📖	mathematical	—	ContDiff WithTop ENat WithTop.add instAddENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AnalyticOnNhd Set.univ ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing fderiv	—	RingHomIsometric.ids smulCommClass_self contDiffOn_succ_iff_fderivWithin uniqueDiffOn_univ NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul
contDiff_succ_iff_hasFDerivAt 📖	mathematical	—	ContDiff WithTop ENat WithTop.add instAddENat WithTop.natCast ENat.instNatCast WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat 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 HasFDerivAt NormedAddCommGroup.toAddCommGroup	—	RingHomIsometric.ids smulCommClass_self contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn uniqueDiffOn_univ NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul
contDiff_zero 📖	mathematical	—	ContDiff WithTop ENat WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	contDiffOn_univ continuousOn_univ contDiffOn_zero
iteratedFDerivWithin_eq_iteratedFDeriv 📖	mathematical	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContDiffAt WithTop ENat WithTop.natCast ENat.instNatCast Set Set.instMembership	iteratedFDerivWithin iteratedFDeriv	—	iteratedFDerivWithin_univ ContDiffWithinAt.contDiffOn' le_rfl iteratedFDerivWithin_inter_open iteratedFDerivWithin_subset Set.inter_subset_inter_left Set.subset_univ UniqueDiffOn.inter IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup uniqueDiffOn_univ NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Set.univ_inter Set.insert_eq_of_mem
iteratedFDerivWithin_subset 📖	mathematical	Set Set.instHasSubset UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContDiffOn WithTop ENat WithTop.natCast ENat.instNatCast Set.instMembership	iteratedFDerivWithin	—	HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn HasFTaylorSeriesUpToOn.mono ContDiffOn.ftaylorSeriesWithin le_rfl

---

← Back to Index