Documentation Verification Report

Monotone

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

Statistics

Metric	Count
Definitions	0
Theorems `ae_differentiableAt`, `ae_hasDerivAt`, `ae_differentiableWithinAt`, `ae_differentiableWithinAt_of_mem`, `ae_hasDerivAt`, `tendsto_apply_add_mul_sq_div_sub`	6
Total	6

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_differentiableAt` 📖	mathematical	`Monotone` `Real` `Real.instPreorder`	`Filter.Eventually` `DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.MeasureSpace.volume`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `ae_hasDerivAt` `Filter.univ_mem'` `HasDerivAt.differentiableAt`
`ae_hasDerivAt` 📖	mathematical	`Monotone` `Real` `Real.instPreorder`	`Filter.Eventually` `HasDerivAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IsModuleTopology.toContinuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Real.instAdd` `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` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsTopologicalSemiring.toIsModuleTopology` `Real.semiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal` `ENNReal.toReal` `MeasureTheory.Measure.rnDeriv` `Real.measurableSpace` `StieltjesFunction.measure` `Real.linearOrder` `stieltjesFunction` `instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `Real.instConditionallyCompleteLinearOrder` `Real.borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `Real.instField` `Real.partialOrder` `PosMulReflectLE.toPosMulReflectLT` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `PosMulStrictMono.toPosMulReflectLE` `MulZeroClass.toMul` `MulZeroClass.toZero` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Set.Countable.ae_notMem` `countable_not_continuousAt` `Real.noAtoms_volume` `StieltjesFunction.ae_hasDerivAt` `Filter.univ_mem'` `le_antisymm` `continuousAt_iff_leftLim_eq_rightLim` `leftLim_le` `le_refl` `le_rightLim` `tendsto_apply_add_mul_sq_div_sub` `nhdsGT_le_nhdsNE` `slope_fun_def_field` `Filter.tendsto_sup` `nhdsLT_sup_nhdsGT` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `hasDerivAt_iff_tendsto_slope` `tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within` `Filter.Tendsto.mono_left` `Filter.Tendsto.add` `IsTopologicalSemiring.toContinuousAdd` `Filter.tendsto_id` `Filter.Tendsto.const_mul` `IsTopologicalSemiring.toContinuousMul` `Filter.Tendsto.pow` `Filter.Tendsto.sub_const` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `neg_mul` `one_mul` `sub_self` `zero_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `MulZeroClass.mul_zero` `add_zero` `nhdsWithin_le_nhds` `Ioo_mem_nhdsGT` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `contravariant_lt_of_covariant_le` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Set.mem_Ioi` `lt_of_not_ge` `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.mul_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `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.pow_congr` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_nat` `Mathlib.Tactic.Ring.coeff_one` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.pow_bit0` `Mathlib.Tactic.Ring.pow_one` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `mul_pos_of_neg_of_neg` `AddGroup.existsAddOfLE` `IsStrictOrderedRing.toMulPosStrictMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `contravariant_swap_add_of_contravariant_add` `tendsto_of_tendsto_of_tendsto_of_le_of_le'` `self_mem_nhdsWithin` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `sub_le_sub_right` `rightLim_le` `sub_pos` `le_of_lt` `le_rfl` `nhdsLT_le_nhdsNE` `Ioo_mem_nhdsLT` `instClosedIicTopology` `Set.mem_Iio` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `sq_nonneg` `IsOrderedRing.toPosMulMono` `Set.mem_Ioo` `div_le_div_of_nonpos_of_le` `LT.lt.le` `sub_neg` `sub_le_sub_iff_right` `sq_pos_of_neg`

MonotoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_differentiableWithinAt` 📖	mathematical	`MonotoneOn` `Real` `Real.instPreorder` `MeasurableSet` `Real.measurableSpace`	`Filter.Eventually` `DifferentiableWithinAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_restrict_iff'` `ae_differentiableWithinAt_of_mem`
`ae_differentiableWithinAt_of_mem` 📖	mathematical	`MonotoneOn` `Real` `Real.instPreorder`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.MeasureSpace.volume`	—	`ae_of_mem_of_ae_of_mem_inter_Ioo` `Real.noAtoms_volume` `MeasureTheory.Measure.instOuterMeasureClass` `exists_monotone_extension` `mono` `Set.inter_subset_left` `map_bddBelow` `map_bddAbove` `Filter.mp_mem` `Monotone.ae_differentiableAt` `Filter.univ_mem'` `DifferentiableWithinAt.congr_of_eventuallyEq` `DifferentiableAt.differentiableWithinAt` `nhdsWithin_le_nhds` `Ioo_mem_nhds` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `self_mem_nhdsWithin` `LT.lt.le`

StieltjesFunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_hasDerivAt` 📖	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` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IsModuleTopology.toContinuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Real.instAdd` `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` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsTopologicalSemiring.toIsModuleTopology` `Real.semiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal` `toFun` `Real.linearOrder` `ENNReal.toReal` `MeasureTheory.Measure.rnDeriv` `Real.measurableSpace` `measure` `instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `Real.instConditionallyCompleteLinearOrder` `Real.borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `Real.instField` `Real.partialOrder` `PosMulReflectLE.toPosMulReflectLT` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `PosMulStrictMono.toPosMulReflectLE` `MulZeroClass.toMul` `MulZeroClass.toZero` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Set.Countable.ae_notMem` `countable_leftLim_ne` `Real.noAtoms_volume` `MeasureTheory.Measure.rnDeriv_lt_top` `MeasureTheory.sigmaFinite_of_locallyFinite` `instIsLocallyFiniteMeasure` `MeasureTheory.Measure.isUnifLocDoublingMeasureOfIsAddHaarMeasure` `FiniteDimensional.rclike_to_real` `instIsAddHaarMeasureVolume` `Real.locallyFinite_volume` `VitaliFamily.ae_tendsto_rnDeriv` `Filter.univ_mem'` `Filter.Tendsto.congr'` `self_mem_nhdsWithin` `measure_Icc` `Real.volume_Icc` `ENNReal.ofReal_div_of_pos` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `ENNReal.toReal_ofReal` `div_nonneg` `sub_nonneg` `mono` `LT.lt.le` `Filter.Tendsto.comp` `ENNReal.tendsto_toReal` `LT.lt.ne` `Real.tendsto_Icc_vitaliFamily_right` `Monotone.leftLim_le` `neg_neg` `div_neg` `neg_div'` `neg_sub` `Real.tendsto_Icc_vitaliFamily_left` `tendsto_apply_add_mul_sq_div_sub` `nhdsLT_le_nhdsNE` `tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within` `Filter.Tendsto.mono_left` `Filter.Tendsto.add` `IsTopologicalSemiring.toContinuousAdd` `Filter.tendsto_id` `Filter.Tendsto.const_mul` `IsTopologicalSemiring.toContinuousMul` `Filter.Tendsto.pow` `Filter.Tendsto.sub_const` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `one_mul` `sub_self` `zero_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `MulZeroClass.mul_zero` `add_zero` `nhdsWithin_le_nhds` `Ioo_mem_nhdsLT` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Set.mem_Iio` `lt_of_not_ge` `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.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.pow_congr` `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_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_nat` `Mathlib.Tactic.Ring.coeff_one` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.pow_bit0` `Mathlib.Tactic.Ring.pow_one` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `mul_pos_of_neg_of_neg` `AddGroup.existsAddOfLE` `IsStrictOrderedRing.toMulPosStrictMono` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `tendsto_of_tendsto_of_tendsto_of_le_of_le'` `div_le_div_of_nonpos_of_le` `le_of_not_gt` `Mathlib.Tactic.Linarith.add_neg` `sub_le_sub_iff_right` `Monotone.le_leftLim` `sq_pos_of_pos` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `le_refl` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `hasDerivAt_iff_tendsto_slope` `slope_fun_def_field` `nhdsLT_sup_nhdsGT` `Filter.tendsto_sup`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_apply_add_mul_sq_div_sub` 📖	—	`Filter` `Real` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Filter.Tendsto` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instSub` `nhds` `Real.instAdd` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid`	—	—	`Filter.Tendsto.mono_left` `Filter.Tendsto.const_add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Filter.Tendsto.const_mul` `IsTopologicalSemiring.toContinuousMul` `Filter.Tendsto.sub_const` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `Filter.tendsto_id` `LE.le.trans` `nhdsWithin_le_nhds` `Filter.Tendsto.congr'` `Filter.Eventually.filter_mono` `Filter.mp_mem` `self_mem_nhdsWithin` `Filter.univ_mem'` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `sub_ne_zero` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_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_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_nat` `Mathlib.Tactic.Ring.coeff_one` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.pow_bit0` `Mathlib.Tactic.Ring.pow_one` `Mathlib.Tactic.Ring.pow_zero` `sub_self` `MulZeroClass.mul_zero` `add_zero` `Filter.Tendsto.mul` `Filter.Tendsto.comp` `Filter.Tendsto.mono_right` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Tactic.FieldSimp.eq_div_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div'`

---

← Back to Index