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, dissipate_mem, 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	70
Total	83

IsPiSystem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biInter_mem 📖	mathematical	IsPiSystem Finset.Nonempty Set Set.instMembership Set.Nonempty Set.iInter Finset SetLike.instMembership Finset.instSetLike	Set Set.instMembership Set.iInter Finset SetLike.instMembership Finset.instSetLike	—	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	IsPiSystem setOf Set Set.instMembership Set.preimage	—	Set.preimage_inter Set.nonempty_of_nonempty_preimage
dissipate_mem 📖	mathematical	IsPiSystem Set Set.instMembership Set.Nonempty Set.dissipate	Set Set.instMembership Set.dissipate	—	Set.dissipate_zero_nat Set.dissipate_succ Set.Nonempty.left
insert_empty 📖	mathematical	IsPiSystem	IsPiSystem Set Set.instInsert Set.instEmptyCollection	—	Set.empty_inter Set.inter_empty Set.mem_insert_of_mem
insert_univ 📖	mathematical	IsPiSystem	IsPiSystem Set Set.instInsert Set.univ	—	Set.inter_self Set.univ_inter Set.inter_univ Set.mem_insert_of_mem
prod 📖	mathematical	IsPiSystem	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	12 math math: ext_iff, has_compl, generate_inter, has_compl_iff, has_union, has_iUnion_nat, has_diff, has_iUnion, has_univ, has_empty, le_def, generateHas_def
generate 📖	CompOp	4 math math: generate_inter, 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	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	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	Has Set 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	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	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	Has Set 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	41 math math: isPiSystem_Ixx, isPiSystem_prod, isPiSystem_image_Iic, isPiSystem_iUnion_of_directed_le, MeasurableSpace.isPiSystem_measurableSet, IsPiSystem.insert_empty, isPiSystem_Ioi, isPiSystem_image_Ioi, isPiSystem_iUnion_of_monotone, IsPiSystem.pi, 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.comap, isPiSystem_isClosed, isPiSystem_Ico, IsPiSystem.singleton, isPiSystem_image_Iio, isPiSystem_piiUnionInter, isPiSystem_Iio, IsPiSystem.prod, isPiSystem_Ixx_mem, IsPiSystem.insert_univ, isPiSystem_Ioc_mem, MeasureTheory.isPiSystem_squareCylinders, 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	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 📖	mathematical	MeasurableSet Set Set.instMembership generatePiSystem	MeasurableSet	—	MeasurableSet.inter
generatePiSystem_mono 📖	mathematical	Set Set.instHasSubset	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 Set	—	isPiSystem_Ixx_mem
isPiSystem_Ixx_mem 📖	mathematical	Set Set.instInter SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	IsPiSystem setOf Set Set.instMembership	—	sup_ind inf_ind
isPiSystem_generatePiSystem 📖	mathematical	—	IsPiSystem generatePiSystem	—	—
isPiSystem_iUnion_of_directed_le 📖	mathematical	IsPiSystem Directed Set Set.instLE	IsPiSystem Set.iUnion Set	—	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	IsPiSystem Set.iUnion Set	—	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	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	MeasurableSet iSup MeasurableSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice Set Set.instMembership	—	Finset.measurableSet_biInter le_iSup₂
mem_generatePiSystem_iUnion_elim 📖	mathematical	IsPiSystem Set Set.instMembership generatePiSystem Set.iUnion	Finset Set.iInter SetLike.instMembership Finset.instSetLike Set Set.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	Finset Set Set.instHasSubset SetLike.coe Finset.instSetLike Set.iInter SetLike.instMembership Set.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	Set Set.instMembership piiUnionInter setOf MeasurableSet	—	subset_piiUnionInter
piiUnionInter_mono_left 📖	mathematical	Set Set.instHasSubset	Set Set.instHasSubset piiUnionInter	—	—
piiUnionInter_mono_right 📖	mathematical	Set Set.instHasSubset	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 SetLike.instMembership	—	Set.ext
subset_generatePiSystem_self 📖	mathematical	—	Set Set.instHasSubset generatePiSystem	—	—
subset_piiUnionInter 📖	mathematical	Set Set.instMembership	Set Set.instHasSubset piiUnionInter	—	Set.mem_singleton_iff Set.Subset.trans piiUnionInter_singleton Set.subset_union_left piiUnionInter_mono_right

---

← Back to Index