IdentDistribIndep

📁 Source: Mathlib/Probability/IdentDistribIndep.lean

Statistics

Metric	Count
Definitions	0
Theorems pi, prodMk	2
Total	2

ProbabilityTheory.IdentDistrib

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pi 📖	mathematical	ProbabilityTheory.IdentDistrib ProbabilityTheory.iIndepFun	MeasurableSpace.pi	—	aemeasurable_pi_lambda aemeasurable_fst aemeasurable_snd ProbabilityTheory.iIndepFun.isProbabilityMeasure ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀' MeasureTheory.Measure.ext map_eq
prodMk 📖	mathematical	ProbabilityTheory.IdentDistrib ProbabilityTheory.IndepFun	Prod.instMeasurableSpace	—	AEMeasurable.prodMk aemeasurable_fst aemeasurable_snd map_eq MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.Measure.isFiniteMeasure_of_map ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map

---

← Back to Index