Projective

📁 Source: Mathlib/MeasureTheory/Constructions/Projective.lean

Statistics

Metric	Count
Definitions IsProjectiveLimit, IsProjectiveMeasureFamily	2
Theorems isFiniteMeasure, isProbabilityMeasure, measure_cylinder, measure_univ_eq, measure_univ_unique, unique, congr_cylinder, congr_cylinder_of_subset, eq_zero_of_isEmpty, measure_univ_eq, measure_univ_eq_of_subset	11
Total	13

MeasureTheory

Definitions

Name	Category	Theorems
IsProjectiveLimit 📖	MathDef	6 math math: isProjectiveLimit_nat_iff, Measure.isProjectiveLimit_infinitePi, ProbabilityTheory.Kernel.isProjectiveLimit_trajFun, Measure.isProjectiveLimit_infinitePiNat, ProbabilityTheory.isProjectiveLimit_map, isProjectiveLimit_nat_iff'
IsProjectiveMeasureFamily 📖	MathDef	4 math math: isProjectiveMeasureFamily_inducedFamily, isProjectiveMeasureFamily_pi, ProbabilityTheory.isProjectiveMeasureFamily_map_restrict, ProbabilityTheory.Kernel.isProjectiveMeasureFamily_partialTraj

MeasureTheory.IsProjectiveLimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isFiniteMeasure 📖	—	MeasureTheory.IsFiniteMeasure MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike MeasureTheory.IsProjectiveLimit	—	—	measure_univ_eq MeasureTheory.measure_lt_top
isProbabilityMeasure 📖	—	MeasureTheory.IsProbabilityMeasure MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike MeasureTheory.IsProjectiveLimit	—	—	measure_univ_eq MeasureTheory.IsProbabilityMeasure.measure_univ
measure_cylinder 📖	mathematical	MeasureTheory.IsProjectiveLimit MeasurableSet MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.cylinder	—	MeasureTheory.cylinder.eq_1 MeasureTheory.Measure.map_apply measurable_pi_lambda measurable_pi_apply
measure_univ_eq 📖	mathematical	MeasureTheory.IsProjectiveLimit	DFunLike.coe MeasureTheory.Measure MeasurableSpace.pi Set ENNReal MeasureTheory.Measure.instFunLike Set.univ Finset SetLike.instMembership Finset.instSetLike	—	MeasureTheory.cylinder_univ measure_cylinder MeasurableSet.univ
measure_univ_unique 📖	mathematical	MeasureTheory.IsProjectiveLimit	DFunLike.coe MeasureTheory.Measure MeasurableSpace.pi Set ENNReal MeasureTheory.Measure.instFunLike Set.univ	—	measure_univ_eq
unique 📖	—	MeasureTheory.IsFiniteMeasure MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike MeasureTheory.IsProjectiveLimit	—	—	MeasureTheory.ext_of_generate_finite MeasureTheory.generateFrom_measurableCylinders MeasureTheory.isPiSystem_measurableCylinders isFiniteMeasure MeasureTheory.mem_measurableCylinders measure_cylinder measure_univ_unique

MeasureTheory.IsProjectiveMeasureFamily

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_cylinder 📖	mathematical	MeasureTheory.IsProjectiveMeasureFamily MeasurableSet MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike MeasureTheory.cylinder	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike	—	Finset.subset_union_left Finset.subset_union_right MeasureTheory.inter_cylinder Set.inter_self congr_cylinder_of_subset
congr_cylinder_of_subset 📖	mathematical	MeasureTheory.IsProjectiveMeasureFamily MeasurableSet MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike MeasureTheory.cylinder Finset.instHasSubset	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike	—	isEmpty_or_nonempty eq_zero_of_isEmpty MeasureTheory.eq_of_cylinder_eq_of_subset MeasureTheory.Measure.map_apply measurable_pi_lambda measurable_pi_apply
eq_zero_of_isEmpty 📖	mathematical	MeasureTheory.IsProjectiveMeasureFamily	MeasureTheory.Measure MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike MeasureTheory.Measure.instZero	—	isEmpty_pi Finset.subset_insert MeasureTheory.Measure.eq_zero_of_isEmpty MeasureTheory.Measure.map_zero
measure_univ_eq 📖	mathematical	MeasureTheory.IsProjectiveMeasureFamily	DFunLike.coe MeasureTheory.Measure MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Set ENNReal MeasureTheory.Measure.instFunLike Set.univ	—	measure_univ_eq_of_subset Finset.subset_union_left Finset.subset_union_right
measure_univ_eq_of_subset 📖	mathematical	MeasureTheory.IsProjectiveMeasureFamily Finset Finset.instHasSubset	DFunLike.coe MeasureTheory.Measure MeasurableSpace.pi SetLike.instMembership Finset.instSetLike Set ENNReal MeasureTheory.Measure.instFunLike Set.univ	—	Set.preimage_univ MeasureTheory.Measure.map_apply measurable_pi_lambda measurable_pi_apply MeasurableSet.univ

---

← Back to Index