FiniteDimensionalLaws

📁 Source: Mathlib/Probability/Process/FiniteDimensionalLaws.lean

Statistics

Metric	Count
Definitions	0
Theorems identDistrib_iff_forall_finset_identDistrib, isProjectiveLimit_map, isProjectiveMeasureFamily_map_restrict, map_eq_iff_forall_finset_map_restrict_eq, map_eq_of_forall_ae_eq, map_restrict_eq_of_forall_ae_eq	6
Total	6

ProbabilityTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
identDistrib_iff_forall_finset_identDistrib 📖	mathematical	AEMeasurable MeasurableSpace.pi	IdentDistrib Finset SetLike.instMembership Finset.instSetLike Finset.restrict	—	Measurable.comp_aemeasurable Finset.measurable_restrict map_eq_iff_forall_finset_map_restrict_eq IdentDistrib.map_eq
isProjectiveLimit_map 📖	mathematical	AEMeasurable MeasurableSpace.pi	MeasureTheory.IsProjectiveLimit MeasureTheory.Measure.map Finset SetLike.instMembership Finset.instSetLike Finset.restrict	—	AEMeasurable.map_map_of_aemeasurable Measurable.aemeasurable Finset.measurable_restrict
isProjectiveMeasureFamily_map_restrict 📖	mathematical	AEMeasurable	MeasureTheory.IsProjectiveMeasureFamily MeasureTheory.Measure.map MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.restrict	—	AEMeasurable.map_map_of_aemeasurable Measurable.aemeasurable Finset.measurable_restrict₂ aemeasurable_pi_lambda Finite.to_countable Finite.of_fintype
map_eq_iff_forall_finset_map_restrict_eq 📖	mathematical	AEMeasurable MeasurableSpace.pi	MeasureTheory.Measure.map Finset SetLike.instMembership Finset.instSetLike Finset.restrict	—	AEMeasurable.map_map_of_aemeasurable Measurable.aemeasurable Finset.measurable_restrict isProjectiveLimit_map MeasureTheory.IsProjectiveLimit.unique MeasureTheory.Measure.isFiniteMeasure_map
map_eq_of_forall_ae_eq 📖	mathematical	AEMeasurable MeasurableSpace.pi Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.Measure.map	—	MeasureTheory.Measure.instOuterMeasureClass map_eq_iff_forall_finset_map_restrict_eq map_restrict_eq_of_forall_ae_eq
map_restrict_eq_of_forall_ae_eq 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.Measure.map MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.restrict	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_all_iff Finite.to_countable Finite.of_fintype MeasureTheory.Measure.map_congr Filter.mp_mem Filter.univ_mem'

---

← Back to Index