Documentation Verification Report

MemPartition

📁 Source: Mathlib/Data/Set/MemPartition.lean

Statistics

Metric	Count
Definitions `instFintype_memPartition`, `memPartition`, `memPartitionSet`	3
Theorems `disjoint_memPartition`, `finite_memPartition`, `instFinite_memPartition`, `memPartitionSet_eq_iff`, `memPartitionSet_mem`, `memPartitionSet_of_mem`, `memPartitionSet_succ`, `memPartitionSet_zero`, `memPartition_succ`, `memPartition_zero`, `mem_memPartitionSet`, `sUnion_memPartition`	12
Total	15

(root)

Definitions

Name	Category	Theorems
`instFintype_memPartition` 📖	CompOp	—
`memPartition` 📖	CompOp	14 math math: `memPartition_zero`, `finite_memPartition`, `sUnion_memPartition`, `MeasurableSpace.generateFrom_memPartition_le`, `MeasurableSpace.measurableSet_generateFrom_memPartition_iff`, `MeasurableSpace.measurableSet_generateFrom_memPartition`, `MeasurableSpace.generateFrom_memPartition_le_range`, `MeasurableSpace.generateFrom_iUnion_memPartition`, `MeasurableSpace.generateFrom_memPartition_le_succ`, `ProbabilityTheory.measurable_memPartitionSet_subtype`, `memPartition_succ`, `MeasurableSpace.generateFrom_iUnion_memPartition_le`, `instFinite_memPartition`, `memPartitionSet_mem`
`memPartitionSet` 📖	CompOp	11 math math: `memPartitionSet_succ`, `memPartitionSet_eq_iff`, `memPartitionSet_zero`, `mem_memPartitionSet`, `ProbabilityTheory.measurableSet_partitionFiltration_memPartitionSet`, `ProbabilityTheory.measurable_memPartitionSet_subtype`, `ProbabilityTheory.measurable_partitionFiltration_memPartitionSet`, `MeasurableSpace.measurableSet_memPartitionSet`, `memPartitionSet_of_mem`, `ProbabilityTheory.measurable_memPartitionSet`, `memPartitionSet_mem`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_memPartition` 📖	mathematical	`Set` `Set.instMembership` `memPartition`	`Disjoint` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`memPartition_succ` `Disjoint.mono` `Set.inter_subset_left` `Disjoint.mono_left` `Set.inter_subset_right` `Set.disjoint_sdiff_right` `Disjoint.mono_right` `Set.disjoint_sdiff_left` `Set.diff_subset`
`finite_memPartition` 📖	mathematical	—	`Set.Finite` `Set` `memPartition`	—	`memPartition_succ` `Set.finite_coe_iff` `Set.setOf_exists` `Set.iUnion_congr_Prop` `Finite.Set.finite_biUnion` `Set.union_singleton`
`instFinite_memPartition` 📖	mathematical	—	`Finite` `Set.Elem` `Set` `memPartition`	—	`Set.finite_coe_iff` `finite_memPartition`
`memPartitionSet_eq_iff` 📖	mathematical	`Set` `Set.instMembership` `memPartition`	`memPartitionSet`	—	`mem_memPartitionSet` `disjoint_memPartition` `memPartitionSet_mem` `Set.not_disjoint_iff_nonempty_inter`
`memPartitionSet_mem` 📖	mathematical	—	`Set` `Set.instMembership` `memPartition` `memPartitionSet`	—	`memPartitionSet_succ` `memPartition_succ`
`memPartitionSet_of_mem` 📖	mathematical	`Set` `Set.instMembership` `memPartition`	`memPartitionSet`	—	`memPartitionSet_eq_iff`
`memPartitionSet_succ` 📖	mathematical	—	`memPartitionSet` `Set` `Set.instMembership` `Set.instInter` `Set.instSDiff`	—	—
`memPartitionSet_zero` 📖	mathematical	—	`memPartitionSet` `Set.univ`	—	—
`memPartition_succ` 📖	mathematical	—	`memPartition` `setOf` `Set` `Set.instMembership` `Set.instInter` `Set.instSDiff`	—	—
`memPartition_zero` 📖	mathematical	—	`memPartition` `Set` `Set.instSingletonSet` `Set.univ`	—	—
`mem_memPartitionSet` 📖	mathematical	—	`Set` `Set.instMembership` `memPartitionSet`	—	`memPartitionSet_succ`
`sUnion_memPartition` 📖	mathematical	—	`Set.sUnion` `memPartition` `Set.univ`	—	`Set.sUnion_singleton` `memPartition_succ` `Set.ext`

---

← Back to Index