Theorems · Theorem · real analysis

eVariationOn.eVariationOn_inter_Iio_eq_inter_Iic_of_continuousWithinAt

∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E} {s : Set α} {a : α},
  (nhdsWithin a (s ∩ Set.Iio a)).NeBot →
    ContinuousWithinAt f (s ∩ Set.Iic a) a → eVariationOn f (s ∩ Set.Iio a) = eVariationOn f (s ∩ Set.Iic a)

If a function is continuous on the left at a point a, then its variations on Iio a and on Iic a coincide. We give a version relative to a set s.

Defined in

Mathlib.Topology.EMetricSpace.BoundedVariation

Cited by

2 results in Mathlib

Foundations

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

Assumes

LinearOrderPseudoEMetricSpaceTopologicalSpaceOrderTopology