Theorems · Theorem · real analysis

eVariationOn.eVariationOn_on_inter_Iic_eq_Iio_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.Iio a)).NeBot →
    a ∈ s →
      Filter.Tendsto f (nhdsWithin a (s ∩ Set.Iio a)) (nhds l) →
        eVariationOn f (s ∩ Set.Iic a) = eVariationOn f (s ∩ Set.Iio a) + edist (f a) l

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

Defined in

Mathlib.Topology.EMetricSpace.BoundedVariation

Cited by

4 results in Mathlib

Foundations

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

Assumes

LinearOrderPseudoEMetricSpaceTopologicalSpaceOrderTopology