Theorems · Theorem · real analysis

eVariationOn.pair

∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) (a b : α),
  eVariationOn f {a, b} = edist (f a) (f b)

The variation of f on a two-point set {a, b} is the distance between its two values.

Defined in

Mathlib.Topology.EMetricSpace.BoundedVariation

Cited by

2 results in Mathlib

Foundations

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

Assumes

LinearOrderPseudoEMetricSpace