Theorems · Theorem · real analysis

eVariationOn.eVariationOn_on_inter_Ici_eq_Ioi_add_edist

∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E} {s : Set α} {a : α} {l : E},
  (nhdsWithin a (s ∩ Set.Ioi a)).NeBot →
    a ∈ s →
      Filter.Tendsto f (nhdsWithin a (s ∩ Set.Ioi a)) (nhds l) →
        eVariationOn f (s ∩ Set.Ici a) = eVariationOn f (s ∩ Set.Ioi a) + edist (f a) l

The variation of a function on Ici a is the sum of the variation on Ioi a and the contribution of a, i.e., the distance between the right limit and the value at a. We give a version relative to a set s.

Defined in

Mathlib.Topology.EMetricSpace.BoundedVariation

Cited by

0 results in Mathlib

Foundations

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

Assumes

LinearOrderPseudoEMetricSpaceTopologicalSpaceOrderTopology