Theorems · Theorem · real analysis

variationOnFromTo.tendsto_right

∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {E : Type u_3} [inst_1 : PseudoMetricSpace E]
  [inst_2 : TopologicalSpace α] [OrderTopology α] {f : α → E} {l : E} {a b : α},
  a ∈ s →
    b ∈ s →
      LocallyBoundedVariationOn f s →
        Filter.Tendsto f (nhdsWithin b (s ∩ Set.Ioi b)) (nhds l) →
          Filter.Tendsto (variationOnFromTo f s a) (nhdsWithin b (s ∩ Set.Ioi b))
            (nhds (variationOnFromTo f s a b + dist (f b) l))

The jump of variationOnFromTo on the right of a point is given by the distance between the right limit and the value of the function.

Defined in

Mathlib.Topology.EMetricSpace.VariationOnFromTo

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrderPseudoMetricSpaceTopologicalSpaceOrderTopology