Mathlib Map

Theorems · Theorem · measure theory

List.stronglyMeasurable_sum

∀ {α : Type u_1} {M : Type u_5} [inst : AddMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M]
  {m : MeasurableSpace α} (l : List (α → M)),
  (∀ f ∈ l, MeasureTheory.StronglyMeasurable f) → MeasureTheory.StronglyMeasurable l.sum
Defined in
Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Cited by
2 results in Mathlib
Foundations
Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AddMonoidTopologicalSpaceContinuousAdd
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Multiset.stronglyMeasurable_sum · cited by 1Multiset.stronglyMeasurab…List.stronglyMeasurable_fun_sum · cited by 0List.stronglyMeasurable_f…TopologicalSpace · cited by 24529TopologicalSpaceMeasurableSpace · cited by 13106MeasurableSpaceAddMonoid · cited by 2864AddMonoidContinuousAdd · cited by 777ContinuousAddMeasureTheory.StronglyMeasurable · cited by 363MeasureTheory.StronglyMea…MeasureTheory.stronglyMeasurable_zero · cited by 13MeasureTheory.stronglyMea…MeasureTheory.StronglyMeasurable.add · cited by 10StronglyMeasurable.addList.stronglyMeasurable_sumCITED BYCITES

Cites7

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.