Theorems · Theorem · real analysis
BoundedVariationOn.locallyBoundedVariationOn
∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
BoundedVariationOn f s → LocallyBoundedVariationOn f s- Cited by
- 5 results in Mathlib
- Foundations
- Depth 151 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- LinearOrderstatement and proof · cited by 8,572
- PseudoEMetricSpacestatement and proof · cited by 1,536
- Set.inter_subset_leftproof · cited by 360
- BoundedVariationOnstatement and proof · cited by 65
- LocallyBoundedVariationOnstatement · cited by 41
- BoundedVariationOn.monoproof · cited by 3
Cited by5
Results whose statement or proof uses this declaration.
- BoundedVariationOn.intervalIntegrable_derivproof · cited by 1
- BoundedVariationOn.continuousWithinAt_variationOnFromTo_Iciproof · cited by 1
- BoundedVariationOn.ae_differentiableAt_of_mem_uIccproof · cited by 1
- variationOnFromTo.leftLim_eqproof · cited by 0
- variationOnFromTo.rightLim_eqproof · cited by 0