PicardLindelof

📁 Source: Mathlib/Analysis/ODE/PicardLindelof.lean

Statistics

Metric	Count
Definitions IsPicardLindelof, FunSpace, compProj, instCoeFunForallElemRealIcc, instInhabited, instMetricSpace, next, toContinuousMap, toFun, picard	10
Theorems exists_eventually_eq_hasDerivAt, exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt, exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt₀, continuousOn, continuousOn_uncurry, exists_eq_forall_mem_Icc_eq_picard, exists_eq_forall_mem_Icc_hasDerivWithinAt, exists_eq_forall_mem_Icc_hasDerivWithinAt₀, exists_forall_mem_closedBall_eq_forall_mem_Icc_hasDerivWithinAt, exists_forall_mem_closedBall_eq_hasDerivWithinAt_continuousOn, exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith, lipschitzOnWith, mul_max_le, norm_le, of_contDiffAt_one, of_time_independent, compProj_apply, compProj_mem_closedBall, compProj_of_mem, compProj_val, continuous, continuousOn_comp_compProj, continuous_compProj, dist_comp_iterate_next_le, dist_iterate_iterate_next_le_of_lipschitzWith, dist_iterate_next_apply_le, dist_iterate_next_iterate_next_le, dist_iterate_next_le, dist_next_next, exists_contractingWith_iterate_next, exists_forall_closedBall_funSpace_dist_le_mul, exists_isFixedPt_next, instCompleteSpace, intervalIntegrable_comp_compProj, isUniformInducing_toContinuousMap, lipschitzWith, mem_closedBall, mem_closedBall₀, next_apply, next_apply₀, range_toContinuousMap, toContinuousMap_apply_eq_apply, contDiffOn_comp, contDiffOn_enat_Icc_of_hasDerivWithinAt, contDiffOn_enat_picard_Icc, contDiffOn_nat_picard_Icc, continuousOn_comp, hasDerivWithinAt_picard_Icc, picard_apply, picard_apply₀, picard_eq_of_hasDerivAt	51
Total	61

ContDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_eventually_eq_hasDerivAt 📖	mathematical	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	Filter.Eventually HasDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul SProd.sprod Filter Filter.instSProd nhds	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt Filter.eventually_iff_exists_mem Filter.prod_mem_prod_iff nhds_neBot Metric.closedBall_mem_nhds Ioo_mem_nhds HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid 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.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero 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_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Ring.add_pf_add_lt
exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt 📖	mathematical	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	Real.instLT Real.instZero HasDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul Real.pseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsPicardLindelof.of_contDiffAt_one IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt HasDerivWithinAt.hasDerivAt Set.Ioo_subset_Icc_self Icc_mem_nhds HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid
exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt₀ 📖	mathematical	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	Real.instLT Real.instZero HasDerivAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul Real.pseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt Metric.mem_closedBall_self le_of_lt

IsPicardLindelof

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn 📖	mathematical	IsPicardLindelof Set Set.instMembership Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NNReal.toReal	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc Real.instPreorder	—	—
continuousOn_uncurry 📖	mathematical	IsPicardLindelof	ContinuousOn Real instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SProd.sprod Set Set.instSProd Set.Icc Real.instPreorder Metric.closedBall NNReal.toReal	—	continuousOn_prod_of_continuousOn_lipschitzOnWith' lipschitzOnWith continuousOn
exists_eq_forall_mem_Icc_eq_picard 📖	mathematical	IsPicardLindelof Set Set.instMembership Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NNReal.toReal	Real Set.Icc Real.instPreorder ODE.picard	—	ODE.FunSpace.exists_isFixedPt_next le_trans Set.projIcc_val intervalIntegral.integral_same add_zero ODE.FunSpace.compProj_apply ODE.FunSpace.next_apply Set.projIcc_of_mem
exists_eq_forall_mem_Icc_hasDerivWithinAt 📖	mathematical	IsPicardLindelof Set Set.instMembership Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NNReal.toReal	Real Set.Icc Real.instPreorder HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ODE.FunSpace.exists_isFixedPt_next ODE.FunSpace.compProj_val ODE.FunSpace.next_apply₀ HasDerivWithinAt.congr_of_mem ODE.hasDerivWithinAt_picard_Icc continuousOn_uncurry Continuous.continuousOn ODE.FunSpace.continuous_compProj ODE.FunSpace.compProj_mem_closedBall mul_max_le ODE.FunSpace.compProj_of_mem ODE.FunSpace.next_apply
exists_eq_forall_mem_Icc_hasDerivWithinAt₀ 📖	mathematical	IsPicardLindelof NNReal instZeroNNReal	Real Set Set.instMembership Set.Icc Real.instPreorder HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul	—	exists_eq_forall_mem_Icc_hasDerivWithinAt Metric.mem_closedBall_self le_rfl
exists_forall_mem_closedBall_eq_forall_mem_Icc_hasDerivWithinAt 📖	mathematical	IsPicardLindelof	Real Set Set.instMembership Set.Icc Real.instPreorder HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith
exists_forall_mem_closedBall_eq_hasDerivWithinAt_continuousOn 📖	mathematical	IsPicardLindelof	Real Set Set.instMembership Set.Icc Real.instPreorder HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul ContinuousOn instTopologicalSpaceProd SProd.sprod Set.instSProd Metric.closedBall NNReal.toReal	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith continuousOn_prod_of_continuousOn_lipschitzOnWith HasDerivWithinAt.continuousOn
exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith 📖	mathematical	IsPicardLindelof	Real Set Set.instMembership Set.Icc Real.instPreorder HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul LipschitzOnWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Metric.closedBall NNReal.toReal	—	ODE.FunSpace.exists_isFixedPt_next IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ODE.FunSpace.compProj_val ODE.FunSpace.next_apply₀ le_trans ODE.FunSpace.compProj_apply HasDerivWithinAt.congr_of_mem ODE.hasDerivWithinAt_picard_Icc continuousOn_uncurry Continuous.continuousOn ODE.FunSpace.continuous_compProj ODE.FunSpace.compProj_mem_closedBall mul_max_le ODE.FunSpace.compProj_of_mem ODE.FunSpace.next_apply ODE.FunSpace.exists_forall_closedBall_funSpace_dist_le_mul LipschitzOnWith.of_dist_le_mul ODE.FunSpace.toContinuousMap_apply_eq_apply compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal ContinuousMap.dist_le_iff_of_nonempty
lipschitzOnWith 📖	mathematical	IsPicardLindelof Real Set Set.instMembership Set.Icc Real.instPreorder	LipschitzOnWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NNReal.toReal	—	—
mul_max_le 📖	mathematical	IsPicardLindelof	Real Real.instLE Real.instMul NNReal.toReal Real.instMax Real.instSub Set Set.instMembership Set.Icc Real.instPreorder	—	—
norm_le 📖	mathematical	IsPicardLindelof Real Set Set.instMembership Set.Icc Real.instPreorder Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NNReal.toReal	Real.instLE Norm.norm NormedAddCommGroup.toNorm	—	—
of_contDiffAt_one 📖	mathematical	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	IsPicardLindelof Real.instSub Real.instAdd Set Set.instMembership Set.Icc Real.instPreorder	—	ContDiffAt.exists_lipschitzOnWith Metric.mem_nhds_iff Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid add_nonneg mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing NNReal.coe_nonneg le_of_lt norm_nonneg Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Nat.instAtLeastTwoHAddOfNat norm_le_norm_sub_add add_le_add_left LipschitzOnWith.norm_sub_le subset_trans Set.instIsTransSubset Metric.closedBall_subset_ball half_lt_self PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing mem_of_mem_nhds mul_le_mul_of_nonneg_left mem_closedBall_iff_norm Metric.closedBall_subset_closedBall half_le_self le_add_of_nonneg_right zero_le_one Real.instZeroLEOneClass div_pos Mathlib.Meta.NormNum.instAtLeastTwo half_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono NNReal.instIsStrictOrderedRing of_time_independent LipschitzOnWith.mono add_sub_cancel_left sub_sub_cancel max_self Mathlib.Tactic.FieldSimp.le_eq_cancel_le PosMulStrictMono.toPosMulMono Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.cons_pos zero_lt_one NeZero.one GroupWithZero.toNontrivial Mathlib.Meta.NormNum.isNat_le_true Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt
of_time_independent 📖	mathematical	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm NNReal.toReal LipschitzOnWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instMul Real.instMax Real.instSub Set Set.instMembership Set.Icc Real.instPreorder	IsPicardLindelof	—	continuousOn_const

ODE

Definitions

Name	Category	Theorems
FunSpace 📖	CompData	11 math math: FunSpace.exists_contractingWith_iterate_next, FunSpace.isUniformInducing_toContinuousMap, FunSpace.range_toContinuousMap, FunSpace.dist_next_next, FunSpace.toContinuousMap_apply_eq_apply, FunSpace.exists_forall_closedBall_funSpace_dist_le_mul, FunSpace.dist_iterate_next_le, FunSpace.dist_iterate_next_iterate_next_le, FunSpace.instCompleteSpace, FunSpace.exists_isFixedPt_next, FunSpace.dist_iterate_next_apply_le
picard 📖	CompOp	6 math math: FunSpace.next_apply, IsPicardLindelof.exists_eq_forall_mem_Icc_eq_picard, hasDerivWithinAt_picard_Icc, picard_apply₀, picard_eq_of_hasDerivAt, picard_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffOn_comp 📖	—	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Real.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal SProd.sprod Set Set.instSProd Set.instMembership	—	—	ContDiffOn.comp ContDiffOn.prodMk contDiffOn_fun_id Set.mem_prod
contDiffOn_enat_Icc_of_hasDerivWithinAt 📖	—	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Real.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal WithTop.some ENat SProd.sprod Set Set.instSProd Set.Icc Real.instPreorder HasDerivWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul Set.MapsTo	—	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Nat.instAtLeastTwoHAddOfNat 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.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.neg_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add 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_pf_right Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Nat.cast_one 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.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_add Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing neg_eq_zero CancelDenoms.sub_subst CancelDenoms.div_subst CancelDenoms.add_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_eq sub_eq_zero_of_eq Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsRat.to_isNNRat Set.uIcc_subset_Icc picard_eq_of_hasDerivAt ContinuousOn.mono ContDiffOn.continuousOn Set.prod_subset_prod_left HasDerivWithinAt.mono Set.MapsTo.mono_left ContDiffOn.congr contDiffOn_enat_picard_Icc HasDerivWithinAt.continuousOn le_iff_lt_or_eq not_lt Set.notMem_empty Set.Icc_eq_empty not_le Set.Icc_self Set.eq_of_mem_singleton contDiffWithinAt_singleton
contDiffOn_enat_picard_Icc 📖	—	Real Set Set.instMembership Set.Icc Real.instPreorder ContDiffOn DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Real.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal WithTop.some ENat SProd.sprod Set.instSProd ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace picard	—	—	contDiffOn_infty contDiffOn_nat_picard_Icc
contDiffOn_nat_picard_Icc 📖	—	Real Set Set.instMembership Set.Icc Real.instPreorder ContDiffOn DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Real.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal WithTop ENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat SProd.sprod Set.instSProd ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace picard	—	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul hasDerivWithinAt_picard_Icc ContDiffOn.continuousOn Nat.cast_zero HasDerivWithinAt.continuousOn Nat.cast_add Nat.cast_one contDiffOn_succ_iff_derivWithin uniqueDiffOn_Icc HasDerivWithinAt.differentiableWithinAt instIsEmptyFalse ContDiffOn.congr contDiffOn_comp ContDiffOn.of_succ HasDerivWithinAt.derivWithin UniqueDiffOn.uniqueDiffWithinAt Set.Subsingleton.eq_singleton_of_mem Set.subsingleton_Icc_of_ge not_lt Set.eq_of_mem_singleton contDiffWithinAt_singleton
continuousOn_comp 📖	—	ContinuousOn Real instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SProd.sprod Set Set.instSProd Set.MapsTo	—	—	contDiffOn_zero contDiffOn_comp
hasDerivWithinAt_picard_Icc 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder ContinuousOn instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SProd.sprod Set.instSProd	HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField IsBoundedSMul.continuousSMul Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul picard	—	HasDerivWithinAt.const_add intervalIntegral.integral_hasDerivWithinAt_right ContinuousOn.intervalIntegrable Real.locallyFinite_volume ContinuousOn.mono continuousOn_comp Set.uIcc_of_gt Set.Icc_subset_Icc Set.uIcc_of_le intervalIntegral.FTCFilter.nhdsIcc ContinuousOn.stronglyMeasurableAtFilter_nhdsWithin BorelSpace.opensMeasurable Real.borelSpace PseudoEMetricSpace.pseudoMetrizableSpace secondCountableTopologyEither_of_left instSecondCountableTopologyReal measurableSet_Icc HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid
picard_apply 📖	mathematical	—	picard AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid intervalIntegral MeasureTheory.MeasureSpace.volume Real Real.measureSpace	—	—
picard_apply₀ 📖	mathematical	—	picard	—	intervalIntegral.integral_same add_zero
picard_eq_of_hasDerivAt 📖	mathematical	ContinuousOn Real instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SProd.sprod Set Set.instSProd Set.uIcc Real.lattice HasDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField IsBoundedSMul.continuousSMul Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul Set.MapsTo	picard	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul add_sub_cancel picard_apply intervalIntegral.integral_eq_sub_of_hasDeriv_right HasDerivWithinAt.continuousOn HasDerivAt.hasDerivWithinAt HasDerivWithinAt.hasDerivAt Set.Ioo_subset_Icc_self Icc_mem_nhds HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid ContinuousOn.intervalIntegrable Real.locallyFinite_volume continuousOn_comp

ODE.FunSpace

Definitions

Name	Category	Theorems
compProj 📖	CompOp	8 math math: next_apply, continuousOn_comp_compProj, compProj_of_mem, continuous_compProj, intervalIntegrable_comp_compProj, compProj_val, compProj_mem_closedBall, compProj_apply
instCoeFunForallElemRealIcc 📖	CompOp	—
instInhabited 📖	CompOp	—
instMetricSpace 📖	CompOp	8 math math: exists_contractingWith_iterate_next, isUniformInducing_toContinuousMap, dist_next_next, exists_forall_closedBall_funSpace_dist_le_mul, dist_iterate_next_le, dist_iterate_next_iterate_next_le, instCompleteSpace, dist_iterate_next_apply_le
next 📖	CompOp	8 math math: exists_contractingWith_iterate_next, next_apply, dist_next_next, next_apply₀, dist_iterate_next_le, dist_iterate_next_iterate_next_le, exists_isFixedPt_next, dist_iterate_next_apply_le
toContinuousMap 📖	CompOp	3 math math: isUniformInducing_toContinuousMap, range_toContinuousMap, toContinuousMap_apply_eq_apply
toFun 📖	CompOp	11 math math: next_apply, toContinuousMap_apply_eq_apply, next_apply₀, compProj_of_mem, mem_closedBall, continuous, compProj_val, mem_closedBall₀, dist_iterate_next_apply_le, lipschitzWith, compProj_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compProj_apply 📖	mathematical	—	compProj toFun Set.projIcc Real Real.linearOrder le_trans Real.instPreorder Set Set.instMembership Set.Icc Preorder.toLE	—	—
compProj_mem_closedBall 📖	mathematical	Real Real.instLE Real.instMul NNReal.toReal Real.instMax Real.instSub Set Set.instMembership Set.Icc Real.instPreorder	Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup compProj	—	le_trans compProj_apply mem_closedBall
compProj_of_mem 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder	compProj toFun	—	le_trans compProj_apply Set.projIcc_of_mem
compProj_val 📖	mathematical	—	compProj Real Set Set.instMembership Set.Icc Real.instPreorder toFun	—	le_trans Set.projIcc_val
continuous 📖	mathematical	—	Continuous Set.Elem Real Set.Icc Real.instPreorder instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toFun	—	LipschitzWith.continuous lipschitzWith
continuousOn_comp_compProj 📖	mathematical	IsPicardLindelof	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup compProj Set.Icc Real.instPreorder	—	ODE.continuousOn_comp continuousOn_prod_of_continuousOn_lipschitzOnWith' IsPicardLindelof.lipschitzOnWith IsPicardLindelof.continuousOn Continuous.continuousOn continuous_compProj mem_closedBall IsPicardLindelof.mul_max_le
continuous_compProj 📖	mathematical	—	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup compProj	—	Continuous.comp continuous continuous_projIcc instOrderTopologyReal
dist_comp_iterate_next_le 📖	—	IsPicardLindelof Set Set.instMembership Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NNReal.toReal Real Real.instLE Dist.dist PseudoMetricSpace.toDist toFun Nat.iterate ODE.FunSpace next Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid abs Real.lattice Real.instAddGroup Real.instSub Set.Icc Real.instPreorder Real.instNatCast Nat.factorial MetricSpace.toPseudoMetricSpace instMetricSpace	—	—	LipschitzOnWith.dist_le_mul IsPicardLindelof.lipschitzOnWith mem_closedBall IsPicardLindelof.mul_max_le pow_succ' mul_assoc mul_div_assoc mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing mul_pow NNReal.coe_nonneg
dist_iterate_iterate_next_le_of_lipschitzWith 📖	mathematical	IsPicardLindelof Set Set.instMembership Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NNReal.toReal LipschitzWith ODE.FunSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace instMetricSpace Nat.iterate next	Real Real.instLE Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Real.instMul Finset.sum Real.instAddCommMonoid Finset.range DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid Real.instMax Real.instSub Set.Icc Real.instPreorder Real.instNatCast Nat.factorial	—	Function.iterate_zero_apply Finset.mul_sum Finset.sum_mul dist_le_range_sum_of_dist_le Function.iterate_succ_apply le_trans LipschitzWith.dist_iterate_succ_le_geometric mul_assoc mul_comm mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing dist_iterate_next_le pow_nonneg IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono NNReal.coe_nonneg
dist_iterate_next_apply_le 📖	mathematical	IsPicardLindelof Set Set.instMembership Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NNReal.toReal	Real Real.instLE Dist.dist PseudoMetricSpace.toDist toFun Nat.iterate ODE.FunSpace next Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid abs Real.lattice Real.instAddGroup Real.instSub Set.Icc Real.instPreorder Real.instNatCast Nat.factorial MetricSpace.toPseudoMetricSpace instMetricSpace	—	pow_zero Nat.cast_one div_self NeZero.charZero_one RCLike.charZero_rclike one_mul ContinuousMap.dist_apply_le_dist compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal Function.iterate_succ_apply' dist_eq_norm next_apply ODE.picard_apply add_sub_add_left_eq_sub intervalIntegral.integral_sub intervalIntegrable_comp_compProj intervalIntegral.norm_intervalIntegral_eq MeasureTheory.norm_integral_le_of_norm_le Continuous.integrableOn_uIoc BorelSpace.opensMeasurable Real.borelSpace MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Continuous.comp' Continuous.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_id' continuous_const Continuous.div_const Continuous.pow Continuous.abs Real.instIsOrderedAddMonoid Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Filter.Eventually.mono MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_restrict_mem measurableSet_Ioc instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal subset_trans Set.instIsTransSubset Set.uIoc_subset_uIcc Set.uIcc_subset_Icc compProj_of_mem dist_comp_iterate_next_le le_of_abs_le intervalIntegral.abs_intervalIntegral_eq intervalIntegral.integral_mul_const intervalIntegral.integral_div intervalIntegral.integral_const_mul abs_mul Real.instIsOrderedRing abs_div Real.instIsStrictOrderedRing integral_pow_abs_sub_uIoc abs_pow abs_dist NNReal.abs_eq abs_abs IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add mul_div div_div Nat.cast_succ Nat.cast_mul Nat.factorial_succ Nat.abs_cast mul_pow le_refl
dist_iterate_next_iterate_next_le 📖	mathematical	IsPicardLindelof Set Set.instMembership Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NNReal.toReal	Real Real.instLE Dist.dist ODE.FunSpace PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace instMetricSpace Nat.iterate next Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid Real.instMax Real.instSub Set.Icc Real.instPreorder Real.instNatCast Nat.factorial	—	compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal Function.Embedding.injective Isometry.dist_eq MetricSpace.isometry_induced ContinuousMap.dist_le le_max_of_le_left sub_nonneg_of_le covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing pow_nonneg IsOrderedRing.toZeroLEOneClass NNReal.coe_nonneg Nat.cast_pos' Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Nat.factorial_pos dist_nonneg le_trans dist_iterate_next_apply_le mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono pow_le_pow_left₀ abs_nonneg mul_le_mul_of_nonneg_left abs_sub_le_max_sub le_of_lt
dist_iterate_next_le 📖	mathematical	IsPicardLindelof Set Set.instMembership Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NNReal.toReal	Real Real.instLE Dist.dist ODE.FunSpace PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace instMetricSpace Nat.iterate next Real.instMul Finset.sum Real.instAddCommMonoid Finset.range DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid Real.instMax Real.instSub Set.Icc Real.instPreorder Real.instNatCast Nat.factorial	—	Function.iterate_zero_apply Finset.sum_mul dist_le_range_sum_of_dist_le Function.iterate_succ_apply dist_iterate_next_iterate_next_le
dist_next_next 📖	mathematical	IsPicardLindelof Set Set.instMembership Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NNReal.toReal	Dist.dist ODE.FunSpace PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace instMetricSpace next	—	compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal Function.Embedding.injective Isometry.dist_eq MetricSpace.isometry_induced dist_eq_norm ContinuousMap.norm_eq_iSup_norm add_sub_add_right_eq_sub le_trans ciSup_const
exists_contractingWith_iterate_next 📖	mathematical	IsPicardLindelof	ContractingWith ODE.FunSpace MetricSpace.toEMetricSpace instMetricSpace Nat.iterate next	—	Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.eventually FloorSemiring.tendsto_pow_div_factorial_atTop Real.instIsStrictOrderedRing instOrderTopologyReal gt_mem_nhds zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike le_max_of_le_left sub_nonneg_of_le covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono pow_nonneg IsOrderedRing.toZeroLEOneClass Real.instIsOrderedRing IsOrderedRing.toPosMulMono mul_nonneg NNReal.coe_nonneg Nat.cast_pos' Nat.factorial_pos LipschitzWith.of_dist_le_mul dist_iterate_next_iterate_next_le
exists_forall_closedBall_funSpace_dist_le_mul 📖	mathematical	IsPicardLindelof	Real Real.instLE Dist.dist ODE.FunSpace PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace instMetricSpace Real.instMul NNReal.toReal SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	exists_contractingWith_iterate_next le_max_of_le_left sub_nonneg_of_le covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing Finset.sum_nonneg Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing pow_nonneg IsOrderedRing.toZeroLEOneClass NNReal.coe_nonneg Nat.cast_pos' Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Nat.factorial_pos le_of_tendsto_of_tendsto' HasSolidNorm.orderClosedTopology instHasSolidNormReal Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.comp Filter.Tendsto.dist tendsto_const_nhds Filter.tendsto_id instCompleteSpace ContractingWith.fixedPoint_unique Function.IsFixedPt.iterate ContractingWith.tendsto_iterate_fixedPoint dist_next_next Filter.Tendsto.mul_const IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.Tendsto.const_mul Finset.sum_congr NNReal.coe_sub le_of_lt HasSum.tendsto_sum_nat hasSum_geometric_of_lt_one dist_iterate_iterate_next_le_of_lipschitzWith
exists_isFixedPt_next 📖	mathematical	IsPicardLindelof Set Set.instMembership Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NNReal.toReal	Function.IsFixedPt ODE.FunSpace next	—	exists_contractingWith_iterate_next instCompleteSpace ContractingWith.isFixedPt_fixedPoint_iterate
instCompleteSpace 📖	mathematical	—	CompleteSpace ODE.FunSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace instMetricSpace	—	completeSpace_iff_isComplete_range isUniformInducing_toContinuousMap IsClosed.isComplete ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace CompactlyCoherentSpace.of_sequentialSpace FrechetUrysohnSpace.to_sequentialSpace Subtype.instFrechetUrysohnSpace FirstCountableTopology.frechetUrysohnSpace TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace range_toContinuousMap Set.setOf_and IsClosed.inter IsClosed.preimage continuous_coeFun ContinuousMap.instContinuousEvalConst isClosed_setOf_lipschitzWith isClosed_le HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Continuous.norm Continuous.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup Continuous.eval_const continuous_id' continuous_const
intervalIntegrable_comp_compProj 📖	mathematical	IsPicardLindelof	IntervalIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup compProj MeasureTheory.MeasureSpace.volume Real Real.measureSpace Set Set.instMembership Set.Icc Real.instPreorder	—	ContinuousOn.intervalIntegrable Real.locallyFinite_volume ContinuousOn.mono continuousOn_comp_compProj Set.uIcc_subset_Icc
isUniformInducing_toContinuousMap 📖	mathematical	—	IsUniformInducing ODE.FunSpace ContinuousMap Set.Elem Real Set.Icc Real.instPreorder instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MetricSpace.toPseudoMetricSpace instMetricSpace ContinuousMap.compactConvergenceUniformSpace DFunLike.coe Function.Embedding Function.instFunLikeEmbedding toContinuousMap	—	—
lipschitzWith 📖	mathematical	—	LipschitzWith Set.Elem Real Set.Icc Real.instPreorder instPseudoEMetricSpaceSubtype Set Set.instMembership EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Real.metricSpace NormedAddCommGroup.toMetricSpace toFun	—	—
mem_closedBall 📖	mathematical	Real Real.instLE Real.instMul NNReal.toReal Real.instMax Real.instSub Set Set.instMembership Set.Icc Real.instPreorder	Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toFun	—	Metric.mem_closedBall dist_eq_norm norm_sub_le_norm_sub_add_norm_sub add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add LipschitzWith.dist_le_mul lipschitzWith mem_closedBall_iff_norm mem_closedBall₀ add_le_add_left mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing abs_sub_le_max_sub NNReal.coe_nonneg sub_add_cancel
mem_closedBall₀ 📖	mathematical	—	Set Set.instMembership Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NNReal.toReal toFun	—	—
next_apply 📖	mathematical	IsPicardLindelof Set Set.instMembership Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NNReal.toReal	toFun next ODE.picard Real Set.Icc Real.instPreorder compProj	—	—
next_apply₀ 📖	mathematical	IsPicardLindelof Set Set.instMembership Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NNReal.toReal	toFun next	—	intervalIntegral.integral_same le_trans add_zero
range_toContinuousMap 📖	mathematical	—	Set.range ContinuousMap Set.Elem Real Set.Icc Real.instPreorder instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ODE.FunSpace DFunLike.coe Function.Embedding Function.instFunLikeEmbedding toContinuousMap setOf LipschitzWith instPseudoEMetricSpaceSubtype EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Real.metricSpace NormedAddCommGroup.toMetricSpace ContinuousMap.instFunLike Metric.closedBall NNReal.toReal	—	Set.ext
toContinuousMap_apply_eq_apply 📖	mathematical	—	DFunLike.coe ContinuousMap Set.Elem Real Set.Icc Real.instPreorder instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ContinuousMap.instFunLike Function.Embedding ODE.FunSpace Function.instFunLikeEmbedding toContinuousMap toFun	—	—

(root)

Definitions

Name	Category	Theorems
IsPicardLindelof 📖	CompData	2 math math: IsPicardLindelof.of_contDiffAt_one, IsPicardLindelof.of_time_independent

---

← Back to Index