HasLawExists

📁 Source: Mathlib/Probability/HasLawExists.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_hasLaw, exists_hasLaw_indepFun, exists_iid	3
Total	3

Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_hasLaw 📖	mathematical	—	Measurable ProbabilityTheory.HasLaw	—	measurable_id ProbabilityTheory.HasLaw.id

ProbabilityTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_hasLaw_indepFun 📖	mathematical	MeasureTheory.IsProbabilityMeasure	Measurable HasLaw iIndepFun	—	measurable_pi_apply MeasureTheory.MeasurePreserving.hasLaw measurePreserving_eval_infinitePi iIndepFun_iff_map_fun_eq_infinitePi_map MeasureTheory.Measure.instIsProbabilityMeasureForallInfinitePi MeasureTheory.Measure.map_id' MeasureTheory.MeasurePreserving.map_eq
exists_iid 📖	mathematical	—	Measurable HasLaw iIndepFun MeasureTheory.IsProbabilityMeasure	—	exists_hasLaw_indepFun

---

← Back to Index