UniformTime

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

Statistics

Metric	Count
Definitions	0
Theorems eqOn_abs_add_one_of_isMIntegralCurveOn_Ioo, eqOn_of_isMIntegralCurveOn_Ioo, eqOn_piecewise_of_isMIntegralCurveOn_Ioo, exists_isMIntegralCurve_iff_exists_isMIntegralCurveOn_Ioo, exists_isMIntegralCurve_of_isMIntegralCurveOn, isMIntegralCurveOn_piecewise, isMIntegralCurve_abs_add_one_of_isMIntegralCurveOn_Ioo	7
Total	7

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqOn_abs_add_one_of_isMIntegralCurveOn_Ioo 📖	mathematical	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 Real.instZero IsMIntegralCurveOn Set.Ioo Real.instPreorder Real.instNeg	Set.EqOn Real.instAdd abs Real.lattice Real.instAddGroup Real.instOne	—	eqOn_of_isMIntegralCurveOn_Ioo Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid abs_nonneg Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one LT.lt.le abs_lt lt_add_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd neg_lt_self_iff lt_trans
eqOn_of_isMIntegralCurveOn_Ioo 📖	mathematical	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 Real.instZero IsMIntegralCurveOn Set.Ioo Real.instPreorder Real.instNeg Real.instLT Real.instLE	Set.EqOn	—	isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless Set.mem_Ioo neg_lt_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsMIntegralCurveOn.mono lt_of_lt_of_le Set.Ioo_subset_Ioo le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl 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.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.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero
eqOn_piecewise_of_isMIntegralCurveOn_Ioo 📖	mathematical	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 IsMIntegralCurveOn Set.Ioo Real.instPreorder Set Set.instMembership Set.instInter	Set.EqOn Set.piecewise Set.decidableMemIoo Preorder.toLT Real.decidableLT	—	isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless max_lt lt_min IsMIntegralCurveOn.mono Set.Ioo_subset_Ioo le_max_left min_le_left le_max_right min_le_right Set.piecewise.eq_1
exists_isMIntegralCurve_iff_exists_isMIntegralCurveOn_Ioo 📖	mathematical	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	Real.instZero IsMIntegralCurve IsMIntegralCurveOn Set.Ioo Real.instPreorder Real.instNeg	—	IsMIntegralCurve.isMIntegralCurveOn isMIntegralCurve_abs_add_one_of_isMIntegralCurveOn_Ioo
exists_isMIntegralCurve_of_isMIntegralCurveOn 📖	mathematical	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 Real.instLT Real.instZero IsMIntegralCurveOn Set.Ioo Real.instPreorder Real.instNeg	IsMIntegralCurve	—	Nat.instAtLeastTwoHAddOfNat Real.add_neg_lt_sSup neg_lt IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add neg_zero half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Set.mem_setOf neg_sub sub_add_sub_cancel sub_self le_csSup Set.piecewise.eq_1 lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero 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_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.neg_congr Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_gt 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.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le CancelDenoms.sub_subst CancelDenoms.neg_subst CancelDenoms.add_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 Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.add_neg sub_eq_add_neg IsMIntegralCurveOn.mono isMIntegralCurveOn_piecewise isMIntegralCurveOn_comp_add neg_lt_neg Mathlib.Meta.NormNum.isNat_add Set.Ioo_subset_Ioo_union_Ioo le_of_not_gt le_rfl Set.union_comm isMIntegralCurveOn_comp_sub not_lt lt_add_of_pos_right exists_isMIntegralCurve_iff_exists_isMIntegralCurveOn_Ioo not_bddAbove_iff Set.Ioo_subset_Ioo neg_le_neg LT.lt.le
isMIntegralCurveOn_piecewise 📖	mathematical	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 IsMIntegralCurveOn Set.Ioo Real.instPreorder Set Set.instMembership Set.instInter	Set.piecewise Set.decidableMemIoo Preorder.toLT Real.decidableLT Set.instUnion	—	Set.piecewise.eq_1 HasMFDerivWithinAt.congr_of_eventuallyEq HasMFDerivAt.hasMFDerivWithinAt HasMFDerivWithinAt.hasMFDerivAt Ioo_mem_nhds HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.eventuallyEq_iff_exists_mem IsOpen.nhdsWithin_eq IsOpen.union isOpen_Ioo Set.mem_union eqOn_piecewise_of_isMIntegralCurveOn_Ioo
isMIntegralCurve_abs_add_one_of_isMIntegralCurveOn_Ioo 📖	mathematical	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 Real.instZero IsMIntegralCurveOn Set.Ioo Real.instPreorder Real.instNeg	IsMIntegralCurve Real.instAdd abs Real.lattice Real.instAddGroup Real.instOne	—	Set.mem_Ioo abs_lt IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add lt_add_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd HasMFDerivAt.congr_of_eventuallyEq HasMFDerivWithinAt.hasMFDerivAt Right.add_pos_of_nonneg_of_pos abs_nonneg Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Ioo_mem_nhds HasSolidNorm.orderClosedTopology instHasSolidNormReal Filter.eventuallyEq_iff_exists_mem lt_add_of_pos_right zero_lt_one eqOn_abs_add_one_of_isMIntegralCurveOn_Ioo

---

← Back to Index