Theorems · Theorem · real analysis

BoundedVariationOn.exists_tendsto_atTop

∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [CompleteSpace E]
  [hE : Nonempty E] {f : α → E} {s : Set α},
  BoundedVariationOn f s → ∃ l, Filter.Tendsto f (Filter.principal s ⊓ Filter.atTop) (nhds l)

A bounded variation function has a limit at +∞.

Defined in

Mathlib.Topology.EMetricSpace.BoundedVariation

Cited by

2 results in Mathlib

Foundations

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

Assumes

LinearOrderPseudoEMetricSpaceCompleteSpaceNonempty