Theorems · Theorem · measure theory

Measurable.forall

∀ {α : Type u_1} {ι : Sort uι} [inst : MeasurableSpace α] [Countable ι] {p : ι → α → Prop},
  (∀ (i : ι), Measurable (p i)) → Measurable fun a => ∀ (i : ι), p i a

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Constructions

Cited by

2 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceCountable