Basic

📁 Source: Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean

Statistics

Metric	Count
Definitions IsMIntegralCurve, IsMIntegralCurveAt, IsMIntegralCurveOn	3
Theorems continuous, isMIntegralCurveAt, isMIntegralCurveOn, continuousAt, eventually_hasDerivAt, hasMFDerivAt, isMIntegralCurveOn, continuousOn, continuousWithinAt, hasDerivWithinAt, isMIntegralCurveAt, mono, isMIntegralCurveAt_iff, isMIntegralCurveAt_iff', isMIntegralCurveOn_iff_isMIntegralCurveAt, isMIntegralCurve_iff_isMIntegralCurveAt, isMIntegralCurve_iff_isMIntegralCurveOn	17
Total	20

IsMIntegralCurve

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous 📖	mathematical	IsMIntegralCurve	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	continuous_iff_continuousAt IsMIntegralCurveAt.continuousAt isMIntegralCurveAt
isMIntegralCurveAt 📖	mathematical	IsMIntegralCurve	IsMIntegralCurveAt	—	isMIntegralCurveAt_iff Filter.univ_mem HasMFDerivAt.hasMFDerivWithinAt
isMIntegralCurveOn 📖	mathematical	IsMIntegralCurve	IsMIntegralCurveOn	—	HasMFDerivAt.hasMFDerivWithinAt

IsMIntegralCurveAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousAt 📖	mathematical	IsMIntegralCurveAt	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	isMIntegralCurveAt_iff ContinuousWithinAt.continuousAt IsMIntegralCurveOn.continuousWithinAt mem_of_mem_nhds
eventually_hasDerivAt 📖	mathematical	IsMIntegralCurveAt	Filter.Eventually Real HasDerivAt 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 PartialEquiv.toFun extChartAt DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.funLike tangentCoordChange nhds	—	Filter.Eventually.mono IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Filter.Eventually.and eventually_mem_nhds_iff ContinuousAt.preimage_mem_nhds continuousAt extChartAt_source_mem_nhds mem_of_mem_nhds hasDerivAt_iff_hasFDerivAt hasMFDerivAt_iff_hasFDerivAt HasMFDerivAt.congr_mfderiv RingHomCompTriple.ids HasMFDerivAt.comp hasMFDerivAt_extChartAt extChartAt_source Set.mem_preimage ContinuousLinearMap.ext_iff ContinuousLinearMap.comp_apply ContinuousLinearMap.smulRight_apply map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass ContinuousLinearMap.one_apply IsScalarTower.left mfderiv_chartAt_eq_tangentCoordChange
hasMFDerivAt 📖	mathematical	IsMIntegralCurveAt	HasMFDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf Real.pseudoMetricSpace chartedSpaceSelf ContinuousLinearMap.smulRight Real.instAddCommMonoid TangentSpace instTopologicalSpaceTangentSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.semiring NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing instModuleTangentSpace IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction instContinuousSMulTangentSpace ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.one	—	IsScalarTower.left isMIntegralCurveAt_iff HasMFDerivWithinAt.hasMFDerivAt mem_of_mem_nhds
isMIntegralCurveOn 📖	mathematical	IsMIntegralCurveAt	IsMIntegralCurveOn	—	HasMFDerivAt.hasMFDerivWithinAt Filter.eventually_iff_exists_mem mem_of_mem_nhds

IsMIntegralCurveOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn 📖	mathematical	IsMIntegralCurveOn	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	HasMFDerivWithinAt.continuousWithinAt
continuousWithinAt 📖	mathematical	IsMIntegralCurveOn Real Set Set.instMembership	ContinuousWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	—
hasDerivWithinAt 📖	mathematical	IsMIntegralCurveOn Real Set Set.instMembership PartialEquiv.source extChartAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	HasDerivWithinAt 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 PartialEquiv.toFun DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.funLike tangentCoordChange	—	extChartAt_source IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul hasDerivWithinAt_iff_hasFDerivWithinAt hasMFDerivWithinAt_iff_hasFDerivWithinAt HasMFDerivWithinAt.congr_mfderiv RingHomCompTriple.ids HasMFDerivWithinAt.comp hasMFDerivWithinAt_extChartAt Set.subset_preimage_image ContinuousLinearMap.ext_iff ContinuousLinearMap.comp_apply ContinuousLinearMap.smulRight_apply map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass ContinuousLinearMap.one_apply IsScalarTower.left mfderiv_chartAt_eq_tangentCoordChange
isMIntegralCurveAt 📖	mathematical	IsMIntegralCurveOn Set Real Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	IsMIntegralCurveAt	—	isMIntegralCurveAt_iff
mono 📖	—	IsMIntegralCurveOn Set Real Set.instHasSubset	—	—	HasMFDerivWithinAt.mono

(root)

Definitions

Name	Category	Theorems
IsMIntegralCurve 📖	MathDef	9 math math: isMIntegralCurve_comp_add, isMIntegralCurve_comp_sub, isMIntegralCurve_const, isMIntegralCurve_iff_isMIntegralCurveOn, isMIntegralCurve_abs_add_one_of_isMIntegralCurveOn_Ioo, isMIntegralCurve_iff_isMIntegralCurveAt, exists_isMIntegralCurve_of_isMIntegralCurveOn, exists_isMIntegralCurve_iff_exists_isMIntegralCurveOn_Ioo, isMIntegralCurve_comp_mul_ne_zero
IsMIntegralCurveAt 📖	MathDef	11 math math: IsMIntegralCurveOn.isMIntegralCurveAt, exists_isMIntegralCurveAt_of_contMDiffAt_boundaryless, isMIntegralCurveOn_iff_isMIntegralCurveAt, isMIntegralCurveAt_iff, exists_isMIntegralCurveAt_of_contMDiffAt, isMIntegralCurveAt_comp_mul_ne_zero, isMIntegralCurveAt_comp_sub, isMIntegralCurveAt_comp_add, isMIntegralCurve_iff_isMIntegralCurveAt, isMIntegralCurveAt_iff', IsMIntegralCurve.isMIntegralCurveAt
IsMIntegralCurveOn 📖	MathDef	10 math math: isMIntegralCurveOn_iff_isMIntegralCurveAt, isMIntegralCurveOn_comp_add, isMIntegralCurveOn_comp_sub, isMIntegralCurveAt_iff, IsMIntegralCurve.isMIntegralCurveOn, isMIntegralCurve_iff_isMIntegralCurveOn, isMIntegralCurveOn_comp_mul_ne_zero, isMIntegralCurveAt_iff', exists_isMIntegralCurve_iff_exists_isMIntegralCurveOn_Ioo, IsMIntegralCurveAt.isMIntegralCurveOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isMIntegralCurveAt_iff 📖	mathematical	—	IsMIntegralCurveAt Set Real Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace IsMIntegralCurveOn	—	Filter.eventually_iff_exists_mem IsMIntegralCurveAt.eq_1 HasMFDerivAt.hasMFDerivWithinAt mem_nhds_iff IsOpen.mem_nhds HasMFDerivWithinAt.hasMFDerivAt
isMIntegralCurveAt_iff' 📖	mathematical	—	IsMIntegralCurveAt Real Real.instLT Real.instZero IsMIntegralCurveOn Metric.ball Real.pseudoMetricSpace	—	isMIntegralCurveAt_iff Metric.mem_nhds_iff HasMFDerivWithinAt.mono Metric.ball_mem_nhds
isMIntegralCurveOn_iff_isMIntegralCurveAt 📖	mathematical	IsOpen Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	IsMIntegralCurveOn IsMIntegralCurveAt	—	IsMIntegralCurveOn.isMIntegralCurveAt IsOpen.mem_nhds IsMIntegralCurveAt.isMIntegralCurveOn
isMIntegralCurve_iff_isMIntegralCurveAt 📖	mathematical	—	IsMIntegralCurve IsMIntegralCurveAt	—	IsMIntegralCurve.isMIntegralCurveAt isMIntegralCurveAt_iff HasMFDerivWithinAt.hasMFDerivAt mem_of_mem_nhds
isMIntegralCurve_iff_isMIntegralCurveOn 📖	mathematical	—	IsMIntegralCurve IsMIntegralCurveOn Set.univ Real	—	IsMIntegralCurve.isMIntegralCurveOn HasMFDerivWithinAt.hasMFDerivAt Set.mem_univ Filter.univ_mem

---

← Back to Index