Theorems · Theorem · real analysis
AbsolutelyContinuousOnInterval.symm
∀ {X : Type u_1} [inst : PseudoMetricSpace X] {f : ℝ → X} {a b : ℝ},
AbsolutelyContinuousOnInterval f a b → AbsolutelyContinuousOnInterval f b a- Cited by
- 2 results in Mathlib
- Foundations
- Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- PseudoMetricSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- nhdsproof · cited by 5,554
- Finset.sumproof · cited by 5,195
- Filter.Tendstoproof · cited by 3,814
- PseudoMetricSpacestatement and proof · cited by 1,550
- Dist.distproof · cited by 1,539
- Finset.rangeproof · cited by 1,341
- Filter.principalproof · cited by 740
- AbsolutelyContinuousOnIntervalstatement and proof · cited by 31
- AbsolutelyContinuousOnInterval.totalLengthFilterproof · cited by 13
- AbsolutelyContinuousOnInterval.disjWithin_commproof · cited by 1
Cited by2
Results whose statement or proof uses this declaration.
- AbsolutelyContinuousOnInterval.boundedVariationOnproof · cited by 2
- AbsolutelyContinuousOnInterval.const_of_ae_hasDerivAt_zeroproof · cited by 1