ExistUnique

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

Statistics

Metric	Count
Definitions	0
Theorems periodic_of_eq, periodic_xor_injective, exists_isMIntegralCurveAt_of_contMDiffAt, exists_isMIntegralCurveAt_of_contMDiffAt_boundaryless, isMIntegralCurveAt_eventuallyEq_of_contMDiffAt, isMIntegralCurveAt_eventuallyEq_of_contMDiffAt_boundaryless, isMIntegralCurveOn_Ioo_eqOn_of_contMDiff, isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless, isMIntegralCurve_Ioo_eq_of_contMDiff_boundaryless, isMIntegralCurve_eq_of_contMDiff	10
Total	10

IsMIntegralCurve

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
periodic_of_eq 📖	mathematical	IsMIntegralCurve ContMDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	Function.Periodic Real.instAdd Real.instSub	—	isMIntegralCurve_Ioo_eq_of_contMDiff_boundaryless comp_add add_sub_cancel
periodic_xor_injective 📖	mathematical	IsMIntegralCurve ContMDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	Xor' Real.instLT Real.instZero Function.Periodic Real.instAdd	—	xor_iff_iff_not Function.Periodic.not_injective ne_of_gt Mathlib.Tactic.Push.not_forall_eq Function.Injective.eq_1 abs_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid sub_ne_zero abs_of_neg neg_sub periodic_of_eq abs_of_nonneg

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isMIntegralCurveAt_of_contMDiffAt 📖	mathematical	ContMDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ModelWithCorners.IsInteriorPoint	IsMIntegralCurveAt	—	contMDiffAt_iff IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt₀ ContDiffAt.snd ContDiffWithinAt.contDiffAt range_mem_nhds_isInteriorPoint Metric.eventually_nhds_iff_ball HasDerivAt.continuousAt Metric.mem_ball_self continuousAt_def IsOpen.mem_nhds isOpen_interior ModelWithCorners.isInteriorPoint_iff Filter.Eventually.exists_mem Filter.Eventually.and eventually_mem_nhds_iff PartialEquiv.left_inv mem_extChartAt_source isMIntegralCurveAt_iff Set.mem_preimage mem_of_mem_nhds Set.mem_of_mem_of_subset interior_subset PartialEquiv.target_subset_preimage_source HasMFDerivAt.hasMFDerivWithinAt ContinuousAt.comp continuousAt_extChartAt_symm'' tangentCoordChange_def HasDerivWithinAt.hasFDerivWithinAt HasDerivWithinAt.congr_simp PartialEquiv.trans_refl Set.range_id tangentCoordChange_self tangentCoordChange_comp HasFDerivAt.comp_hasDerivAt HasFDerivWithinAt.hasFDerivAt PartialEquiv.right_inv hasFDerivWithinAt_tangentCoordChange mem_nhds_iff subset_trans Set.instIsTransSubset extChartAt_target_subset_range
exists_isMIntegralCurveAt_of_contMDiffAt_boundaryless 📖	mathematical	ContMDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	IsMIntegralCurveAt	—	exists_isMIntegralCurveAt_of_contMDiffAt BoundarylessManifold.isInteriorPoint
isMIntegralCurveAt_eventuallyEq_of_contMDiffAt 📖	mathematical	ModelWithCorners.IsInteriorPoint Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ContMDiffAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat IsMIntegralCurveAt	Filter.EventuallyEq nhds Real.pseudoMetricSpace	—	contMDiffAt_iff ContDiffAt.exists_lipschitzOnWith ContDiffAt.snd ContDiffWithinAt.contDiffAt range_mem_nhds_isInteriorPoint eventually_mem_nhds_iff continuousAt_def IsMIntegralCurveAt.continuousAt extChartAt_source_mem_nhds Set.mem_preimage mem_of_mem_nhds IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Filter.Eventually.and Filter.Eventually.mono IsMIntegralCurveAt.eventually_hasDerivAt HasDerivAt.congr_deriv PartialEquiv.left_inv ContinuousAt.preimage_mem_nhds ContinuousAt.comp continuousAt_extChartAt ODE_solution_unique_of_eventually Filter.Eventually.of_forall Filter.EventuallyEq.trans Filter.EventuallyEq.fun_comp Filter.EventuallyEq.symm
isMIntegralCurveAt_eventuallyEq_of_contMDiffAt_boundaryless 📖	mathematical	ContMDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat IsMIntegralCurveAt	Filter.EventuallyEq nhds Real.pseudoMetricSpace	—	isMIntegralCurveAt_eventuallyEq_of_contMDiffAt BoundarylessManifold.isInteriorPoint
isMIntegralCurveOn_Ioo_eqOn_of_contMDiff 📖	mathematical	Real Set Set.instMembership Set.Ioo Real.instPreorder ModelWithCorners.IsInteriorPoint DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ContMDiff Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat IsMIntegralCurveOn	Set.EqOn	—	IsPreconnected.subset_of_closure_inter_subset isPreconnected_Ioo instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing isOpen_iff_mem_nhds Ioo_mem_nhds HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid isMIntegralCurveAt_eventuallyEq_of_contMDiffAt ContMDiff.contMDiffAt IsMIntegralCurveOn.isMIntegralCurveAt Filter.Eventually.mono Filter.Eventually.and Set.inter_comm Subtype.image_preimage_val Set.image_subset_image_iff Subtype.val_injective Set.preimage_setOf_eq IsClosed.closure_subset isClosed_eq continuous_iff_continuousAt ContinuousAt.comp ContinuousWithinAt.continuousAt IsMIntegralCurveOn.continuousWithinAt continuousAt_subtype_val closure_subtype Set.mem_preimage Set.mem_setOf Set.subset_def
isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless 📖	mathematical	Real Set Set.instMembership Set.Ioo Real.instPreorder ContMDiff DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat IsMIntegralCurveOn	Set.EqOn	—	isMIntegralCurveOn_Ioo_eqOn_of_contMDiff BoundarylessManifold.isInteriorPoint
isMIntegralCurve_Ioo_eq_of_contMDiff_boundaryless 📖	—	ContMDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat IsMIntegralCurve	—	—	isMIntegralCurve_eq_of_contMDiff BoundarylessManifold.isInteriorPoint
isMIntegralCurve_eq_of_contMDiff 📖	—	ModelWithCorners.IsInteriorPoint Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ContMDiff Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat IsMIntegralCurve	—	—	exists_abs_lt Real.instIsOrderedRing Real.instNontrivial abs_lt IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add 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.neg_congr Mathlib.Tactic.Ring.atom_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.sub_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt 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.add_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Ring.add_pf_add_zero isMIntegralCurveOn_Ioo_eqOn_of_contMDiff IsMIntegralCurveOn.mono IsMIntegralCurve.isMIntegralCurveOn Set.subset_univ

---

← Back to Index