1.11. ForMathlib.MeasureTheory.MeasurableSpace.Sigma
From the authors
Measurability of functions on a sigma type
A function on Σ a, β a is measurable as soon as each of its restrictions f ∘ Sigma.mk a is.
We also record measurability facts about the first projection of Σ n : ℕ, β n.
Module LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Sigma contains 10 exposed declarations.
-
measurable_sigma_mk -
measurable_sigma_of_measurable_comp_mk -
measurableSet_sigma_iff -
measurable_sigma_iff -
measurable_sigma_fst -
Measurable.sigmaMk -
measurableEmbedding_sigma_mk -
measurableSet_sigma_fst_le -
measurableSet_sigma_fst_lt -
MeasureTheory.Measure.map_sigmaMk_succ_apply_fst_le