Mathlib Map

Theorems · Theorem · real analysis

AbsolutelyContinuousOnInterval.add

∀ {F : Type u_2} [inst : SeminormedAddCommGroup F] {a b : ℝ} {f g : ℝ → F},
  AbsolutelyContinuousOnInterval f a b →
    AbsolutelyContinuousOnInterval g a b → AbsolutelyContinuousOnInterval (f + g) a b
Defined in
Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Cited by
2 results in Mathlib
Foundations
Depth 156 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
SeminormedAddCommGroup
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AbsolutelyContinuousOnInterval.sub · cited by 2AbsolutelyContinuousOnInt…AbsolutelyContinuousOnInterval.fun_add · cited by 0AbsolutelyContinuousOnInt…Real · cited by 25697Realnhds · cited by 5554nhdsFinset.sum · cited by 5195Finset.sumFilter.Tendsto · cited by 3814Filter.Tendstoadd_zero · cited by 2707add_zeroSeminormedAddCommGroup · cited by 2671SeminormedAddCommGroupDist.dist · cited by 1539Dist.distFinset.range · cited by 1341Finset.rangeFilter.principal · cited by 740Filter.principalFinset.sum_le_sum · cited by 182Finset.sum_le_sumFinset.sum_add_distrib · cited by 131Finset.sum_add_distribdist_nonneg · cited by 126dist_nonnegFilter.Tendsto.add · cited by 102Tendsto.addFinset.sum_nonneg · cited by 91Finset.sum_nonnegAbsolutelyContinuousOnInterval · cited by 31AbsolutelyContinuousOnInt…AbsolutelyContinuousOnInterva…CITED BYCITES

Cites19

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.