Theorems · Theorem · real analysis

HasConstantSpeedOnWith.union

∀ {E : Type u_2} [inst : PseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} {l : NNReal} {t : Set ℝ},
  HasConstantSpeedOnWith f s l →
    HasConstantSpeedOnWith f t l → ∀ {x : ℝ}, IsGreatest s x → IsLeast t x → HasConstantSpeedOnWith f (s ∪ t) l

Defined in: Mathlib.Analysis.ConstantSpeed
Cited by: 2 results in Mathlib
Foundations: Depth 155 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.

Cites30

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

Setstatement and proof · cited by 53,352
Realstatement and proof · cited by 25,697
ENNRealproof · cited by 9,879
NNRealstatement and proof · cited by 4,310
mul_oneproof · cited by 3,885
LE.le.transproof · cited by 3,151
add_zeroproof · cited by 2,707
Set.extproof · cited by 2,266
MulZeroClass.mul_zeroproof · cited by 2,091
le_antisymmproof · cited by 2,068
Set.Iccproof · cited by 1,702
le_rflproof · cited by 1,558

Cited by2

Results whose statement or proof uses this declaration.

HasConstantSpeedOnWith.Icc_Iccproof · cited by 1
HasUnitSpeedOn.unionproof · cited by 0