PiSystem

📁 Source: Mathlib/MeasureTheory/PiSystem.lean

Statistics

Metric	Count
Definitions `IsPiSystem`, `DynkinSystem`, `GenerateHas`, `Has`, `generate`, `instInhabited`, `instLEDynkinSystem`, `instPartialOrder`, `ofMeasurableSpace`, `restrictOn`, `toMeasurableSpace`, `generatePiSystem`, `piiUnionInter`	13
Theorems `biInter_mem`, `comap`, `insert_empty`, `insert_univ`, `prod`, `singleton`, `ext`, `ext_iff`, `generateFrom_eq`, `generateHas_compl`, `generateHas_def`, `generate_has_subset_generate_measurable`, `generate_inter`, `generate_le`, `has_compl`, `has_compl_iff`, `has_diff`, `has_empty`, `has_iUnion`, `has_iUnion_nat`, `has_union`, `has_univ`, `le_def`, `ofMeasurableSpace_le_ofMeasurableSpace_iff`, `ofMeasurableSpace_toMeasurableSpace`, `induction_on_inter`, `isPiSystem_measurableSet`, `generateFrom_generatePiSystem_eq`, `generateFrom_measurableSet_of_generatePiSystem`, `generateFrom_piiUnionInter_le`, `generateFrom_piiUnionInter_measurableSet`, `generateFrom_piiUnionInter_singleton_left`, `generatePiSystem_eq`, `generatePiSystem_measurableSet`, `generatePiSystem_mono`, `generatePiSystem_subset_self`, `isPiSystem_Icc`, `isPiSystem_Icc_mem`, `isPiSystem_Ici`, `isPiSystem_Ico`, `isPiSystem_Ico_mem`, `isPiSystem_Iic`, `isPiSystem_Iio`, `isPiSystem_Ioc`, `isPiSystem_Ioc_mem`, `isPiSystem_Ioi`, `isPiSystem_Ioo`, `isPiSystem_Ioo_mem`, `isPiSystem_Ixx`, `isPiSystem_Ixx_mem`, `isPiSystem_generatePiSystem`, `isPiSystem_iUnion_of_directed_le`, `isPiSystem_iUnion_of_monotone`, `isPiSystem_image_Ici`, `isPiSystem_image_Iic`, `isPiSystem_image_Iio`, `isPiSystem_image_Ioi`, `isPiSystem_piiUnionInter`, `le_generateFrom_piiUnionInter`, `measurableSet_iSup_of_mem_piiUnionInter`, `mem_generatePiSystem_iUnion_elim`, `mem_generatePiSystem_iUnion_elim'`, `mem_piiUnionInter_of_measurableSet`, `piiUnionInter_mono_left`, `piiUnionInter_mono_right`, `piiUnionInter_singleton`, `piiUnionInter_singleton_left`, `subset_generatePiSystem_self`, `subset_piiUnionInter`	69
Total	82

IsPiSystem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biInter_mem` 📖	—	`IsPiSystem` `Finset.Nonempty` `Set` `Set.instMembership` `Set.Nonempty` `Set.iInter` `Finset` `Finset.instMembership`	—	—	`Finset.Nonempty.cons_induction` `Set.iInter_congr_Prop` `Set.iInter_iInter_eq_left` `Finset.cons_eq_insert` `Set.iInter_iInter_eq_or_left` `Set.Nonempty.right`
`comap` 📖	mathematical	`IsPiSystem`	`setOf` `Set` `Set.instMembership` `Set.preimage`	—	`Set.preimage_inter` `Set.nonempty_of_nonempty_preimage`
`insert_empty` 📖	mathematical	`IsPiSystem`	`Set` `Set.instInsert` `Set.instEmptyCollection`	—	`Set.empty_inter` `Set.inter_empty` `Set.mem_insert_of_mem`
`insert_univ` 📖	mathematical	`IsPiSystem`	`Set` `Set.instInsert` `Set.univ`	—	`Set.inter_self` `Set.univ_inter` `Set.inter_univ` `Set.mem_insert_of_mem`
`prod` 📖	mathematical	`IsPiSystem`	`Set.image2` `Set` `SProd.sprod` `Set.instSProd`	—	`Set.prod_inter_prod` `Set.mem_image2_of_mem` `Set.prod_nonempty_iff`
`singleton` 📖	mathematical	—	`IsPiSystem` `Set` `Set.instSingletonSet`	—	`Set.mem_singleton_iff` `Set.inter_self`

MeasurableSpace

Definitions

Name	Category	Theorems
`DynkinSystem` 📖	CompData	3 math math: `DynkinSystem.generate_le`, `DynkinSystem.le_def`, `DynkinSystem.ofMeasurableSpace_le_ofMeasurableSpace_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`induction_on_inter` 📖	—	`generateFrom` `IsPiSystem` `Set` `Set.instEmptyCollection` `MeasurableSet.empty` `MeasurableSpace` `MeasurableSet` `GenerateMeasurable.basic` `Compl.compl` `Set.instCompl` `MeasurableSet.compl` `Set.iUnion` `MeasurableSet.iUnion` `instCountableNat`	—	—	`MeasurableSet.empty` `MeasurableSet.compl` `MeasurableSet.iUnion` `instCountableNat` `DynkinSystem.generate_inter` `DynkinSystem.generateFrom_eq`
`isPiSystem_measurableSet` 📖	mathematical	—	`IsPiSystem` `setOf` `Set` `MeasurableSet`	—	`MeasurableSet.inter`

MeasurableSpace.DynkinSystem

Definitions

Name	Category	Theorems
`GenerateHas` 📖	CompData	2 math math: `generateHas_compl`, `generateHas_def`
`Has` 📖	MathDef	6 math math: `ext_iff`, `has_compl_iff`, `has_univ`, `has_empty`, `le_def`, `generateHas_def`
`generate` 📖	CompOp	3 math math: `generate_le`, `generateFrom_eq`, `generateHas_def`
`instInhabited` 📖	CompOp	—
`instLEDynkinSystem` 📖	CompOp	3 math math: `generate_le`, `le_def`, `ofMeasurableSpace_le_ofMeasurableSpace_iff`
`instPartialOrder` 📖	CompOp	—
`ofMeasurableSpace` 📖	CompOp	2 math math: `ofMeasurableSpace_toMeasurableSpace`, `ofMeasurableSpace_le_ofMeasurableSpace_iff`
`restrictOn` 📖	CompOp	—
`toMeasurableSpace` 📖	CompOp	2 math math: `ofMeasurableSpace_toMeasurableSpace`, `generateFrom_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`Has`	—	—	—
`ext_iff` 📖	mathematical	—	`Has`	—	`ext`
`generateFrom_eq` 📖	mathematical	`IsPiSystem`	`MeasurableSpace.generateFrom` `toMeasurableSpace` `generate` `generate_inter`	—	`le_antisymm` `generate_inter` `MeasurableSpace.generateFrom_le` `ofMeasurableSpace_le_ofMeasurableSpace_iff` `ofMeasurableSpace_toMeasurableSpace` `generate_le` `MeasurableSpace.measurableSet_generateFrom`
`generateHas_compl` 📖	mathematical	—	`GenerateHas` `Compl.compl` `Set` `Set.instCompl`	—	`compl_compl`
`generateHas_def` 📖	mathematical	—	`Has` `generate` `GenerateHas`	—	—
`generate_has_subset_generate_measurable` 📖	mathematical	`Has` `generate`	`MeasurableSet` `MeasurableSpace.generateFrom`	—	`generate_le` `MeasurableSpace.measurableSet_generateFrom`
`generate_inter` 📖	mathematical	`IsPiSystem` `Has` `generate`	`Set` `Set.instInter`	—	`generate_le` `Set.eq_empty_or_nonempty` `Set.inter_comm`
`generate_le` 📖	mathematical	`Has`	`MeasurableSpace.DynkinSystem` `instLEDynkinSystem` `generate`	—	`has_empty` `has_compl` `has_iUnion` `instCountableNat`
`has_compl` 📖	mathematical	`Has`	`Compl.compl` `Set` `Set.instCompl`	—	—
`has_compl_iff` 📖	mathematical	—	`Has` `Compl.compl` `Set` `Set.instCompl`	—	`compl_compl` `has_compl`
`has_diff` 📖	mathematical	`Has` `Set` `Set.instHasSubset`	`Set.instSDiff`	—	`has_compl_iff` `Set.compl_inter` `compl_compl` `has_union` `has_compl` `Disjoint.mono_right` `disjoint_compl_left`
`has_empty` 📖	mathematical	—	`Has` `Set` `Set.instEmptyCollection`	—	—
`has_iUnion` 📖	mathematical	`Pairwise` `Function.onFun` `Set` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Has`	`Set.iUnion`	—	`nonempty_encodable` `Encodable.iUnion_decode₂` `has_iUnion_nat` `Encodable.iUnion_decode₂_disjoint_on` `Encodable.iUnion_decode₂_cases` `has_empty`
`has_iUnion_nat` 📖	mathematical	`Pairwise` `Function.onFun` `Set` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Has`	`Set.iUnion`	—	—
`has_union` 📖	mathematical	`Has` `Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`Set.instUnion`	—	`Set.union_eq_iUnion` `has_iUnion` `Bool.countable` `pairwise_disjoint_on_bool`
`has_univ` 📖	mathematical	—	`Has` `Set.univ`	—	`Set.compl_empty` `has_compl` `has_empty`
`le_def` 📖	mathematical	—	`MeasurableSpace.DynkinSystem` `instLEDynkinSystem` `Pi.hasLe` `Set` `Prop.le` `Has`	—	—
`ofMeasurableSpace_le_ofMeasurableSpace_iff` 📖	mathematical	—	`MeasurableSpace.DynkinSystem` `instLEDynkinSystem` `ofMeasurableSpace` `MeasurableSpace` `MeasurableSpace.instLE`	—	—
`ofMeasurableSpace_toMeasurableSpace` 📖	mathematical	`Has` `Set` `Set.instInter`	`ofMeasurableSpace` `toMeasurableSpace`	—	`ext`

(root)

Definitions

Name	Category	Theorems
`IsPiSystem` 📖	MathDef	32 math math: `isPiSystem_Ixx`, `isPiSystem_prod`, `isPiSystem_image_Iic`, `MeasurableSpace.isPiSystem_measurableSet`, `isPiSystem_Ioi`, `isPiSystem_image_Ioi`, `Real.isPiSystem_Iic_rat`, `MeasureTheory.IsSetSemiring.isPiSystem`, `isPiSystem_generatePiSystem`, `isPiSystem_Ioc`, `isPiSystem_Ico_mem`, `Real.isPiSystem_Iio_rat`, `Real.isPiSystem_Ioi_rat`, `Real.isPiSystem_Ici_rat`, `isPiSystem_isClosed`, `isPiSystem_Ico`, `IsPiSystem.singleton`, `isPiSystem_image_Iio`, `isPiSystem_Iio`, `isPiSystem_Ixx_mem`, `isPiSystem_Ioc_mem`, `isPiSystem_Icc`, `isPiSystem_Ici`, `isPiSystem_isOpen`, `isPiSystem_Ioo`, `MeasureTheory.isPiSystem_measurableCylinders`, `isPiSystem_pi`, `isPiSystem_Icc_mem`, `isPiSystem_Iic`, `isPiSystem_Ioo_mem`, `isPiSystem_image_Ici`, `Real.isPiSystem_Ioo_rat`
`generatePiSystem` 📖	CompData	6 math math: `generatePiSystem_subset_self`, `isPiSystem_generatePiSystem`, `subset_generatePiSystem_self`, `generateFrom_generatePiSystem_eq`, `generatePiSystem_eq`, `generatePiSystem_mono`
`piiUnionInter` 📖	CompOp	17 math math: `ProbabilityTheory.iIndepSets.piiUnionInter_of_notMem`, `ProbabilityTheory.indepSets_piiUnionInter_of_disjoint`, `ProbabilityTheory.iCondIndepSets.piiUnionInter_of_notMem`, `generateFrom_piiUnionInter_singleton_left`, `ProbabilityTheory.condIndepSets_piiUnionInter_of_disjoint`, `ProbabilityTheory.Kernel.indepSets_piiUnionInter_of_disjoint`, `le_generateFrom_piiUnionInter`, `generateFrom_piiUnionInter_measurableSet`, `generateFrom_piiUnionInter_le`, `piiUnionInter_mono_right`, `mem_piiUnionInter_of_measurableSet`, `isPiSystem_piiUnionInter`, `piiUnionInter_mono_left`, `subset_piiUnionInter`, `piiUnionInter_singleton`, `ProbabilityTheory.Kernel.iIndepSets.piiUnionInter_of_notMem`, `piiUnionInter_singleton_left`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`generateFrom_generatePiSystem_eq` 📖	mathematical	—	`MeasurableSpace.generateFrom` `generatePiSystem`	—	`le_antisymm` `MeasurableSpace.generateFrom_le` `generateFrom_measurableSet_of_generatePiSystem` `MeasurableSpace.measurableSet_generateFrom`
`generateFrom_measurableSet_of_generatePiSystem` 📖	mathematical	`Set` `Set.instMembership` `generatePiSystem`	`MeasurableSet` `MeasurableSpace.generateFrom`	—	`generatePiSystem_measurableSet` `MeasurableSpace.measurableSet_generateFrom`
`generateFrom_piiUnionInter_le` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `MeasurableSpace.generateFrom`	`piiUnionInter`	—	`MeasurableSpace.generateFrom_le` `Finset.measurableSet_biInter` `MeasurableSpace.measurableSet_generateFrom`
`generateFrom_piiUnionInter_measurableSet` 📖	mathematical	—	`MeasurableSpace.generateFrom` `piiUnionInter` `setOf` `Set` `MeasurableSet` `iSup` `MeasurableSpace` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `MeasurableSpace.instCompleteLattice` `Set.instMembership`	—	`le_antisymm` `MeasurableSpace.generateFrom_measurableSet` `MeasurableSpace.generateFrom_mono` `measurableSet_iSup_of_mem_piiUnionInter` `iSup₂_le` `mem_piiUnionInter_of_measurableSet`
`generateFrom_piiUnionInter_singleton_left` 📖	mathematical	—	`MeasurableSpace.generateFrom` `piiUnionInter` `Set` `Set.instSingletonSet` `setOf` `Set.instMembership`	—	`le_antisymm` `MeasurableSpace.generateFrom_le` `Finset.measurableSet_biInter` `MeasurableSpace.measurableSet_generateFrom` `MeasurableSpace.generateFrom_mono` `Finset.mem_singleton` `Finset.mem_coe` `Set.mem_singleton` `Set.iInter_congr_Prop` `Set.iInter_iInter_eq_left`
`generatePiSystem_eq` 📖	mathematical	`IsPiSystem`	`generatePiSystem`	—	`Set.Subset.antisymm` `generatePiSystem_subset_self` `subset_generatePiSystem_self`
`generatePiSystem_measurableSet` 📖	—	`MeasurableSet` `Set` `Set.instMembership` `generatePiSystem`	—	—	`MeasurableSet.inter`
`generatePiSystem_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`generatePiSystem`	—	`Set.mem_of_subset_of_mem` `isPiSystem_generatePiSystem`
`generatePiSystem_subset_self` 📖	mathematical	`IsPiSystem`	`Set` `Set.instHasSubset` `generatePiSystem`	—	—
`isPiSystem_Icc` 📖	mathematical	—	`IsPiSystem` `setOf` `Set` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Icc`	—	`isPiSystem_Ixx` `Set.nonempty_Icc` `Set.Icc_inter_Icc`
`isPiSystem_Icc_mem` 📖	mathematical	—	`IsPiSystem` `setOf` `Set` `Set.instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Icc`	—	`isPiSystem_Ixx_mem` `Set.nonempty_Icc` `Set.Icc_inter_Icc`
`isPiSystem_Ici` 📖	mathematical	—	`IsPiSystem` `Set.range` `Set` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`isPiSystem_image_Ici` `Set.image_univ`
`isPiSystem_Ico` 📖	mathematical	—	`IsPiSystem` `setOf` `Set` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ico`	—	`isPiSystem_Ixx` `LE.le.trans_lt` `Set.Ico_inter_Ico`
`isPiSystem_Ico_mem` 📖	mathematical	—	`IsPiSystem` `setOf` `Set` `Set.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ico`	—	`isPiSystem_Ixx_mem` `LE.le.trans_lt` `Set.Ico_inter_Ico`
`isPiSystem_Iic` 📖	mathematical	—	`IsPiSystem` `Set.range` `Set` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`isPiSystem_image_Iic` `Set.image_univ`
`isPiSystem_Iio` 📖	mathematical	—	`IsPiSystem` `Set.range` `Set` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`isPiSystem_image_Iio` `Set.image_univ`
`isPiSystem_Ioc` 📖	mathematical	—	`IsPiSystem` `setOf` `Set` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioc`	—	`isPiSystem_Ixx` `LT.lt.trans_le` `Set.Ioc_inter_Ioc`
`isPiSystem_Ioc_mem` 📖	mathematical	—	`IsPiSystem` `setOf` `Set` `Set.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioc`	—	`isPiSystem_Ixx_mem` `LT.lt.trans_le` `Set.Ioc_inter_Ioc`
`isPiSystem_Ioi` 📖	mathematical	—	`IsPiSystem` `Set.range` `Set` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`isPiSystem_image_Ioi` `Set.image_univ`
`isPiSystem_Ioo` 📖	mathematical	—	`IsPiSystem` `setOf` `Set` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioo`	—	`isPiSystem_Ixx` `LT.lt.trans` `Set.Ioo_inter_Ioo`
`isPiSystem_Ioo_mem` 📖	mathematical	—	`IsPiSystem` `setOf` `Set` `Set.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioo`	—	`isPiSystem_Ixx_mem` `LT.lt.trans` `Set.Ioo_inter_Ioo`
`isPiSystem_Ixx` 📖	mathematical	`Set` `Set.instInter` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	`IsPiSystem` `setOf`	—	`isPiSystem_Ixx_mem`
`isPiSystem_Ixx_mem` 📖	mathematical	`Set` `Set.instInter` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	`IsPiSystem` `setOf` `Set.instMembership`	—	`sup_ind` `inf_ind`
`isPiSystem_generatePiSystem` 📖	mathematical	—	`IsPiSystem` `generatePiSystem`	—	—
`isPiSystem_iUnion_of_directed_le` 📖	mathematical	`IsPiSystem` `Directed` `Set` `Set.instLE`	`Set.iUnion`	—	`Set.mem_iUnion`
`isPiSystem_iUnion_of_monotone` 📖	mathematical	`IsPiSystem` `Monotone` `Set` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra`	`Set.iUnion`	—	`isPiSystem_iUnion_of_directed_le` `Monotone.directed_le` `SemilatticeSup.instIsDirectedOrder`
`isPiSystem_image_Ici` 📖	mathematical	—	`IsPiSystem` `Set.image` `Set` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`isPiSystem_image_Iic`
`isPiSystem_image_Iic` 📖	mathematical	—	`IsPiSystem` `Set.image` `Set` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`inf_ind` `Set.Iic_inter_Iic`
`isPiSystem_image_Iio` 📖	mathematical	—	`IsPiSystem` `Set.image` `Set` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`inf_ind` `Set.Iio_inter_Iio`
`isPiSystem_image_Ioi` 📖	mathematical	—	`IsPiSystem` `Set.image` `Set` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`isPiSystem_image_Iio`
`isPiSystem_piiUnionInter` 📖	mathematical	`IsPiSystem`	`piiUnionInter`	—	`Finset.coe_union` `Set.ext` `Set.nonempty_iff_ne_empty` `le_antisymm` `Set.iInter_subset_of_subset` `Set.empty_subset` `Set.not_nonempty_iff_eq_empty` `Set.inter_univ` `Set.univ_inter`
`le_generateFrom_piiUnionInter` 📖	mathematical	`Set` `Set.instMembership`	`MeasurableSpace` `MeasurableSpace.instLE` `MeasurableSpace.generateFrom` `piiUnionInter`	—	`MeasurableSpace.generateFrom_mono` `subset_piiUnionInter`
`measurableSet_iSup_of_mem_piiUnionInter` 📖	mathematical	`Set` `Set.instMembership` `piiUnionInter` `setOf` `MeasurableSet`	`iSup` `MeasurableSpace` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `MeasurableSpace.instCompleteLattice`	—	`Finset.measurableSet_biInter` `le_iSup₂`
`mem_generatePiSystem_iUnion_elim` 📖	mathematical	`IsPiSystem` `Set` `Set.instMembership` `generatePiSystem` `Set.iUnion`	`Set.iInter` `Finset` `Finset.instMembership`	—	`Set.iInter_congr_Prop` `Set.iInter_iInter_eq_left` `Set.ext` `Set.Nonempty.mono` `Set.inter_subset_inter` `Set.biInter_subset_of_mem` `Finset.mem_union`
`mem_generatePiSystem_iUnion_elim'` 📖	mathematical	`IsPiSystem` `Set` `Set.instMembership` `generatePiSystem` `Set.iUnion`	`Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Set.iInter` `Finset.instMembership`	—	`Set.ext` `mem_generatePiSystem_iUnion_elim` `Finset.coe_image` `Subtype.coe_preimage_self` `Finset.set_biInter_finset_image` `Function.Injective.extend_apply` `Subtype.val_injective`
`mem_piiUnionInter_of_measurableSet` 📖	mathematical	`Set` `Set.instMembership` `MeasurableSet`	`piiUnionInter` `setOf`	—	`subset_piiUnionInter`
`piiUnionInter_mono_left` 📖	mathematical	`Set` `Set.instHasSubset`	`piiUnionInter`	—	—
`piiUnionInter_mono_right` 📖	mathematical	`Set` `Set.instHasSubset`	`piiUnionInter`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset`
`piiUnionInter_singleton` 📖	mathematical	—	`piiUnionInter` `Set` `Set.instSingletonSet` `Set.instUnion` `Set.univ`	—	`Set.ext` `Finset.ext` `Finset.mem_singleton` `Set.iInter_congr_Prop` `Set.iInter_iInter_eq_left` `Set.iInter_of_empty` `instIsEmptyFalse` `Set.iInter_univ` `Set.mem_singleton` `Finset.coe_singleton` `subset_refl` `Set.instReflSubset` `Finset.coe_empty` `Set.iInter_false`
`piiUnionInter_singleton_left` 📖	mathematical	—	`piiUnionInter` `Set` `Set.instSingletonSet` `setOf` `Finset` `Set.instHasSubset` `SetLike.coe` `Finset.instSetLike` `Set.iInter` `Finset.instMembership`	—	`Set.ext`
`subset_generatePiSystem_self` 📖	mathematical	—	`Set` `Set.instHasSubset` `generatePiSystem`	—	—
`subset_piiUnionInter` 📖	mathematical	`Set` `Set.instMembership`	`Set.instHasSubset` `piiUnionInter`	—	`Set.mem_singleton_iff` `Set.Subset.trans` `piiUnionInter_singleton` `Set.subset_union_left` `piiUnionInter_mono_right`

---

← Back to Index