Theorems · Theorem · real analysis

eVariationOn.Icc_add_Icc

∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {s : Set α}
  {a b c : α},
  a ≤ b →
    b ≤ c →
      b ∈ s → eVariationOn f (s ∩ Set.Icc a b) + eVariationOn f (s ∩ Set.Icc b c) = eVariationOn f (s ∩ Set.Icc a c)

Defined in

Mathlib.Topology.EMetricSpace.BoundedVariation

Cited by

2 results in Mathlib

Foundations

Depth 155 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderPseudoEMetricSpace