Theorems · Theorem · real analysis

HasConstantSpeedOnWith.Icc_Icc

∀ {E : Type u_2} [inst : PseudoEMetricSpace E] {f : ℝ → E} {l : NNReal} {x y z : ℝ},
  HasConstantSpeedOnWith f (Set.Icc x y) l →
    HasConstantSpeedOnWith f (Set.Icc y z) l → HasConstantSpeedOnWith f (Set.Icc x z) l

Defined in: Mathlib.Analysis.ConstantSpeed
Cited by: 1 results in Mathlib
Foundations: Depth 156 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: PseudoEMetricSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites19

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setproof · cited by 53,352
Realstatement and proof · cited by 25,697
ENNRealproof · cited by 9,879
NNRealstatement and proof · cited by 4,310
LE.le.transproof · cited by 3,151
Set.Iccstatement and proof · cited by 1,702
PseudoEMetricSpacestatement and proof · cited by 1,536
NNReal.toRealproof · cited by 1,260
ENNReal.ofRealproof · cited by 863
le_totalproof · cited by 294
sup_of_le_rightproof · cited by 143
inf_of_le_rightproof · cited by 128

Cited by1

Results whose statement or proof uses this declaration.

HasUnitSpeedOn.Icc_Iccproof · cited by 0