Theorems · Theorem · real analysis
BoundedVariationOn.eVariationOn_Iic_eq_Iio_add_edist
∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [CompleteSpace E]
[DenselyOrdered α] {f : α → E} {a : α},
BoundedVariationOn f Set.univ →
eVariationOn f (Set.Iic a) = eVariationOn f (Set.Iio a) + edist (f a) (Function.leftLim f a)- Cited by
- 1 results in Mathlib
- Foundations
- Depth 161 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites32
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpaceproof · cited by 24,529
- ENNRealstatement · cited by 9,879
- LinearOrderstatement and proof · cited by 8,572
- nhdsproof · cited by 5,554
- Set.univstatement and proof · cited by 3,945
- Filter.Tendstoproof · cited by 3,814
- add_zeroproof · cited by 2,707
- CompleteSpacestatement and proof · cited by 2,532
- Set.extproof · cited by 2,266
- nhdsWithinproof · cited by 1,912
- PseudoEMetricSpacestatement and proof · cited by 1,536
- OrderTopologyproof · cited by 1,355
Cited by1
Results whose statement or proof uses this declaration.
- BoundedVariationOn.eVariationOn_Ici_eq_Ioi_add_edistproof · cited by 0