Theorems · Theorem · measure theory
Finset.measurable_prod_apply
∀ {M : Type u_2} {ι : Type u_3} {α : Type u_4} {β : Type u_5} [inst : CommMonoid M] [inst_1 : MeasurableSpace M]
[MeasurableMul₂ M] {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : ι → α → β → M} {g : α → β} {s : Finset ι},
(∀ i ∈ s, Measurable ↿(f i)) → Measurable g → Measurable fun a => (∏ i ∈ s, f i a) (g a)Compositional version of Finset.measurable_prod for use by fun_prop.
- Defined in
- Mathlib.MeasureTheory.Group.Arithmetic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- MeasurableSpacestatement and proof · cited by 13,106
- Finset.prodstatement · cited by 2,356
- CommMonoidstatement and proof · cited by 2,264
- Measurablestatement and proof · cited by 1,499
- measurable_id'proof · cited by 145
- MeasurableMul₂statement and proof · cited by 139
- Measurable.prodMkproof · cited by 115
- Measurable.fun_compproof · cited by 95
- Finset.prod_applyproof · cited by 70
- Function.HasUncurry.uncurrystatement and proof · cited by 57
- Finset.measurable_prodproof · cited by 11
Cited by1
Results whose statement or proof uses this declaration.
- Measurable.tprod'proof · cited by 0