LHopital

📁 Source: Mathlib/Analysis/Calculus/LHopital.lean

Statistics

Metric	Count
Definitions	0
Theorems lhopital_zero_atBot, lhopital_zero_atBot_on_Iio, lhopital_zero_atTop, lhopital_zero_atTop_on_Ioi, lhopital_zero_left_on_Ioc, lhopital_zero_left_on_Ioo, lhopital_zero_nhds, lhopital_zero_nhdsGT, lhopital_zero_nhdsLT, lhopital_zero_nhdsNE, lhopital_zero_right_on_Ico, lhopital_zero_right_on_Ioo, lhopital_zero_nhdsWithin_convex, lhopital_zero_atBot, lhopital_zero_atBot_on_Iio, lhopital_zero_atTop, lhopital_zero_atTop_on_Ioi, lhopital_zero_left_on_Ioo, lhopital_zero_nhds, lhopital_zero_nhdsGT, lhopital_zero_nhdsLT, lhopital_zero_nhdsNE, lhopital_zero_nhdsWithin_convex, lhopital_zero_right_on_Ico, lhopital_zero_right_on_Ioo, lhopital_zero_nhdsWithin_convex	26
Total	26

HasDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lhopital_zero_atBot 📖	—	Filter.Eventually Real HasDerivAt 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 ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Filter.atBot Real.instPreorder Real.instZero Filter.Tendsto nhds DivInvMonoid.toDiv Real.instDivInvMonoid	—	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.eventually_iff_exists_mem Filter.inter_mem Filter.mem_atBot_sets instIsCodirectedOrder Real.instIsOrderedRing Real.instArchimedean le_of_lt lhopital_zero_atBot_on_Iio
lhopital_zero_atBot_on_Iio 📖	—	HasDerivAt 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 ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Filter.Tendsto Filter.atBot Real.instPreorder nhds Real.instZero DivInvMonoid.toDiv Real.instDivInvMonoid	—	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal comp hasDerivAt_neg lhopital_zero_atTop_on_Ioi Set.neg_Iio Real.instIsOrderedAddMonoid neg_eq_zero neg_eq_neg_one_mul mul_comm Filter.Tendsto.comp Filter.tendsto_neg_atTop_atBot mul_neg mul_one neg_div_neg_eq Filter.tendsto_neg_atBot_atTop neg_neg
lhopital_zero_atTop 📖	—	Filter.Eventually Real HasDerivAt 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 ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Filter.atTop Real.instPreorder Real.instZero Filter.Tendsto nhds DivInvMonoid.toDiv Real.instDivInvMonoid	—	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.eventually_iff_exists_mem Filter.inter_mem Filter.mem_atTop_sets instIsDirectedOrder Real.instIsOrderedRing Real.instArchimedean le_of_lt lhopital_zero_atTop_on_Ioi
lhopital_zero_atTop_on_Ioi 📖	—	HasDerivAt 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 ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Filter.Tendsto Filter.atTop Real.instPreorder nhds Real.instZero DivInvMonoid.toDiv Real.instDivInvMonoid	—	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal lt_of_le_of_lt le_max_left lt_one_add Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_max_right ne_of_lt lt_trans lt_inv_comm₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono comp hasDerivAt_inv lhopital_zero_right_on_Ioo inv_pos mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass neg_ne_zero inv_ne_zero pow_ne_zero isReduced_of_noZeroDivisors Filter.Tendsto.comp tendsto_inv_nhdsGT_zero instOrderTopologyReal Filter.tendsto_congr' Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' mul_div_mul_right ne_of_gt inv_pos_of_pos pow_pos IsStrictOrderedRing.toZeroLEOneClass tendsto_inv_atTop_nhdsGT_zero inv_inv
lhopital_zero_left_on_Ioc 📖	—	Real Real.instLT HasDerivAt 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 ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal ContinuousOn Set.Ioc Real.instPreorder Real.instZero Filter.Tendsto DivInvMonoid.toDiv Real.instDivInvMonoid nhdsWithin Set.Iio	—	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal lhopital_zero_left_on_Ioo nhdsWithin_Ioo_eq_nhdsLT instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid ContinuousWithinAt.tendsto ContinuousWithinAt.mono Set.right_mem_Ioc Set.Ioo_subset_Ioc_self
lhopital_zero_left_on_Ioo 📖	—	Real Real.instLT HasDerivAt 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 ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Filter.Tendsto nhdsWithin Set.Iio Real.instPreorder nhds Real.instZero DivInvMonoid.toDiv Real.instDivInvMonoid	—	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal comp hasDerivAt_neg lhopital_zero_right_on_Ioo neg_lt_neg Real.instIsOrderedAddMonoid Set.neg_Ioo neg_eq_zero neg_eq_neg_one_mul mul_comm Filter.Tendsto.comp tendsto_neg_nhdsGT_neg IsTopologicalRing.toContinuousNeg mul_neg mul_one neg_div_neg_eq tendsto_neg_nhdsLT neg_neg
lhopital_zero_nhds 📖	mathematical	Filter.Eventually Real HasDerivAt 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 ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal nhds Real.instZero Filter.Tendsto DivInvMonoid.toDiv Real.instDivInvMonoid	nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal lhopital_zero_nhdsNE eventually_nhdsWithin_of_eventually_nhds tendsto_nhdsWithin_of_tendsto_nhds
lhopital_zero_nhdsGT 📖	—	Filter.Eventually Real HasDerivAt 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 ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal nhdsWithin Set.Ioi Real.instPreorder Real.instZero Filter.Tendsto nhds DivInvMonoid.toDiv Real.instDivInvMonoid	—	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.eventually_iff_exists_mem Filter.inter_mem mem_nhdsGT_iff_exists_Ioo_subset instOrderTopologyReal instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial lhopital_zero_right_on_Ioo
lhopital_zero_nhdsLT 📖	—	Filter.Eventually Real HasDerivAt 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 ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal nhdsWithin Set.Iio Real.instPreorder Real.instZero Filter.Tendsto nhds DivInvMonoid.toDiv Real.instDivInvMonoid	—	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.eventually_iff_exists_mem Filter.inter_mem mem_nhdsLT_iff_exists_Ioo_subset instOrderTopologyReal instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial lhopital_zero_left_on_Ioo
lhopital_zero_nhdsNE 📖	—	Filter.Eventually Real HasDerivAt 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 ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet Real.instZero Filter.Tendsto nhds DivInvMonoid.toDiv Real.instDivInvMonoid	—	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal nhdsWithin_union lhopital_zero_nhdsLT lhopital_zero_nhdsGT
lhopital_zero_right_on_Ico 📖	—	Real Real.instLT HasDerivAt 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 ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal ContinuousOn Set.Ico Real.instPreorder Real.instZero Filter.Tendsto DivInvMonoid.toDiv Real.instDivInvMonoid nhdsWithin Set.Ioi	—	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal lhopital_zero_right_on_Ioo nhdsWithin_Ioo_eq_nhdsGT instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid ContinuousWithinAt.tendsto ContinuousWithinAt.mono Set.left_mem_Ico Set.Ioo_subset_Ico_self
lhopital_zero_right_on_Ioo 📖	—	Real Real.instLT HasDerivAt 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 ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Filter.Tendsto nhdsWithin Set.Ioi Real.instPreorder nhds Real.instZero DivInvMonoid.toDiv Real.instDivInvMonoid	—	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Set.Ioo_subset_Ioo le_refl le_of_lt nhdsWithin_Ioo_eq_nhdsLT instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid ContinuousWithinAt.tendsto ContinuousWithinAt.mono ContinuousAt.continuousWithinAt continuousAt exists_hasDerivAt_eq_zero' sub_zero exists_ratio_hasDerivAt_eq_ratio_slope' tendsto_nhdsWithin_of_tendsto_nhds ContinuousAt.tendsto nhdsWithin_Ioo_eq_nhdsGT instClosedIciTopology tendsto_nhdsWithin_congr Filter.Tendsto.comp tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within tendsto_of_tendsto_of_tendsto_of_le_of_le' instOrderTopologyReal tendsto_const_nhds Filter.tendsto_id eventually_nhdsWithin_of_forall le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Linarith.add_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing lt_of_not_ge Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_nonpos_of_le Function.sometimes_spec

HasDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lhopital_zero_nhdsWithin_convex 📖	—	Convex Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Filter.Eventually HasDerivWithinAt 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 ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Set Set.instSDiff Set.instSingletonSet nhdsWithin Real.instZero Filter.Tendsto nhds DivInvMonoid.toDiv Real.instDivInvMonoid	—	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.Tendsto.of_neBot_imp closure_mono Set.diff_subset mem_closure_iff_nhdsWithin_neBot Convex.diff_singleton_eventually_mem_nhds Real.instIsStrictOrderedRing instOrderTopologyReal IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Filter.Eventually.mp Filter.Eventually.mono hasDerivAt Set.eq_empty_or_nonempty Set.inter_union_distrib_left Set.union_self nhdsWithin_empty Convex.nhdsWithin_diff_eq_nhdsGT HasDerivAt.lhopital_zero_nhdsGT Convex.nhdsWithin_diff_eq_nhdsLT HasDerivAt.lhopital_zero_nhdsLT Convex.nhdsWithin_diff_eq_nhdsNE HasDerivAt.lhopital_zero_nhdsNE

deriv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lhopital_zero_atBot 📖	—	Filter.Eventually Real DifferentiableAt 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 Filter.atBot Real.instPreorder deriv Real.instZero Filter.Tendsto nhds DivInvMonoid.toDiv Real.instDivInvMonoid	—	—	Filter.Eventually.mono by_contradiction deriv_zero_of_not_differentiableAt ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal DifferentiableAt.hasDerivAt HasDerivAt.lhopital_zero_atBot
lhopital_zero_atBot_on_Iio 📖	—	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 Set.Iio Real.instPreorder Filter.Tendsto Filter.atBot nhds Real.instZero DivInvMonoid.toDiv Real.instDivInvMonoid deriv	—	—	DifferentiableWithinAt.differentiableAt Iio_mem_nhds instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid by_contradiction deriv_zero_of_not_differentiableAt HasDerivAt.lhopital_zero_atBot_on_Iio DifferentiableAt.hasDerivAt
lhopital_zero_atTop 📖	—	Filter.Eventually Real DifferentiableAt 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 Filter.atTop Real.instPreorder deriv Real.instZero Filter.Tendsto nhds DivInvMonoid.toDiv Real.instDivInvMonoid	—	—	Filter.Eventually.mp Filter.Eventually.of_forall by_contradiction deriv_zero_of_not_differentiableAt ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.Eventually.mono DifferentiableAt.hasDerivAt HasDerivAt.lhopital_zero_atTop
lhopital_zero_atTop_on_Ioi 📖	—	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 Set.Ioi Real.instPreorder Filter.Tendsto Filter.atTop nhds Real.instZero DivInvMonoid.toDiv Real.instDivInvMonoid deriv	—	—	DifferentiableWithinAt.differentiableAt Ioi_mem_nhds instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid by_contradiction deriv_zero_of_not_differentiableAt HasDerivAt.lhopital_zero_atTop_on_Ioi DifferentiableAt.hasDerivAt
lhopital_zero_left_on_Ioo 📖	—	Real Real.instLT DifferentiableOn 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 Set.Ioo Real.instPreorder Filter.Tendsto nhdsWithin Set.Iio nhds Real.instZero DivInvMonoid.toDiv Real.instDivInvMonoid deriv	—	—	DifferentiableWithinAt.differentiableAt Ioo_mem_nhds HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid by_contradiction deriv_zero_of_not_differentiableAt HasDerivAt.lhopital_zero_left_on_Ioo DifferentiableAt.hasDerivAt
lhopital_zero_nhds 📖	mathematical	Filter.Eventually Real DifferentiableAt 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 nhds deriv Real.instZero Filter.Tendsto DivInvMonoid.toDiv Real.instDivInvMonoid	nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	—	lhopital_zero_nhdsNE eventually_nhdsWithin_of_eventually_nhds tendsto_nhdsWithin_of_tendsto_nhds
lhopital_zero_nhdsGT 📖	—	Filter.Eventually Real DifferentiableAt 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 nhdsWithin Set.Ioi Real.instPreorder deriv Real.instZero Filter.Tendsto nhds DivInvMonoid.toDiv Real.instDivInvMonoid	—	—	Set.Ici_diff_left lhopital_zero_nhdsWithin_convex convex_Ici Real.instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing
lhopital_zero_nhdsLT 📖	—	Filter.Eventually Real DifferentiableAt 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 nhdsWithin Set.Iio Real.instPreorder deriv Real.instZero Filter.Tendsto nhds DivInvMonoid.toDiv Real.instDivInvMonoid	—	—	Set.Iic_diff_right lhopital_zero_nhdsWithin_convex convex_Iic Real.instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing
lhopital_zero_nhdsNE 📖	—	Filter.Eventually Real DifferentiableAt 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 nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet deriv Real.instZero Filter.Tendsto nhds DivInvMonoid.toDiv Real.instDivInvMonoid	—	—	Set.compl_eq_univ_diff lhopital_zero_nhdsWithin_convex convex_univ
lhopital_zero_nhdsWithin_convex 📖	—	Convex Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Filter.Eventually DifferentiableAt 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 nhdsWithin Set Set.instSDiff Set.instSingletonSet deriv Real.instZero Filter.Tendsto nhds DivInvMonoid.toDiv Real.instDivInvMonoid	—	—	derivWithin.lhopital_zero_nhdsWithin_convex Filter.Eventually.mono DifferentiableAt.differentiableWithinAt Filter.Eventually.mp Convex.diff_singleton_eventually_mem_nhds Real.instIsStrictOrderedRing instOrderTopologyReal derivWithin_of_mem_nhds Filter.Tendsto.congr'
lhopital_zero_right_on_Ico 📖	—	Real Real.instLT DifferentiableOn 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 Set.Ioo Real.instPreorder ContinuousOn Set.Ico Real.instZero Filter.Tendsto DivInvMonoid.toDiv Real.instDivInvMonoid deriv nhdsWithin Set.Ioi	—	—	lhopital_zero_right_on_Ioo nhdsWithin_Ioo_eq_nhdsGT instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid ContinuousWithinAt.tendsto ContinuousWithinAt.mono Set.left_mem_Ico Set.Ioo_subset_Ico_self
lhopital_zero_right_on_Ioo 📖	—	Real Real.instLT DifferentiableOn 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 Set.Ioo Real.instPreorder Filter.Tendsto nhdsWithin Set.Ioi nhds Real.instZero DivInvMonoid.toDiv Real.instDivInvMonoid deriv	—	—	DifferentiableWithinAt.differentiableAt Ioo_mem_nhds HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid by_contradiction deriv_zero_of_not_differentiableAt HasDerivAt.lhopital_zero_right_on_Ioo DifferentiableAt.hasDerivAt

derivWithin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lhopital_zero_nhdsWithin_convex 📖	—	Convex Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Filter.Eventually DifferentiableWithinAt 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 Set Set.instSDiff Set.instSingletonSet nhdsWithin derivWithin Real.instZero Filter.Tendsto nhds DivInvMonoid.toDiv Real.instDivInvMonoid	—	—	Filter.Eventually.mp Filter.Eventually.of_forall by_contradiction derivWithin_zero_of_not_differentiableWithinAt ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal DifferentiableWithinAt.hasDerivWithinAt HasDerivWithinAt.lhopital_zero_nhdsWithin_convex

---

← Back to Index