Documentation Verification Report

ProjectiveFamilyContent

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

Statistics

Metric	Count
Definitions `projectiveFamilyContent`, `projectiveFamilyFun`	2
Theorems `isSetAlgebra_measurableCylinders`, `isSetRing_measurableCylinders`, `isSetSemiring_measurableCylinders`, `projectiveFamilyContent_congr`, `projectiveFamilyContent_cylinder`, `projectiveFamilyContent_diff`, `projectiveFamilyContent_diff_of_subset`, `projectiveFamilyContent_eq`, `projectiveFamilyContent_iUnion_le`, `projectiveFamilyContent_mono`, `projectiveFamilyContent_ne_top`, `projectiveFamilyFun_congr`, `projectiveFamilyFun_empty`, `projectiveFamilyFun_union`	14
Total	16

MeasureTheory

Definitions

Name	Category	Theorems
`projectiveFamilyContent` 📖	CompOp	7 math math: `projectiveFamilyContent_eq`, `projectiveFamilyContent_diff`, `projectiveFamilyContent_cylinder`, `projectiveFamilyContent_congr`, `projectiveFamilyContent_diff_of_subset`, `projectiveFamilyContent_iUnion_le`, `projectiveFamilyContent_mono`
`projectiveFamilyFun` 📖	CompOp	4 math math: `projectiveFamilyFun_empty`, `projectiveFamilyContent_eq`, `projectiveFamilyFun_union`, `projectiveFamilyFun_congr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSetAlgebra_measurableCylinders` 📖	mathematical	—	`IsSetAlgebra` `measurableCylinders`	—	`empty_mem_measurableCylinders` `compl_mem_measurableCylinders` `union_mem_measurableCylinders`
`isSetRing_measurableCylinders` 📖	mathematical	—	`IsSetRing` `measurableCylinders`	—	`IsSetAlgebra.isSetRing` `isSetAlgebra_measurableCylinders`
`isSetSemiring_measurableCylinders` 📖	mathematical	—	`IsSetSemiring` `measurableCylinders`	—	`IsSetRing.isSetSemiring` `isSetRing_measurableCylinders`
`projectiveFamilyContent_congr` 📖	mathematical	`IsProjectiveMeasureFamily` `cylinder` `MeasurableSet` `MeasurableSpace.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike`	`DFunLike.coe` `AddContent` `ENNReal` `ENNReal.instAddCommMonoid` `measurableCylinders` `Set` `instFunLikeAddContentSet` `projectiveFamilyContent` `Measure` `Measure.instFunLike`	—	`projectiveFamilyContent_eq` `projectiveFamilyFun_congr` `mem_measurableCylinders`
`projectiveFamilyContent_cylinder` 📖	mathematical	`IsProjectiveMeasureFamily` `MeasurableSet` `MeasurableSpace.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike`	`DFunLike.coe` `AddContent` `ENNReal` `ENNReal.instAddCommMonoid` `measurableCylinders` `Set` `instFunLikeAddContentSet` `projectiveFamilyContent` `cylinder` `Measure` `Measure.instFunLike`	—	`projectiveFamilyContent_congr`
`projectiveFamilyContent_diff` 📖	mathematical	`IsProjectiveMeasureFamily` `Set` `Set.instMembership` `measurableCylinders`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.instSub` `DFunLike.coe` `AddContent` `ENNReal.instAddCommMonoid` `instFunLikeAddContentSet` `projectiveFamilyContent` `Set.instSDiff`	—	`le_addContent_diff` `isSetRing_measurableCylinders`
`projectiveFamilyContent_diff_of_subset` 📖	mathematical	`IsFiniteMeasure` `MeasurableSpace.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike` `IsProjectiveMeasureFamily` `Set` `Set.instMembership` `measurableCylinders` `Set.instHasSubset`	`DFunLike.coe` `AddContent` `ENNReal` `ENNReal.instAddCommMonoid` `instFunLikeAddContentSet` `projectiveFamilyContent` `Set.instSDiff` `ENNReal.instSub`	—	`addContent_diff_of_ne_top` `isSetRing_measurableCylinders` `projectiveFamilyContent_ne_top`
`projectiveFamilyContent_eq` 📖	mathematical	`IsProjectiveMeasureFamily`	`DFunLike.coe` `AddContent` `ENNReal` `ENNReal.instAddCommMonoid` `measurableCylinders` `Set` `instFunLikeAddContentSet` `projectiveFamilyContent` `projectiveFamilyFun`	—	—
`projectiveFamilyContent_iUnion_le` 📖	mathematical	`IsProjectiveMeasureFamily` `Set` `Set.instMembership` `measurableCylinders`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `AddContent` `ENNReal.instAddCommMonoid` `instFunLikeAddContentSet` `projectiveFamilyContent` `Set.iUnion` `Finset.sum` `Finset.range`	—	`Set.iUnion_congr_Prop` `addContent_biUnion_le` `ENNReal.instCanonicallyOrderedAdd` `isSetRing_measurableCylinders`
`projectiveFamilyContent_mono` 📖	mathematical	`IsProjectiveMeasureFamily` `Set` `Set.instMembership` `measurableCylinders` `Set.instHasSubset`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `AddContent` `ENNReal.instAddCommMonoid` `instFunLikeAddContentSet` `projectiveFamilyContent`	—	`addContent_mono` `ENNReal.instCanonicallyOrderedAdd` `isSetSemiring_measurableCylinders`
`projectiveFamilyContent_ne_top` 📖	—	`IsFiniteMeasure` `MeasurableSpace.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike` `IsProjectiveMeasureFamily`	—	—	`projectiveFamilyContent_eq` `projectiveFamilyFun.eq_1` `dite_ne_top` `measure_ne_top` `ENNReal.zero_ne_top`
`projectiveFamilyFun_congr` 📖	mathematical	`IsProjectiveMeasureFamily` `Set` `Set.instMembership` `measurableCylinders` `cylinder` `MeasurableSet` `MeasurableSpace.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike`	`projectiveFamilyFun` `DFunLike.coe` `Measure` `ENNReal` `Measure.instFunLike`	—	`projectiveFamilyFun.eq_1` `IsProjectiveMeasureFamily.congr_cylinder` `measurableCylinders.measurableSet` `measurableCylinders.eq_cylinder`
`projectiveFamilyFun_empty` 📖	mathematical	`IsProjectiveMeasureFamily`	`projectiveFamilyFun` `Set` `Set.instEmptyCollection` `ENNReal` `instZeroENNReal`	—	`projectiveFamilyFun_congr` `empty_mem_measurableCylinders` `cylinder_empty` `MeasurableSet.empty` `measure_empty` `Measure.instOuterMeasureClass`
`projectiveFamilyFun_union` 📖	mathematical	`IsProjectiveMeasureFamily` `Set` `Set.instMembership` `measurableCylinders` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`projectiveFamilyFun` `Set.instUnion` `ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`mem_measurableCylinders` `Finset.subset_union_left` `Finset.subset_union_right` `Finset.measurable_restrict₂` `cylinder_eq_cylinder_union` `union_cylinder` `projectiveFamilyFun_congr` `union_mem_measurableCylinders` `MeasurableSet.union` `isEmpty_or_nonempty` `IsProjectiveMeasureFamily.eq_zero_of_isEmpty` `add_zero` `measure_union` `disjoint_cylinder_iff`

---

← Back to Index