Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `IsIntegralCurve`, `IsIntegralCurveAt`, `IsIntegralCurveOn`	3
Theorems `continuous`, `isIntegralCurveAt`, `isIntegralCurveOn`, `continuousAt`, `hasDerivAt`, `isIntegralCurveOn`, `continuousOn`, `continuousWithinAt`, `isIntegralCurveAt`, `mono`, `isIntegralCurveAt_iff_exists_mem_nhds`, `isIntegralCurveAt_iff_exists_pos`, `isIntegralCurveOn_iff_isIntegralCurveAt`, `isIntegralCurveOn_univ`, `isIntegralCurve_iff_isIntegralCurveAt`	15
Total	18

IsIntegralCurve

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous` 📖	mathematical	`IsIntegralCurve`	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`continuous_iff_continuousAt` `IsIntegralCurveAt.continuousAt` `isIntegralCurveAt`
`isIntegralCurveAt` 📖	mathematical	`IsIntegralCurve`	`IsIntegralCurveAt`	—	`isIntegralCurveAt_iff_exists_mem_nhds` `Filter.univ_mem` `HasDerivAt.hasDerivWithinAt`
`isIntegralCurveOn` 📖	mathematical	`IsIntegralCurve`	`IsIntegralCurveOn`	—	`HasDerivAt.hasDerivWithinAt`

IsIntegralCurveAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt` 📖	mathematical	`IsIntegralCurveAt`	`ContinuousAt` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`isIntegralCurveAt_iff_exists_mem_nhds` `ContinuousWithinAt.continuousAt` `IsIntegralCurveOn.continuousWithinAt` `mem_of_mem_nhds`
`hasDerivAt` 📖	mathematical	`IsIntegralCurveAt`	`HasDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsBoundedSMul.continuousSMul` `Real.pseudoMetricSpace` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul`	—	`IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `isIntegralCurveAt_iff_exists_mem_nhds` `HasDerivWithinAt.hasDerivAt` `mem_of_mem_nhds`
`isIntegralCurveOn` 📖	mathematical	`IsIntegralCurveAt`	`IsIntegralCurveOn`	—	`Filter.eventually_iff_exists_mem` `HasDerivAt.hasDerivWithinAt` `mem_of_mem_nhds`

IsIntegralCurveOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousOn` 📖	mathematical	`IsIntegralCurveOn`	`ContinuousOn` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`HasDerivWithinAt.continuousWithinAt`
`continuousWithinAt` 📖	mathematical	`IsIntegralCurveOn` `Real` `Set` `Set.instMembership`	`ContinuousWithinAt` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`HasDerivWithinAt.continuousWithinAt`
`isIntegralCurveAt` 📖	mathematical	`IsIntegralCurveOn` `Set` `Real` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`IsIntegralCurveAt`	—	`isIntegralCurveAt_iff_exists_mem_nhds`
`mono` 📖	mathematical	`IsIntegralCurveOn` `Set` `Real` `Set.instHasSubset`	`IsIntegralCurveOn`	—	`HasDerivWithinAt.mono`

(root)

Definitions

Name	Category	Theorems
`IsIntegralCurve` 📖	MathDef	9 math math: `IsIntegralCurve.comp_mul`, `IsIntegralCurve.comp_add`, `isIntegralCurve_comp_sub`, `isIntegralCurve_comp_add`, `isIntegralCurveOn_univ`, `IsIntegralCurve.comp_sub`, `isIntegralCurve_comp_mul_ne_zero`, `isIntegralCurve_const`, `isIntegralCurve_iff_isIntegralCurveAt`
`IsIntegralCurveAt` 📖	MathDef	12 math math: `isIntegralCurveAt_comp_mul_ne_zero`, `IsIntegralCurveAt.comp_sub`, `isIntegralCurveAt_iff_exists_pos`, `IsIntegralCurve.isIntegralCurveAt`, `IsIntegralCurveOn.isIntegralCurveAt`, `isIntegralCurveAt_iff_exists_mem_nhds`, `isIntegralCurveAt_comp_sub`, `IsIntegralCurveAt.comp_mul_ne_zero`, `isIntegralCurveOn_iff_isIntegralCurveAt`, `IsIntegralCurveAt.comp_add`, `isIntegralCurve_iff_isIntegralCurveAt`, `isIntegralCurveAt_comp_add`
`IsIntegralCurveOn` 📖	MathDef	13 math math: `isIntegralCurveOn_comp_add`, `IsIntegralCurveOn.comp_mul`, `IsIntegralCurveOn.comp_add`, `IsIntegralCurve.isIntegralCurveOn`, `IsIntegralCurveOn.comp_sub`, `isIntegralCurveAt_iff_exists_pos`, `IsIntegralCurveAt.isIntegralCurveOn`, `isIntegralCurveOn_comp_mul_ne_zero`, `IsIntegralCurveOn.mono`, `isIntegralCurveOn_univ`, `isIntegralCurveAt_iff_exists_mem_nhds`, `isIntegralCurveOn_comp_sub`, `isIntegralCurveOn_iff_isIntegralCurveAt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIntegralCurveAt_iff_exists_mem_nhds` 📖	mathematical	—	`IsIntegralCurveAt` `Set` `Real` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IsIntegralCurveOn`	—	`IsIntegralCurveAt.eq_1` `Filter.eventually_iff_exists_mem` `HasDerivAt.hasDerivWithinAt` `mem_nhds_iff` `IsOpen.mem_nhds` `HasDerivWithinAt.hasDerivAt`
`isIntegralCurveAt_iff_exists_pos` 📖	mathematical	—	`IsIntegralCurveAt` `Real` `Real.instLT` `Real.instZero` `IsIntegralCurveOn` `Metric.ball` `Real.pseudoMetricSpace`	—	`IsIntegralCurveAt.eq_1` `Metric.eventually_nhds_iff_ball` `HasDerivAt.hasDerivWithinAt` `HasDerivWithinAt.hasDerivAt` `IsOpen.mem_nhds` `Metric.isOpen_ball`
`isIntegralCurveOn_iff_isIntegralCurveAt` 📖	mathematical	`IsOpen` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`IsIntegralCurveOn` `IsIntegralCurveAt`	—	`IsIntegralCurveOn.isIntegralCurveAt` `IsOpen.mem_nhds` `IsIntegralCurveAt.isIntegralCurveOn`
`isIntegralCurveOn_univ` 📖	mathematical	—	`IsIntegralCurveOn` `Set.univ` `Real` `IsIntegralCurve`	—	`HasDerivWithinAt.hasDerivAt` `Set.mem_univ` `Filter.univ_mem` `IsIntegralCurve.isIntegralCurveOn`
`isIntegralCurve_iff_isIntegralCurveAt` 📖	mathematical	—	`IsIntegralCurve` `IsIntegralCurveAt`	—	`IsIntegralCurve.isIntegralCurveAt` `isIntegralCurveAt_iff_exists_mem_nhds` `HasDerivWithinAt.hasDerivAt` `mem_of_mem_nhds`

---

← Back to Index