ConstantSpeed

📁 Source: Mathlib/Analysis/ConstantSpeed.lean

Statistics

Metric	Count
Definitions HasConstantSpeedOnWith, HasUnitSpeedOn, naturalParameterization	3
Theorems Icc_Icc, hasLocallyBoundedVariationOn, ratio, union, Icc_Icc, union, edist_naturalParameterization_eq_zero, hasConstantSpeedOnWith_iff_ordered, hasConstantSpeedOnWith_iff_variationOnFromTo_eq, hasConstantSpeedOnWith_of_subsingleton, hasConstantSpeedOnWith_zero_iff, has_unit_speed_naturalParameterization, unique_unit_speed, unique_unit_speed_on_Icc_zero	14
Total	17

HasConstantSpeedOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Icc_Icc 📖	—	HasConstantSpeedOnWith Set.Icc Real Real.instPreorder	—	—	le_total Set.Icc_union_Icc_eq_Icc union isGreatest_Icc isLeast_Icc Set.Icc_inter_Icc sup_of_le_right inf_of_le_right LE.le.trans
hasLocallyBoundedVariationOn 📖	mathematical	HasConstantSpeedOnWith	LocallyBoundedVariationOn Real Real.linearOrder	—	—
ratio 📖	mathematical	MonotoneOn Real Real.instPreorder HasConstantSpeedOnWith Set.image Set Set.instMembership	Set.EqOn Real.instAdd Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid NNReal.toReal Real.instSub	—	sub_eq_iff_eq_add mul_comm mul_div_assoc eq_div_iff NNReal.coe_ne_zero hasConstantSpeedOnWith_iff_variationOnFromTo_eq variationOnFromTo.comp_eq_of_monotoneOn
union 📖	mathematical	HasConstantSpeedOnWith IsGreatest Real Real.instLE IsLeast	Set Set.instUnion	—	hasConstantSpeedOnWith_iff_ordered Set.ext le_antisymm LE.le.trans eVariationOn.union le_rfl ENNReal.ofReal_add mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing Subtype.prop sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr 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.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right 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.add_pf_add_gt 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.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg mul_one add_zero Set.Icc_self sub_self MulZeroClass.mul_zero ENNReal.ofReal_zero eVariationOn.subsingleton

HasUnitSpeedOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Icc_Icc 📖	—	HasUnitSpeedOn Set.Icc Real Real.instPreorder	—	—	HasConstantSpeedOnWith.Icc_Icc
union 📖	mathematical	HasUnitSpeedOn IsGreatest Real Real.instLE IsLeast	Set Set.instUnion	—	HasConstantSpeedOnWith.union

(root)

Definitions

Name	Category	Theorems
HasConstantSpeedOnWith 📖	MathDef	4 math math: hasConstantSpeedOnWith_zero_iff, hasConstantSpeedOnWith_of_subsingleton, hasConstantSpeedOnWith_iff_ordered, hasConstantSpeedOnWith_iff_variationOnFromTo_eq
HasUnitSpeedOn 📖	MathDef	1 math math: has_unit_speed_naturalParameterization
naturalParameterization 📖	CompOp	2 math math: has_unit_speed_naturalParameterization, edist_naturalParameterization_eq_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
edist_naturalParameterization_eq_zero 📖	mathematical	LocallyBoundedVariationOn Set Set.instMembership	EDist.edist PseudoEMetricSpace.toEDist naturalParameterization variationOnFromTo ENNReal instZeroENNReal	—	Function.invFunOn_pos variationOnFromTo.edist_zero_of_eq_zero variationOnFromTo.eq_left_iff
hasConstantSpeedOnWith_iff_ordered 📖	mathematical	—	HasConstantSpeedOnWith eVariationOn Real Real.linearOrder Set Set.instInter Set.Icc Real.instPreorder ENNReal.ofReal Real.instMul NNReal.toReal Real.instSub	—	le_total eVariationOn.subsingleton le_antisymm LE.le.trans ENNReal.ofReal_of_nonpos mul_nonpos_of_nonneg_of_nonpos IsOrderedRing.toPosMulMono Real.instIsOrderedRing Subtype.prop sub_nonpos_of_le covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
hasConstantSpeedOnWith_iff_variationOnFromTo_eq 📖	mathematical	—	HasConstantSpeedOnWith LocallyBoundedVariationOn Real Real.linearOrder variationOnFromTo Real.instMul NNReal.toReal Real.instSub	—	HasConstantSpeedOnWith.hasLocallyBoundedVariationOn le_total variationOnFromTo.eq_of_le hasConstantSpeedOnWith_iff_ordered ENNReal.toReal_ofReal mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing Subtype.prop sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid variationOnFromTo.eq_of_ge Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr 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.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt ENNReal.ofReal_toReal
hasConstantSpeedOnWith_of_subsingleton 📖	mathematical	Set.Subsingleton Real	HasConstantSpeedOnWith	—	eVariationOn.subsingleton sub_self MulZeroClass.mul_zero ENNReal.ofReal_zero
hasConstantSpeedOnWith_zero_iff 📖	mathematical	—	HasConstantSpeedOnWith NNReal instZeroNNReal EDist.edist PseudoEMetricSpace.toEDist ENNReal instZeroENNReal	—	MulZeroClass.zero_mul ENNReal.ofReal_zero Mathlib.Tactic.Push.not_forall_eq le_total le_rfl PseudoEMetricSpace.edist_comm ENNReal.instCanonicallyOrderedAdd eVariationOn.mono Set.inter_subset_left
has_unit_speed_naturalParameterization 📖	mathematical	LocallyBoundedVariationOn Set Set.instMembership	HasUnitSpeedOn naturalParameterization Set.image Real variationOnFromTo	—	hasConstantSpeedOnWith_iff_ordered le_total NNReal.coe_one one_mul le_antisymm variationOnFromTo.monotoneOn sub_self ENNReal.ofReal_zero Set.Icc_self eVariationOn.subsingleton sub_eq_add_neg variationOnFromTo.eq_neg_swap neg_neg add_comm variationOnFromTo.add eVariationOn.comp_inter_Icc_eq_of_monotoneOn eVariationOn.eq_of_edist_zero_on edist_naturalParameterization_eq_zero variationOnFromTo.eq_of_le ENNReal.ofReal_toReal
unique_unit_speed 📖	mathematical	MonotoneOn Real Real.instPreorder HasUnitSpeedOn Set.image Set Set.instMembership	Set.EqOn Real.instAdd Real.instSub	—	div_self NeZero.charZero_one RCLike.charZero_rclike one_mul HasConstantSpeedOnWith.ratio one_ne_zero IsStrictOrderedRing.toCharZero NNReal.instIsStrictOrderedRing
unique_unit_speed_on_Icc_zero 📖	mathematical	Real Real.instLE Real.instZero MonotoneOn Real.instPreorder Set.Icc Set.image HasUnitSpeedOn	Set.EqOn	—	le_antisymm LE.le.trans_eq le_rfl Set.mapsTo_image Set.mem_Icc tsub_zero AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid add_zero unique_unit_speed

---

← Back to Index