Extend

📁 Source: Mathlib/Analysis/Calculus/FDeriv/Extend.lean

Statistics

Metric	Count
Definitions	0
Theorems hasDerivAt_of_hasDerivAt_of_ne, hasDerivAt_of_hasDerivAt_of_ne', hasDerivWithinAt_Ici_of_tendsto_deriv, hasDerivWithinAt_Iic_of_tendsto_deriv, hasFDerivWithinAt_closure_of_tendsto_fderiv	5
Total	5

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasDerivAt_of_hasDerivAt_of_ne 📖	—	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul ContinuousAt	—	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul DifferentiableAt.differentiableWithinAt HasDerivAt.differentiableAt ne_of_gt hasDerivWithinAt_Ici_of_tendsto_deriv ContinuousAt.continuousWithinAt self_mem_nhdsWithin Filter.tendsto_inf_left Filter.Tendsto.congr' Filter.mem_of_superset HasDerivAt.deriv ne_of_lt hasDerivWithinAt_Iic_of_tendsto_deriv HasDerivWithinAt.congr_simp Set.Iic_union_Ici HasDerivWithinAt.union
hasDerivAt_of_hasDerivAt_of_ne' 📖	—	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul ContinuousAt	—	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul eq_or_ne hasDerivAt_of_hasDerivAt_of_ne
hasDerivWithinAt_Ici_of_tendsto_deriv 📖	mathematical	DifferentiableOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace ContinuousWithinAt Set Filter Filter.instMembership nhdsWithin Set.Ioi Real.instPreorder Filter.Tendsto deriv nhds	HasDerivWithinAt IsBoundedSMul.continuousSMul Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul Set.Ici	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul mem_nhdsGT_iff_exists_Ioc_subset instOrderTopologyReal instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Set.Subset.trans Set.Ioo_subset_Ioc_self DifferentiableOn.mono convex_Ioo Real.instIsOrderedCancelAddMonoid IsStrictOrderedModule.toPosSMulStrictMono IsStrictOrderedRing.toIsStrictOrderedModule isOpen_Ioo HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid closure_Ioo LT.lt.ne ContinuousWithinAt.mono lt_of_le_of_ne DifferentiableOn.continuousOn IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsScalarTower.left toSpanSingleton_deriv Filter.Tendsto.comp RingHomIsometric.ids Continuous.continuousAt IsBoundedBilinearMap.continuous_right Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing smulCommClass_self IsBoundedSMul.toUniformContinuousConstSMul isBoundedBilinearMap_smulRight tendsto_nhdsWithin_mono_left Set.Ioo_subset_Ioi_self hasDerivWithinAt_iff_hasFDerivWithinAt hasFDerivWithinAt_closure_of_tendsto_fderiv HasDerivWithinAt.mono_of_mem_nhdsWithin Icc_mem_nhdsGE instClosedIciTopology
hasDerivWithinAt_Iic_of_tendsto_deriv 📖	mathematical	DifferentiableOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace ContinuousWithinAt Set Filter Filter.instMembership nhdsWithin Set.Iio Real.instPreorder Filter.Tendsto deriv nhds	HasDerivWithinAt IsBoundedSMul.continuousSMul Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul Set.Iic	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul mem_nhdsLT_iff_exists_Ico_subset instOrderTopologyReal instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Set.Subset.trans Set.Ioo_subset_Ico_self DifferentiableOn.mono convex_Ioo Real.instIsOrderedCancelAddMonoid IsStrictOrderedModule.toPosSMulStrictMono IsStrictOrderedRing.toIsStrictOrderedModule isOpen_Ioo HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid closure_Ioo ne_of_lt ContinuousWithinAt.mono lt_of_le_of_ne DifferentiableOn.continuousOn IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsScalarTower.left toSpanSingleton_deriv Filter.Tendsto.comp RingHomIsometric.ids Continuous.continuousAt IsBoundedBilinearMap.continuous_right Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing smulCommClass_self IsBoundedSMul.toUniformContinuousConstSMul isBoundedBilinearMap_smulRight tendsto_nhdsWithin_mono_left Set.Ioo_subset_Iio_self hasDerivWithinAt_iff_hasFDerivWithinAt hasFDerivWithinAt_closure_of_tendsto_fderiv HasDerivWithinAt.mono_of_mem_nhdsWithin Icc_mem_nhdsLE instClosedIicTopology
hasFDerivWithinAt_closure_of_tendsto_fderiv 📖	mathematical	DifferentiableOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Convex Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction IsOpen ContinuousWithinAt Filter.Tendsto ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid fderiv nhdsWithin nhds ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	HasFDerivWithinAt closure	—	SeminormedAddCommGroup.toIsTopologicalAddGroup HasFDerivWithinAt.of_notMem_closure closure_closure HasFDerivWithinAt.eq_1 hasFDerivAtFilter_iff_isLittleO Asymptotics.isLittleO_iff RingHomIsometric.ids Metric.tendsto_nhdsWithin_nhds Convex.inter convex_ball DifferentiableOn.mono Set.inter_subset_right IsOpen.inter Metric.isOpen_ball DifferentiableAt.fderivWithin IsTopologicalAddGroup.toContinuousAdd IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace DifferentiableWithinAt.differentiableAt IsOpen.mem_nhds IsOpen.uniqueDiffOn PerfectSpace.not_isolated instPerfectSpace le_of_lt map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass Convex.norm_image_sub_le_of_norm_fderivWithin_le' instIsRCLikeNormedField Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub Continuous.continuousWithinAt ContinuousLinearMap.cont ContinuousWithinAt.closure_le HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Set.prod_mono closure_prod_eq closure_mono ContinuousWithinAt.mono nhdsWithin_prod_eq Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.const_add_termg Filter.Tendsto.comp Continuous.continuousAt continuous_norm Filter.tendsto_snd Filter.tendsto_fst tendsto_nhdsWithin_of_tendsto_nhds nhds_prod_eq Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal tendsto_const_nhds IsOpen.inter_closure Metric.mem_ball_self Metric.mem_nhdsWithin_iff

---

← Back to Index