Documentation Verification Report

SetAlgebra

📁 Source: Mathlib/MeasureTheory/SetAlgebra.lean

Statistics

Metric	Count
Definitions `IsSetAlgebra`, `generateSetAlgebra`	2
Theorems `biInter_mem`, `biUnion_mem`, `compl_mem`, `diff_mem`, `empty_mem`, `generateSetAlgebra_eq`, `generateSetAlgebra_subset`, `generateSetAlgebra_subset_self`, `inter_mem`, `isSetRing`, `union_mem`, `univ_mem`, `countable_generateSetAlgebra`, `generateFrom_generateSetAlgebra_eq`, `generateSetAlgebra_mono`, `isSetAlgebra_generateSetAlgebra`, `mem_generateSetAlgebra_elim`, `self_subset_generateSetAlgebra`	18
Total	20

MeasureTheory

Definitions

Name	Category	Theorems
`IsSetAlgebra` 📖	CompData	2 math math: `isSetAlgebra_measurableCylinders`, `isSetAlgebra_generateSetAlgebra`
`generateSetAlgebra` 📖	CompData	8 math math: `generateFrom_generateSetAlgebra_eq`, `countable_generateSetAlgebra`, `IsSetAlgebra.generateSetAlgebra_eq`, `self_subset_generateSetAlgebra`, `isSetAlgebra_generateSetAlgebra`, `IsSetAlgebra.generateSetAlgebra_subset`, `generateSetAlgebra_mono`, `IsSetAlgebra.generateSetAlgebra_subset_self`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`countable_generateSetAlgebra` 📖	mathematical	—	`Set.Countable` `Set` `generateSetAlgebra`	—	`Set.Countable.union` `Set.ext` `compl_compl` `Set.Countable.image` `Set.countable_setOf_finite_subset` `Set.countable_coe_iff` `mem_generateSetAlgebra_elim` `Set.Countable.mono`
`generateFrom_generateSetAlgebra_eq` 📖	mathematical	—	`MeasurableSpace.generateFrom` `generateSetAlgebra`	—	`le_antisymm` `MeasurableSpace.generateFrom_induction` `MeasurableSpace.measurableSet_generateFrom` `MeasurableSet.empty` `MeasurableSet.compl` `MeasurableSet.union` `MeasurableSpace.measurableSet_empty` `MeasurableSet.iUnion` `instCountableNat` `MeasurableSpace.generateFrom_mono` `self_subset_generateSetAlgebra`
`generateSetAlgebra_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`generateSetAlgebra`	—	`self_subset_generateSetAlgebra` `IsSetAlgebra.empty_mem` `isSetAlgebra_generateSetAlgebra` `IsSetAlgebra.compl_mem` `IsSetAlgebra.union_mem`
`isSetAlgebra_generateSetAlgebra` 📖	mathematical	—	`IsSetAlgebra` `generateSetAlgebra`	—	—
`mem_generateSetAlgebra_elim` 📖	mathematical	`Set` `Set.instMembership` `generateSetAlgebra`	`Set.Finite` `Compl.compl` `Set.instCompl` `Set.iUnion` `Set.iInter`	—	`Set.finite_singleton` `Set.eq_of_mem_singleton` `Set.iUnion_congr_Prop` `Set.iUnion_iUnion_eq_left` `Set.iInter_congr_Prop` `Set.iInter_iInter_eq_left` `Set.finite_empty` `Set.notMem_empty` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `Set.finite_coe_iff` `Finite.Set.finite_replacement` `Pi.finite` `compl_compl` `Set.ext` `Set.compl_iUnion` `Set.compl_iInter` `Set.iUnion_exists` `Set.iUnion_iUnion_eq'` `Set.iInter_exists` `Set.Finite.union` `Set.biUnion_union`
`self_subset_generateSetAlgebra` 📖	mathematical	—	`Set` `Set.instHasSubset` `generateSetAlgebra`	—	—

MeasureTheory.IsSetAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biInter_mem` 📖	mathematical	`MeasureTheory.IsSetAlgebra` `Set` `Set.instMembership`	`Set.iInter` `Finset` `Finset.instMembership`	—	`Finset.set_biInter_coe` `Finset.coe_empty` `Set.biInter_empty` `univ_mem` `MeasureTheory.IsSetRing.biInter_mem` `isSetRing`
`biUnion_mem` 📖	mathematical	`MeasureTheory.IsSetAlgebra` `Set` `Set.instMembership`	`Set.iUnion` `Finset` `Finset.instMembership`	—	`MeasureTheory.IsSetRing.biUnion_mem` `isSetRing`
`compl_mem` 📖	mathematical	`MeasureTheory.IsSetAlgebra` `Set` `Set.instMembership`	`Compl.compl` `Set.instCompl`	—	—
`diff_mem` 📖	mathematical	`MeasureTheory.IsSetAlgebra` `Set` `Set.instMembership`	`Set.instSDiff`	—	`inter_mem` `compl_mem`
`empty_mem` 📖	mathematical	`MeasureTheory.IsSetAlgebra`	`Set` `Set.instMembership` `Set.instEmptyCollection`	—	—
`generateSetAlgebra_eq` 📖	mathematical	`MeasureTheory.IsSetAlgebra`	`MeasureTheory.generateSetAlgebra`	—	`Set.Subset.antisymm` `generateSetAlgebra_subset_self` `MeasureTheory.self_subset_generateSetAlgebra`
`generateSetAlgebra_subset` 📖	mathematical	`Set` `Set.instHasSubset` `MeasureTheory.IsSetAlgebra`	`MeasureTheory.generateSetAlgebra`	—	`empty_mem` `compl_mem` `union_mem`
`generateSetAlgebra_subset_self` 📖	mathematical	`MeasureTheory.IsSetAlgebra`	`Set` `Set.instHasSubset` `MeasureTheory.generateSetAlgebra`	—	`generateSetAlgebra_subset` `subset_rfl` `Set.instReflSubset`
`inter_mem` 📖	mathematical	`MeasureTheory.IsSetAlgebra` `Set` `Set.instMembership`	`Set.instInter`	—	`compl_mem` `union_mem` `Set.inter_eq_compl_compl_union_compl`
`isSetRing` 📖	mathematical	`MeasureTheory.IsSetAlgebra`	`MeasureTheory.IsSetRing`	—	`empty_mem` `union_mem` `diff_mem`
`union_mem` 📖	mathematical	`MeasureTheory.IsSetAlgebra` `Set` `Set.instMembership`	`Set.instUnion`	—	—
`univ_mem` 📖	mathematical	`MeasureTheory.IsSetAlgebra`	`Set` `Set.instMembership` `Set.univ`	—	`compl_mem` `empty_mem` `Set.compl_empty`

---

← Back to Index