UniformLimitsDeriv

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

Statistics

Metric	Count
Definitions	0
Theorems one_smulRight, cauchy_map_of_uniformCauchySeqOn_fderiv, difference_quotients_converge_uniformly, hasDerivAt_of_tendstoLocallyUniformlyOn, hasDerivAt_of_tendstoUniformly, hasDerivAt_of_tendstoUniformlyOn, hasDerivAt_of_tendstoUniformlyOnFilter, hasDerivAt_of_tendsto_locally_uniformly_on', hasFDerivAt_of_tendstoLocallyUniformlyOn, hasFDerivAt_of_tendstoUniformly, hasFDerivAt_of_tendstoUniformlyOn, hasFDerivAt_of_tendstoUniformlyOnFilter, hasFDerivAt_of_tendsto_locally_uniformly_on', uniformCauchySeqOnFilter_of_deriv, uniformCauchySeqOnFilter_of_fderiv, uniformCauchySeqOn_ball_of_deriv, uniformCauchySeqOn_ball_of_fderiv	17
Total	17

UniformCauchySeqOnFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
one_smulRight 📖	mathematical	UniformCauchySeqOnFilter PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace ContinuousLinearMap.uniformSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.to_isUniformAddGroup ContinuousLinearMap.smulRight IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction IsBoundedSMul.continuousSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.one	—	SeminormedAddCommGroup.to_isUniformAddGroup IsScalarTower.left IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul RingHomIsometric.ids SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero Metric.tendstoUniformlyOnFilter_iff exists_between LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing GT.gt.lt Filter.Eventually.mono lt_of_le_of_lt dist_eq_norm zero_sub norm_neg ContinuousLinearMap.opNorm_le_bound LT.lt.le smul_sub norm_smul NormedSpace.toNormSMulClass mul_comm mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing le_of_lt norm_nonneg

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchy_map_of_uniformCauchySeqOn_fderiv 📖	—	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsPreconnected UniformCauchySeqOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.uniformSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.to_isUniformAddGroup HasFDerivAt Set Set.instMembership Cauchy Filter.map	—	—	SeminormedAddCommGroup.to_isUniformAddGroup cauchy_map_iff UniformCauchySeqOn.cauchy_map uniformCauchySeqOn_ball_of_fderiv UniformCauchySeqOn.mono Metric.isOpen_iff Nat.instAtLeastTwoHAddOfNat Metric.mem_closure_iff half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Metric.ball_subset_ball' dist_comm le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Nat.cast_one Mathlib.Tactic.Ring.one_mul 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_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_neg CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true CancelDenoms.add_subst HasSubset.Subset.trans Set.instIsTransSubset Metric.mem_ball IsPreconnected.subset_of_closure_inter_subset
difference_quotients_converge_uniformly 📖	mathematical	TendstoUniformlyOnFilter ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.uniformSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.to_isUniformAddGroup nhds Filter.Eventually HasFDerivAt DenselyNormedField.toNontriviallyNormedField SProd.sprod Filter Filter.instSProd Filter.Tendsto	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero RCLike.ofReal Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	SeminormedAddCommGroup.to_isUniformAddGroup UniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero Metric.tendstoUniformlyOnFilter_iff TendstoUniformlyOnFilter.uniformCauchySeqOnFilter exists_pos_rat_lt Real.instIsStrictOrderedRing Real.instArchimedean Filter.Eventually.diag_of_prod_right Filter.Tendsto.eventually Filter.tendsto_swap4_prod RingHomIsometric.ids Filter.eventually_prod_iff Filter.Eventually.and Filter.HasBasis.eventually_iff Metric.nhds_basis_ball Filter.eventually_mem_set Filter.HasBasis.mem_of_mem dist_zero_left smul_sub norm_smul NormedSpace.toNormSMulClass norm_inv RCLike.norm_coe_norm lt_of_le_of_lt sub_self norm_zero inv_zero MulZeroClass.mul_zero LT.lt.le norm_pos_iff eq_of_sub_eq_zero inv_mul_le_iff₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono mul_comm sub_sub_sub_comm Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le instIsRCLikeNormedField SeminormedAddCommGroup.toIsTopologicalAddGroup HasFDerivAt.hasFDerivWithinAt HasFDerivAt.sub convex_ball Metric.mem_ball_self Filter.Eventually.mono Filter.eventually_const nhds_neBot Filter.Eventually.self_of_nhds Filter.Tendsto.const_smul UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub
hasDerivAt_of_tendstoLocallyUniformlyOn 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField TendstoLocallyUniformlyOn SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Filter.Eventually Filter.Tendsto nhds Set Set.instMembership	HasDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule IsBoundedSMul.continuousSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing 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 Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsOpen.mem_nhds Filter.eventually_prod_iff hasDerivAt_of_tendstoUniformlyOnFilter IsOpen.nhdsWithin_eq tendstoLocallyUniformlyOn_iff_filter Filter.eventually_of_mem
hasDerivAt_of_tendstoUniformly 📖	mathematical	TendstoUniformly PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Filter.Eventually Filter.Tendsto nhds UniformSpace.toTopologicalSpace	HasDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField IsBoundedSMul.continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid 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 NormedSpace.toIsBoundedSMul	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Filter.mp_mem Filter.univ_mem' tendstoUniformlyOn_univ hasDerivAt_of_tendstoUniformlyOn isOpen_univ Set.mem_univ
hasDerivAt_of_tendstoUniformlyOn 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField TendstoUniformlyOn SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Filter.Eventually Filter.Tendsto nhds Set Set.instMembership	HasDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule IsBoundedSMul.continuousSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing 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 Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul hasDerivAt_of_tendstoLocallyUniformlyOn TendstoUniformlyOn.tendstoLocallyUniformlyOn
hasDerivAt_of_tendstoUniformlyOnFilter 📖	—	TendstoUniformlyOnFilter PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup nhds UniformSpace.toTopologicalSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Filter.Eventually HasDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule IsBoundedSMul.continuousSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing 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 Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul SProd.sprod Filter Filter.instSProd Filter.Tendsto	—	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsScalarTower.left SeminormedAddCommGroup.to_isUniformAddGroup RingHomIsometric.ids Metric.tendstoUniformlyOnFilter_iff exists_between LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing GT.gt.lt Filter.Eventually.mono lt_of_le_of_lt dist_eq_norm ContinuousLinearMap.opNorm_le_bound LT.lt.le smul_sub norm_smul NormedSpace.toNormSMulClass mul_comm mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing le_of_lt norm_nonneg hasFDerivAt_of_tendstoUniformlyOnFilter
hasDerivAt_of_tendsto_locally_uniformly_on' 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField TendstoLocallyUniformlyOn SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Filter.Eventually DifferentiableOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace Filter.Tendsto nhds Set Set.instMembership	HasDerivAt IsBoundedSMul.continuousSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing 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 Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul	—	hasDerivAt_of_tendstoLocallyUniformlyOn Filter.mp_mem IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Filter.univ_mem' DifferentiableAt.hasDerivAt DifferentiableWithinAt.differentiableAt IsOpen.mem_nhds
hasFDerivAt_of_tendstoLocallyUniformlyOn 📖	—	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup TendstoLocallyUniformlyOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.uniformSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.to_isUniformAddGroup HasFDerivAt Filter.Tendsto nhds Set Set.instMembership	—	—	SeminormedAddCommGroup.to_isUniformAddGroup IsOpen.mem_nhds nhds_neBot Filter.eventually_of_mem hasFDerivAt_of_tendstoUniformlyOnFilter IsOpen.nhdsWithin_eq tendstoLocallyUniformlyOn_iff_filter
hasFDerivAt_of_tendstoUniformly 📖	—	TendstoUniformly 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.uniformSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.to_isUniformAddGroup HasFDerivAt Filter.Tendsto nhds	—	—	SeminormedAddCommGroup.to_isUniformAddGroup tendstoUniformlyOn_univ hasFDerivAt_of_tendstoUniformlyOn isOpen_univ Set.mem_univ
hasFDerivAt_of_tendstoUniformlyOn 📖	—	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup TendstoUniformlyOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.uniformSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.to_isUniformAddGroup HasFDerivAt Filter.Tendsto nhds Set Set.instMembership	—	—	SeminormedAddCommGroup.to_isUniformAddGroup hasFDerivAt_of_tendstoLocallyUniformlyOn TendstoUniformlyOn.tendstoLocallyUniformlyOn
hasFDerivAt_of_tendstoUniformlyOnFilter 📖	—	TendstoUniformlyOnFilter 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.uniformSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.to_isUniformAddGroup nhds Filter.Eventually HasFDerivAt SProd.sprod Filter Filter.instSProd Filter.Tendsto	—	—	SeminormedAddCommGroup.to_isUniformAddGroup hasFDerivAt_iff_tendsto abs_norm abs_inv Real.instIsStrictOrderedRing RCLike.norm_ofReal RCLike.ofReal_inv norm_smul NormedSpace.toNormSMulClass tendsto_zero_iff_norm_tendsto_zero SeminormedAddCommGroup.toIsTopologicalAddGroup smul_add map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass sub_add_sub_cancel 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 add_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Abel.zero_termg Filter.Tendsto.add IsTopologicalAddGroup.toContinuousAdd difference_quotients_converge_uniformly Metric.tendsto_nhds Filter.Eventually.mono Filter.Eventually.filter_mono Filter.curry_le_prod Metric.tendstoUniformlyOnFilter_iff dist_eq_norm Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.sub_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.sub_eq_eval₁ Mathlib.Tactic.Module.NF.zero_sub_eq_eval AddCommGroup.intIsScalarTower Mathlib.Tactic.Module.NF.zero_eq_eval sub_zero Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Nat.cast_one eq_intCast Int.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Int.cast_neg Mathlib.Tactic.Ring.neg_congr 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.neg_mul Filter.eventually_curry_iff Filter.Eventually.curry Filter.Eventually.self_of_nhds norm_inv RCLike.norm_coe_norm norm_mul NormedDivisionRing.toNormMulClass norm_norm Filter.Tendsto.mono_left RingHomIsometric.ids dist_zero_right squeeze_zero_norm sub_self norm_zero inv_zero map_zero AddMonoidHomClass.toZeroHomClass MulZeroClass.mul_zero norm_pos_iff eq_of_sub_eq_zero inv_mul_le_iff₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono mul_comm norm_sub_rev ContinuousLinearMap.le_opNorm Filter.Tendsto.comp Filter.tendsto_fst Filter.Tendsto.prodMap Filter.tendsto_id Filter.eventually_const AddTorsor.nonempty
hasFDerivAt_of_tendsto_locally_uniformly_on' 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup TendstoLocallyUniformlyOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousLinearMap.uniformSpace SeminormedAddCommGroup.to_isUniformAddGroup fderiv DifferentiableOn NormedAddCommGroup.toAddCommGroup Filter.Tendsto nhds Set Set.instMembership	HasFDerivAt	—	SeminormedAddCommGroup.to_isUniformAddGroup hasFDerivAt_of_tendstoLocallyUniformlyOn DifferentiableAt.hasFDerivAt DifferentiableWithinAt.differentiableAt IsOpen.mem_nhds
uniformCauchySeqOnFilter_of_deriv 📖	—	UniformCauchySeqOnFilter PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup nhds UniformSpace.toTopologicalSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Filter.Eventually HasDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule IsBoundedSMul.continuousSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing 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 Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul SProd.sprod Filter Filter.instSProd Cauchy Filter.map	—	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul uniformCauchySeqOnFilter_of_fderiv IsScalarTower.left UniformCauchySeqOnFilter.one_smulRight
uniformCauchySeqOnFilter_of_fderiv 📖	—	UniformCauchySeqOnFilter 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.uniformSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.to_isUniformAddGroup nhds Filter.Eventually HasFDerivAt SProd.sprod Filter Filter.instSProd Cauchy Filter.map	—	—	SeminormedAddCommGroup.to_isUniformAddGroup SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero Metric.tendstoUniformlyOnFilter_iff Filter.Eventually.diag_of_prod_right Filter.Tendsto.eventually Filter.tendsto_swap4_prod RingHomIsometric.ids Filter.eventually_prod_iff Filter.Eventually.and Filter.HasBasis.eventually_iff Metric.nhds_basis_ball Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike lt_of_lt_of_le Metric.mem_ball min_le_right dist_eq_norm min_le_left mul_lt_iff_lt_one_right IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE GT.gt.lt Filter.eventually_mem_set Filter.HasBasis.mem_of_mem dist_zero_left lt_of_le_of_lt Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le SeminormedAddCommGroup.toIsTopologicalAddGroup HasFDerivAt.hasFDerivWithinAt HasFDerivAt.sub LT.lt.le convex_ball Metric.mem_ball_self Metric.cauchy_iff zero_sub neg_sub norm_sub_rev TendstoUniformlyOnFilter.add TendstoUniformlyOnFilter.congr add_zero sub_add_cancel
uniformCauchySeqOn_ball_of_deriv 📖	—	UniformCauchySeqOn PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Metric.ball SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField HasDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace IsBoundedSMul.continuousSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing 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 Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul Cauchy Filter.map	—	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.to_isUniformAddGroup IsScalarTower.left uniformCauchySeqOn_iff_uniformCauchySeqOnFilter UniformCauchySeqOnFilter.one_smulRight uniformCauchySeqOn_ball_of_fderiv
uniformCauchySeqOn_ball_of_fderiv 📖	—	UniformCauchySeqOn 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.uniformSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.to_isUniformAddGroup Metric.ball HasFDerivAt Cauchy Filter.map	—	—	SeminormedAddCommGroup.to_isUniformAddGroup cauchy_map_iff le_or_gt Metric.ball_eq_empty instIsEmptyFalse Filter.prod.instNeBot SeminormedAddGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_zero Metric.tendstoUniformlyOn_iff mul_comm exists_pos_mul_lt Real.instIsStrictOrderedRing GT.gt.lt Filter.Eventually.mono RingHomIsometric.ids LT.lt.gt dist_eq_norm zero_sub norm_neg Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le SeminormedAddCommGroup.toIsTopologicalAddGroup HasFDerivAt.hasFDerivWithinAt HasFDerivAt.sub LT.lt.le convex_ball Metric.mem_ball_self lt_of_le_of_lt mul_lt_mul' IsStrictOrderedRing.toPosMulStrictMono IsOrderedRing.toMulPosMono Real.instIsOrderedRing Eq.le Metric.mem_ball norm_nonneg LT.lt.trans Metric.cauchy_iff Filter.eventually_prod_iff Pi.zero_apply TendstoUniformlyOn.add TendstoUniformlyOn.congr add_zero Filter.univ_mem' sub_add_cancel

---

← Back to Index