Defs

📁 Source: Mathlib/MeasureTheory/MeasurableSpace/Defs.lean

Statistics

Metric	Count
Definitions DiscreteMeasurableSpace, MeasurableSet, MeasurableSingletonClass, GenerateMeasurable, MeasurableSet', copy, generateFrom, giGenerateFrom, instCompleteLattice, instInhabited, instLE, instPartialOrder, mkOfClosure, «termMeasurableSet[_]», «termMeasurable[_,_]», «termMeasurable[_]», instMeasurableSpaceOrderDual	17
Theorems forall_measurableSet, toMeasurableSingletonClass, measurableSet, measurableSet_biInter, measurableSet_biUnion, comp, comp', fun_comp, le, of_discrete, biInter, biUnion, bihimp, compl, compl_iff, cond, const, diff, empty, himp, iInter, iUnion, iff, imp, insert, inter, ite, ite', of_compl, of_discrete, sInter, sUnion, singleton, symmDiff, union, univ, measurableSet_singleton, toDiscreteMeasurableSpace, copy_eq, ext, ext_iff, forall_generateFrom_mem_iff_mem_iff, generateFrom_empty, generateFrom_iUnion_measurableSet, generateFrom_induction, generateFrom_insert_empty, generateFrom_insert_univ, generateFrom_le, generateFrom_le_iff, generateFrom_measurableSet, generateFrom_mono, generateFrom_singleton_empty, generateFrom_singleton_univ, generateFrom_sup_generateFrom, iSup_generateFrom, le_def, measurableSet_bot_iff, measurableSet_compl, measurableSet_copy, measurableSet_empty, measurableSet_generateFrom, measurableSet_iInf, measurableSet_iSup, measurableSet_iUnion, measurableSet_inf, measurableSet_injective, measurableSet_sInf, measurableSet_sSup, measurableSet_sup, measurableSet_top, measurableSpace_iSup_eq, mkOfClosure_sets, measurableSet, measurableSet, measurableSet_biInter, measurableSet_biUnion, measurableSet_sInter, measurableSet_sUnion, measurableSet, measurableSet, instDiscreteMeasurableSpace, measurableSet_eq, measurableSet_insert, measurable_const, measurable_id, measurable_id', nonempty_measurable_superset	87
Total	104

DiscreteMeasurableSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forall_measurableSet 📖	mathematical	—	MeasurableSet	—	—
toMeasurableSingletonClass 📖	mathematical	—	MeasurableSingletonClass	—	MeasurableSet.of_discrete

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableSet 📖	mathematical	—	MeasurableSet SetLike.coe Finset instSetLike	—	Set.Finite.measurableSet finite_toSet
measurableSet_biInter 📖	mathematical	MeasurableSet	MeasurableSet Set.iInter Finset SetLike.instMembership instSetLike	—	Set.Finite.measurableSet_biInter finite_toSet
measurableSet_biUnion 📖	mathematical	MeasurableSet	MeasurableSet Set.iUnion Finset SetLike.instMembership instSetLike	—	Set.Finite.measurableSet_biUnion finite_toSet

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	Measurable	Measurable	—	—
comp' 📖	mathematical	Measurable	Measurable	—	fun_comp
fun_comp 📖	mathematical	Measurable	Measurable	—	comp
le 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measurable	Measurable	—	—
of_discrete 📖	mathematical	—	Measurable	—	MeasurableSet.of_discrete

MeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biInter 📖	mathematical	MeasurableSet	MeasurableSet Set.iInter Set Set.instMembership	—	of_compl Set.compl_iInter₂ biUnion compl
biUnion 📖	mathematical	MeasurableSet	MeasurableSet Set.iUnion Set Set.instMembership	—	Set.biUnion_eq_iUnion Set.Countable.to_subtype iUnion
bihimp 📖	mathematical	MeasurableSet	MeasurableSet bihimp Set SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instHImp	—	inter himp
compl 📖	mathematical	MeasurableSet	MeasurableSet Compl.compl Set Set.instCompl	—	MeasurableSpace.measurableSet_compl
compl_iff 📖	mathematical	—	MeasurableSet Compl.compl Set Set.instCompl	—	of_compl compl
cond 📖	mathematical	MeasurableSet	MeasurableSet Set	—	—
const 📖	mathematical	—	MeasurableSet setOf	—	—
diff 📖	mathematical	MeasurableSet	MeasurableSet Set Set.instSDiff	—	inter compl
empty 📖	mathematical	—	MeasurableSet Set Set.instEmptyCollection	—	MeasurableSpace.measurableSet_empty
himp 📖	mathematical	MeasurableSet	MeasurableSet HImp.himp Set Set.instHImp	—	himp_eq union compl
iInter 📖	mathematical	MeasurableSet	MeasurableSet Set.iInter	—	of_compl Set.compl_iInter iUnion compl
iUnion 📖	mathematical	MeasurableSet	MeasurableSet Set.iUnion	—	isEmpty_or_nonempty Set.iUnion_of_empty exists_surjective_nat Set.iUnion_congr_of_surjective MeasurableSpace.measurableSet_iUnion
iff 📖	mathematical	MeasurableSet setOf	MeasurableSet setOf	—	Set.ext inter imp
imp 📖	mathematical	MeasurableSet setOf	MeasurableSet setOf	—	union compl
insert 📖	mathematical	MeasurableSet	MeasurableSet Set Set.instInsert	—	union singleton
inter 📖	mathematical	MeasurableSet	MeasurableSet Set Set.instInter	—	Set.inter_eq_compl_compl_union_compl compl union
ite 📖	mathematical	MeasurableSet	MeasurableSet Set.ite	—	union inter diff
ite' 📖	mathematical	MeasurableSet	MeasurableSet Set	—	—
of_compl 📖	mathematical	MeasurableSet Compl.compl Set Set.instCompl	MeasurableSet	—	compl compl_compl
of_discrete 📖	mathematical	—	MeasurableSet	—	DiscreteMeasurableSpace.forall_measurableSet
sInter 📖	mathematical	MeasurableSet	MeasurableSet Set.sInter	—	Set.sInter_eq_biInter biInter
sUnion 📖	mathematical	MeasurableSet	MeasurableSet Set.sUnion	—	Set.sUnion_eq_biUnion biUnion
singleton 📖	mathematical	—	MeasurableSet Set Set.instSingletonSet	—	MeasurableSingletonClass.measurableSet_singleton
symmDiff 📖	mathematical	MeasurableSet	MeasurableSet symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff	—	union diff
union 📖	mathematical	MeasurableSet	MeasurableSet Set Set.instUnion	—	Set.union_eq_iUnion iUnion Bool.countable
univ 📖	mathematical	—	MeasurableSet Set.univ	—	of_compl Set.compl_univ

MeasurableSingletonClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableSet_singleton 📖	mathematical	—	MeasurableSet Set Set.instSingletonSet	—	—
toDiscreteMeasurableSpace 📖	mathematical	—	DiscreteMeasurableSpace	—	Set.Countable.measurableSet Set.to_countable SetCoe.countable

MeasurableSpace

Definitions

Name	Category	Theorems
GenerateMeasurable 📖	CompData	7 math math: measurableSet_sSup, cardinal_generateMeasurable_le_continuum, cardinal_generateMeasurable_le, generateMeasurableRec_subset, measurableSet_sup, measurableSet_iSup, generateMeasurable_eq_rec
MeasurableSet' 📖	MathDef	4 math math: measurableSet_empty, measurableSet_compl, le_def, measurableSet_iUnion
copy 📖	CompOp	2 math math: copy_eq, measurableSet_copy
generateFrom 📖	CompOp	107 math math: comap_eq_generateFrom, ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_of_disjoint, ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_of_disjoint, generateFrom_piiUnionInter_singleton_left, ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_le_nat, ProbabilityTheory.IndepSets.indep', borel_eq_generateFrom_isClosed, ProbabilityTheory.condIndepSet_iff_condIndep, generateFrom_empty, MeasureTheory.AddContent.measure_eq, MeasureTheory.measurableSet_generateFrom_singleton_iff, borel_eq_generateFrom_Ici, Real.borel_eq_generateFrom_Iio_rat, ProbabilityTheory.iCondIndepSet_iff_iCondIndep, generateFrom_eq_pi, Real.borel_eq_generateFrom_Ioo_rat, borel_eq_generateFrom_of_subbasis, ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_le, generateFrom_iUnion_measurableSet, generateFrom_Icc_mem_le_borel, generateFrom_sup_generateFrom, generateFrom_memPartition_le, ProbabilityTheory.IndepSet_iff_Indep, generateFrom_pi_eq, borel_eq_generateFrom_Icc, ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_lt, ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_lt, generateFrom_Ico_mem_le_borel, ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_le_nat, measurableSet_generateFrom, Real.borel_eq_generateFrom_Ioi_rat, measurableSet_succ_countablePartition, generateFrom_measurableSet, generateFrom_prod, ProbabilityTheory.iIndepSet.indep_generateFrom_le, borel_eq_generateFrom_Ioc, MeasureTheory.generateFrom_generateSetAlgebra_eq, le_generateFrom_piiUnionInter, measurableSpace_iSup_eq, ProbabilityTheory.condExp_set_generateFrom_singleton, ProbabilityTheory.condExp_generateFrom_singleton, Real.borel_eq_generateFrom_Ici_rat, generateFrom_singleton_univ, generateFrom_piiUnionInter_measurableSet, ProbabilityTheory.condExpKernel_singleton_ae_eq_cond, ProbabilityTheory.iIndepSet.indep_generateFrom_lt, generateFrom_mono, measurable_generateFrom, Dense.borel_eq_generateFrom_Ico_mem, ProbabilityTheory.iSup_partitionFiltration_eq_generateFrom_range, ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_le, generateFrom_natGeneratingSequence, measurableSet_generateFrom_memPartition_iff, cardinal_measurableSet_le_continuum, measurableSet_generateFrom_memPartition, measurableSet_generateFrom_countablePartition_iff, generateFrom_iUnion_countablePartition, Dense.borel_eq_generateFrom_Ico_mem_aux, generateFrom_insert_univ, generateFrom_piiUnionInter_le, generateFrom_memPartition_le_range, CountablyGenerated.isCountablyGenerated, generateFrom_countablePartition_le, generateFrom_prod_eq, Dense.borel_eq_generateFrom_Ioc_mem_aux, borel_eq_generateFrom_Ico, cardinal_measurableSet_le, generateFrom_countableGeneratingSet, generateFrom_eq_prod, generateFrom_singleton, generateFrom_pi, ProbabilityTheory.iIndepSet_iff_iIndep, MeasureTheory.generateFrom_squareCylinders, ProbabilityTheory.iIndepSet.indep_generateFrom_le_nat, generateFrom_iUnion_memPartition, MeasureTheory.comap_eval_le_generateFrom_squareCylinders_singleton, generateFrom_measurableSet_of_generatePiSystem, borel_eq_generateFrom_Ioc_le, generateFrom_memPartition_le_succ, borel_eq_generateFrom_Ioi, generateFrom_countablePartition_le_succ, generateFrom_singleton_le, iSup_generateFrom, borel_eq_generateFrom_Iio, generateFrom_generatePiSystem_eq, DynkinSystem.generateFrom_eq, generateFrom_iUnion_memPartition_le, MeasureTheory.generateFrom_measurableCylinders, ProbabilityTheory.Kernel.IndepSets.indep', generateFrom_insert_empty, ProbabilityTheory.CondIndepSets.condIndep', borel_eq_generateFrom_Iic, Real.borel_eq_generateFrom_Iic_rat, comap_generateFrom, pi_eq_generateFrom_projections, measurableSet_succ_memPartition, mkOfClosure_sets, Dense.borel_eq_generateFrom_Ioc_mem, generateFrom_le_iff, ProbabilityTheory.iIndepSet.indep_generateFrom_of_disjoint, Dense.borel_eq_generateFrom_Icc_mem, DynkinSystem.generate_has_subset_generate_measurable, TopologicalSpace.IsTopologicalBasis.borel_eq_generateFrom, measurableSet_generateFrom_of_mem_supClosure, Dense.borel_eq_generateFrom_Icc_mem_aux, generateFrom_le, generateFrom_singleton_empty
giGenerateFrom 📖	CompOp	—
instCompleteLattice 📖	CompOp	123 math math: measurable_from_top, comap_const, comap_bot, ProbabilityTheory.condIndep_iSup_of_antitone, ProbabilityTheory.Kernel.indep_iSup_directed_limsup, ProbabilityTheory.indep_iSup_of_monotone, ProbabilityTheory.indep_limsup_atTop_self, generateFrom_empty, MeasureTheory.condLExp_bot', Measurable.sup_of_right, ProbabilityTheory.condIndep_bot_left, ProbabilityTheory.condIndep_iSup_of_monotone, measurableSet_iInf, measurableSet_sSup, ProbabilityTheory.Kernel.indep_limsup_atBot_self, map_const, ProbabilityTheory.indep_biSup_limsup, MeasureTheory.OuterMeasure.le_sum_caratheodory, generateFrom_iUnion_measurableSet, ProbabilityTheory.Kernel.indep_iSup_limsup, PMF.toOuterMeasure_caratheodory, ProbabilityTheory.indep_iSup_of_directed_le, MeasureTheory.condLExp_bot, generateFrom_sup_generateFrom, ProbabilityTheory.condIndep_limsup_atTop_self, ProbabilityTheory.Kernel.indep_limsup_self, map_inf, ProbabilityTheory.condExpKernel_ae_eq_condExp', borel_eq_top_of_discrete, ProbabilityTheory.iIndep_comap_mem_iff, MeasureTheory.OuterMeasure.le_add_caratheodory, ProbabilityTheory.indep_iSup_limsup, measurableSet_bot_iff, MeasureTheory.Filtration.rightCont_apply, MeasureTheory.OuterMeasure.zero_caratheodory, comap_prodMk, MeasureTheory.OuterMeasure.top_caratheodory, measurableSpace_iSup_eq, ProbabilityTheory.iIndepSet.iIndep_comap_mem, ProbabilityTheory.Kernel.IsProper.restrict_eq_indicator_smul', MeasureTheory.condExp_bot, generateFrom_singleton_univ, MeasureTheory.Filtration.rightCont_def, generateFrom_piiUnionInter_measurableSet, ProbabilityTheory.condIndep_iSup_limsup, ProbabilityTheory.Kernel.iIndep_comap_mem_iff, MeasureTheory.StronglyMeasurable.integral_condExpKernel', ProbabilityTheory.Kernel.indep_iSup_of_directed_le, ProbabilityTheory.condExp_ae_eq_integral_condExpKernel', CountablyGenerated.sup, ProbabilityTheory.Kernel.indep_iSup_of_monotone, MeasureTheory.IsStoppingTime.measurableSpace_min, MeasureTheory.Filtration.rightCont_eq_of_not_isMax, MeasureTheory.tendsto_ae_condExp, ProbabilityTheory.indep_iSup_directed_limsup, ProbabilityTheory.iSup_partitionFiltration_eq_generateFrom_range, ProbabilityTheory.condIndep_biSup_limsup, ProbabilityTheory.condIndep_limsup_self, ProbabilityTheory.condExpKernel_def, MeasureTheory.SimpleFunc.simpleFunc_bot', comap_iSup, MeasureTheory.IsStoppingTime.measurableSpace_min_const, ProbabilityTheory.Kernel.indep_biSup_limsup, MeasureTheory.sigmaFinite_bot_iff, inf_le_invariants_comp, ProbabilityTheory.indep_limsup_atBot_self, Measurable.iSup', MeasureTheory.tendsto_eLpNorm_condExp, MeasureTheory.condLExp_bot_ae_eq, ProbabilityTheory.iSup_countableFiltration, ProbabilityTheory.indep_iSup_of_antitone, MeasureTheory.Filtration.rightCont_eq, ProbabilityTheory.condIndep_biSup_compl, map_iInf, ProbabilityTheory.condIndep_iSup_directed_limsup, MeasureTheory.Filtration.coeFn_sup, ProbabilityTheory.condVar_bot', ProbabilityTheory.Kernel.indep_limsup_atTop_self, comap_sup, ProbabilityTheory.Kernel.indep_iSup_of_antitone, Measurable.sup_of_left, measurableSet_sInf, ProbabilityTheory.condIndep_bot_right, generateFrom_singleton, ProbabilityTheory.indep_bot_right, ProbabilityTheory.condVar_bot_ae_eq, ProbabilityTheory.indep_bot_left, MeasureTheory.Filtration.sSup_def, instDiscreteMeasurableSpace, MeasureTheory.SimpleFunc.simpleFunc_bot, ProbabilityTheory.condVar_bot, ProbabilityTheory.indep_biSup_compl, ProbabilityTheory.condExpKernel_eq, stronglyMeasurable_bot_iff, map_top, iSup_generateFrom, ProbabilityTheory.condIndep_iSup_of_disjoint, borel_eq_top_of_countable, ProbabilityTheory.iSup_partitionFiltration, measurableSet_top, ProbabilityTheory.Kernel.indep_bot_left, MeasureTheory.sigmaFinite_trim_bot_iff, ProbabilityTheory.condIndep_limsup_atBot_self, MeasureTheory.condExp_bot', ProbabilityTheory.Kernel.indep_bot_right, MeasureTheory.OuterMeasure.dirac_caratheodory, MeasureTheory.Submartingale.exists_ae_trim_tendsto_of_bdd, MeasureTheory.Filtration.rightCont_eq_of_neBot_nhdsGT, ProbabilityTheory.condIndep_iSup_of_directed_le, MeasureTheory.Filtration.coeFn_inf, ProbabilityTheory.Kernel.indep_biSup_compl, measurableSet_inf, measurableSet_sup, ProbabilityTheory.indep_iSup_of_disjoint, ProbabilityTheory.Kernel.indep_iSup_of_disjoint, measurableSet_iSup_of_mem_piiUnionInter, generateFrom_singleton_empty, MeasureTheory.condExp_bot_ae_eq, ProbabilityTheory.indep_limsup_self, MeasureTheory.Filtration.stronglyMeasurable_limitProcess, measurableSet_iSup, MeasureTheory.Filtration.sInf_def, ProbabilityTheory.condExpKernel_apply_eq_condDistrib
instInhabited 📖	CompOp	—
instLE 📖	CompOp	58 math math: MeasureTheory.OuterMeasure.IsMetric.borel_le_caratheodory, MeasureTheory.OuterMeasure.IsMetric.le_caratheodory, comap_mono, map_mono, exists_countablyGenerated_le_of_countablySeparated, OpensMeasurableSpace.borel_le, le_eventuallyMeasurableSpace, MeasureTheory.OuterMeasure.le_sum_caratheodory, MeasureTheory.IsStoppingTime.measurableSpace_le_of_le_const, generateFrom_Icc_mem_le_borel, invariants_le, Measurable.comap_le, generateFrom_memPartition_le, generateFrom_Ico_mem_le_borel, Measurable.le_map, MeasureTheory.IsStoppingTime.measurableSpace_mono, MeasureTheory.cylinderEvents_mono, StieltjesFunction.borel_le_measurable, MeasureTheory.OuterMeasure.le_add_caratheodory, le_generateFrom_piiUnionInter, MeasureTheory.IsStoppingTime.measurableSpace_le, MeasureTheory.Measure.pi_caratheodory, MeasureTheory.condExp_def, measurable_iff_comap_le, MeasureTheory.Filtration.le', generateFrom_mono, MeasureTheory.OuterMeasure.le_smul_caratheodory, generateFrom_piiUnionInter_le, generateFrom_memPartition_le_range, inf_le_invariants_comp, generateFrom_countablePartition_le, pi_le_borel_pi, le_def, MeasureTheory.cylinderEvents_le_pi, MeasureTheory.Content.borel_le_caratheodory, MeasureTheory.measurableSpace_le_predictable_of_measurableSet, MeasureTheory.Filtration.mono, MeasureTheory.Filtration.le, comap_le_iff_le_map, le_invariants_iterate, measurable_iff_le_map, MeasureTheory.comap_eval_le_generateFrom_squareCylinders_singleton, comap_map_le, generateFrom_memPartition_le_succ, generateFrom_countablePartition_le_succ, generateFrom_singleton_le, MeasureTheory.condLExp_def, prod_le_borel_prod, MeasureTheory.sigmaFinite_trim_bot_iff, MeasureTheory.le_toOuterMeasure_caratheodory, generateFrom_iUnion_memPartition_le, le_map_comap, comap_le_comap_pi, generateFrom_le_iff, MeasureTheory.IsStoppingTime.le_measurableSpace_of_const_le, DynkinSystem.ofMeasurableSpace_le_ofMeasurableSpace_iff, generateFrom_le, MeasureTheory.IsStoppingTime.measurableSpace_le_of_le
instPartialOrder 📖	CompOp	9 math math: MeasureTheory.AddContent.measure_eq, MeasureTheory.VectorMeasure.trim_eq_self, MeasureTheory.trim_eq_self, gc_comap_map, MeasureTheory.trim_trim, borel_anti, MeasureTheory.Filtration.mono', monotone_map, monotone_comap
mkOfClosure 📖	CompOp	1 math math: mkOfClosure_sets

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
copy_eq 📖	mathematical	MeasurableSet	copy	—	ext
ext 📖	—	MeasurableSet	—	—	measurableSet_injective
ext_iff 📖	mathematical	—	MeasurableSet	—	ext
forall_generateFrom_mem_iff_mem_iff 📖	mathematical	—	Set Set.instMembership	—	generateFrom_induction Iff.not
generateFrom_empty 📖	mathematical	—	generateFrom Set Set.instEmptyCollection Bot.bot MeasurableSpace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	le_bot_iff generateFrom_le instIsEmptyFalse
generateFrom_iUnion_measurableSet 📖	mathematical	—	generateFrom Set.iUnion Set setOf MeasurableSet iSup MeasurableSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	GaloisInsertion.l_iSup_u
generateFrom_induction 📖	—	Set Set.instEmptyCollection measurableSet_empty generateFrom Compl.compl Set.instCompl MeasurableSet.compl Set.iUnion MeasurableSet.iUnion instCountableNat MeasurableSet	—	—	measurableSet_empty MeasurableSet.compl MeasurableSet.iUnion instCountableNat
generateFrom_insert_empty 📖	mathematical	—	generateFrom Set Set.instInsert Set.instEmptyCollection	—	Set.insert_eq generateFrom_sup_generateFrom generateFrom_singleton_empty bot_sup_eq
generateFrom_insert_univ 📖	mathematical	—	generateFrom Set Set.instInsert Set.univ	—	Set.insert_eq generateFrom_sup_generateFrom generateFrom_singleton_univ bot_sup_eq
generateFrom_le 📖	mathematical	MeasurableSet	MeasurableSpace instLE generateFrom	—	MeasurableSet.empty MeasurableSet.compl MeasurableSet.iUnion instCountableNat
generateFrom_le_iff 📖	mathematical	—	MeasurableSpace instLE generateFrom Set Set.instHasSubset setOf MeasurableSet	—	measurableSet_generateFrom generateFrom_le
generateFrom_measurableSet 📖	mathematical	—	generateFrom setOf Set MeasurableSet	—	le_antisymm generateFrom_le measurableSet_generateFrom
generateFrom_mono 📖	mathematical	Set Set.instHasSubset	MeasurableSpace instLE generateFrom	—	GaloisConnection.monotone_l GaloisInsertion.gc
generateFrom_singleton_empty 📖	mathematical	—	generateFrom Set Set.instSingletonSet Set.instEmptyCollection Bot.bot MeasurableSpace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	bot_unique generateFrom_le MeasurableSet.empty
generateFrom_singleton_univ 📖	mathematical	—	generateFrom Set Set.instSingletonSet Set.univ Bot.bot MeasurableSpace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	bot_unique generateFrom_le
generateFrom_sup_generateFrom 📖	mathematical	—	MeasurableSpace SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice generateFrom Set Set.instUnion	—	GaloisConnection.l_sup GaloisInsertion.gc
iSup_generateFrom 📖	mathematical	—	iSup MeasurableSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice generateFrom Set.iUnion Set	—	GaloisConnection.l_iSup GaloisInsertion.gc
le_def 📖	mathematical	—	MeasurableSpace instLE Pi.hasLe Set Prop.le MeasurableSet'	—	—
measurableSet_bot_iff 📖	mathematical	—	MeasurableSet Bot.bot MeasurableSpace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Set Set.instEmptyCollection Set.univ	—	Set.sUnion_mem_empty_univ Set.forall_mem_range bot_unique measurableSet_empty MeasurableSet.univ
measurableSet_compl 📖	mathematical	MeasurableSet'	MeasurableSet' Compl.compl Set Set.instCompl	—	—
measurableSet_copy 📖	mathematical	MeasurableSet	MeasurableSet copy	—	—
measurableSet_empty 📖	mathematical	—	MeasurableSet' Set Set.instEmptyCollection	—	—
measurableSet_generateFrom 📖	mathematical	Set Set.instMembership	MeasurableSet generateFrom	—	—
measurableSet_iInf 📖	mathematical	—	MeasurableSet iInf MeasurableSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	iInf.eq_1 measurableSet_sInf Set.forall_mem_range
measurableSet_iSup 📖	mathematical	—	MeasurableSet iSup MeasurableSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice GenerateMeasurable setOf Set	—	—
measurableSet_iUnion 📖	mathematical	MeasurableSet'	MeasurableSet' Set.iUnion	—	—
measurableSet_inf 📖	mathematical	—	MeasurableSet MeasurableSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	—
measurableSet_injective 📖	mathematical	—	MeasurableSpace MeasurableSet	—	—
measurableSet_sInf 📖	mathematical	—	MeasurableSet InfSet.sInf MeasurableSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	Set.sInter_image
measurableSet_sSup 📖	mathematical	—	MeasurableSet SupSet.sSup MeasurableSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice GenerateMeasurable setOf Set Set.instMembership	—	Set.sUnion_image
measurableSet_sup 📖	mathematical	—	MeasurableSet MeasurableSpace SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice GenerateMeasurable setOf Set	—	—
measurableSet_top 📖	mathematical	—	MeasurableSet Top.top MeasurableSpace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
measurableSpace_iSup_eq 📖	mathematical	—	iSup MeasurableSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice generateFrom setOf Set MeasurableSet	—	ext measurableSet_iSup
mkOfClosure_sets 📖	mathematical	setOf Set MeasurableSet generateFrom	mkOfClosure generateFrom	—	copy_eq

MeasureTheory

Definitions

Name	Category	Theorems
«termMeasurableSet[_]» 📖	CompOp	—
«termMeasurable[_,_]» 📖	CompOp	—
«termMeasurable[_]» 📖	CompOp	—

Set.Countable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableSet 📖	mathematical	—	MeasurableSet	—	Set.biUnion_of_singleton MeasurableSet.biUnion MeasurableSet.singleton

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableSet 📖	mathematical	—	MeasurableSet	—	induction_on MeasurableSet.empty MeasurableSet.insert
measurableSet_biInter 📖	mathematical	MeasurableSet	MeasurableSet Set.iInter Set Set.instMembership	—	MeasurableSet.biInter countable
measurableSet_biUnion 📖	mathematical	MeasurableSet	MeasurableSet Set.iUnion Set Set.instMembership	—	MeasurableSet.biUnion countable
measurableSet_sInter 📖	mathematical	MeasurableSet	MeasurableSet Set.sInter	—	MeasurableSet.sInter countable
measurableSet_sUnion 📖	mathematical	MeasurableSet	MeasurableSet Set.sUnion	—	MeasurableSet.sUnion countable

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableSet 📖	mathematical	Set.Subsingleton	MeasurableSet	—	induction_on MeasurableSet.empty MeasurableSet.singleton

Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableSet 📖	mathematical	—	MeasurableSet	—	set_cases MeasurableSet.empty MeasurableSet.univ

(root)

Definitions

Name	Category	Theorems
DiscreteMeasurableSpace 📖	CompData	10 math math: Submodule.Quotient.instDiscreteMeasurableSpaceQuotient, QuotientGroup.instDiscreteMeasurableSpace, IterateAddAct.instDiscreteMeasurableSpace, MeasurableSingletonClass.toDiscreteMeasurableSpace, AddChar.instDiscreteMeasurableSpace, QuotientAddGroup.instDiscreteMeasurableSpace, ENat.instDiscreteMeasurableSpace, instDiscreteMeasurableSpace, Quotient.instDiscreteMeasurableSpace, IterateMulAct.instDiscreteMeasurableSpace
MeasurableSet 📖	MathDef	480 math math: Filter.Eventually.exists_measurable_mem_of_smallSets, MeasurableSpace.comap_eq_generateFrom, MeasureTheory.IsStoppingTime.measurableSet_inter_le_iff, MeasurableSet.sep_infinite, Subsingleton.measurableSet, MeasureTheory.measurableSet_sigmaFiniteSetGE, MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range, MeasureTheory.measurableSet_range_of_continuous_injective, MeasurableSet.image_of_measurable_injOn, MeasurableSet.preimage, MeasurableSet.diff, measurableSet_inr_image, IsFoelner.eventually_measurableSet, isPiSystem_prod, MeasureTheory.extend_iUnion_le_tsum_nat, ZSpan.fundamentalDomain_measurableSet, measurableSet_pi_of_nonempty, generatePiSystem_measurableSet, RightDerivMeasurableAux.measurableSet_B, MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable', Set.OrdConnected.measurableSet, MeasurableSet.of_compl, MeasureTheory.exists_decomposition_of_monotoneOn_hasDerivWithinAt, MeasureTheory.FinStronglyMeasurable.exists_set_sigmaFinite, MeasureTheory.OuterMeasure.boundedBy_caratheodory, MeasureTheory.IsStoppingTime.measurableSet, MeasureTheory.IsStoppingTime.measurableSet_gt, ae_eq_const_or_exists_average_ne_compl, MeasureTheory.measurableSet_exists_tendsto, nonempty_measurable_superset, BoxIntegral.Box.measurableSet_Icc, MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range', MeasureTheory.finStronglyMeasurable_iff_stronglyMeasurable_and_exists_set_sigmaFinite, MeasurableSpace.isPiSystem_measurableSet, MeasureTheory.measurableSet_predictable_Ioi_prod, measurableSet_mulSupport, MeasurableSet.singleton, NumberField.mixedEmbedding.measurableSet_plusPart, MeasureTheory.SeparableSpace.exists_measurable_partition_diam_le, Set.Finite.measurableSet_sUnion, MeasurableSpace.map_def, MeasurableSet.cond, MeasurableEmbedding.measurableSet_image, MeasurableSet.image_fract, MeasureTheory.SignedMeasure.exists_compl_positive_negative, MeasureTheory.Measure.InnerRegularWRT.restrict, MeasureTheory.measurableSet_tendsto_fun, ProbabilityTheory.iIndep_iff_iIndepSets, MeasureTheory.measurableSet_generateFrom_singleton_iff, MeasurableSet.image_of_monotoneOn_of_continuousOn, MeasurableSet.of_discrete, ProbabilityTheory.Kernel.iIndep.iIndepSets', measurableSet_setOf, MeasureTheory.exists_measurable_superset₂, MeasurableSet.ite', MeasurableSet.everywherePosSubset, exists_partition_approximatesLinearOn_of_hasFDerivWithinAt, BoxIntegral.Box.measurableSet_coe, measurableSet_support, MeasureTheory.inducedOuterMeasure_caratheodory, MeasureTheory.exists_null_pairwise_disjoint_diff, measurableSet_graph, measurableSet_le, measurableSet_eq_fun, measurableSet_eq_fun', MeasurableSpace.measurableSet_iInf, MeasurableSet.empty, MeasureTheory.IsStoppingTime.measurableSet_ge', isCountablySpanning_measurableSet, MeasurableSpace.measurableSet_sSup, MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable, DiscreteMeasurableSpace.forall_measurableSet, MeasureTheory.Measure.toENNRealVectorMeasure_apply, MeasurableSingletonClass.measurableSet_singleton, MeasurableSpace.countablySeparated_def, MeasurableSet.congr, MeasureTheory.IsStoppingTime.measurableSet_lt_of_isLUB, measurableSet_Ico, MeasurableEmbedding.measurableSet_preimage, Set.Finite.measurableSet_biInter, MeasurableSet.sUnion, MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time, MeasureTheory.Measure.sInf_caratheodory, measurable_mem, measurableSet_Iio, MeasureTheory.exists_isSigmaFiniteSet_measure_ge, MeasureTheory.SignedMeasure.exists_isCompl_positive_negative, MeasureTheory.Measure.exists_subset_measure_lt_top, MeasurableSet.of_mem_measurableCylinders, MeasureTheory.measure_sigmaFiniteSetGE_le, MeasureTheory.OuterMeasure.isCaratheodory_iff, MeasurableSet.subtype_bot_eq, MeasurableSpace.generateFrom_iUnion_measurableSet, MeasurableSet.compl_iff, MeasurableSpace.measurableSet_countableGeneratingSet, MeasurableSet.sInter, ENat.measurable_iff, MeasureTheory.StronglyMeasurable.measurableSet_exists_tendsto, MeasurableSet.coe_union, measurableSet_closure, Filter.principal_isMeasurablyGenerated_iff, MeasurableSet.coe_singleton, Set.Finite.measurableSet_biUnion, MeasureTheory.IsStoppingTime.measurableSet_inter_le_const_iff, Set.Countable.measurableSet, MeasurableSet.of_union₃_range_cover, MeasurableSpace.measurableSet_invariants, MeasureTheory.VectorMeasure.measurable_of_not_zero_le_restrict, MeasureTheory.measurableSet_predictable_singleton_bot_prod, MeasureTheory.exists_subset_real_measurableEquiv, measurableSet_preimage_down, MeasureTheory.IsStoppingTime.measurableSet_eq_stopping_time_min, MeasurableSpace.measurableSet_enumerateCountable_countableGeneratingSet, MeasurableSet.setOf_finite, MeasurableSet.tProd, MeasurableSpace.measurableSet_generateFrom, MeasureTheory.OuterMeasure.trim_eq_iInf', measurableSet_of_differentiableAt_of_isComplete, MeasureTheory.hahn_decomposition, MeasurableEmbedding.measurableSet_image', MeasureTheory.Measure.innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_group, Measurable.setOf, MeasureTheory.IsStoppingTime.measurableSet_lt, ProbabilityTheory.measurableSet_partitionFiltration_of_mem, IsAddFoelner.eventually_measurableSet, MeasureTheory.StronglyMeasurable.measurableSet_lt, Measurable.measurableSet_preimage_iff_of_surjective, exists_spanning_measurableSet_le, MeasurableEquiv.measurableSet_image, MeasureTheory.preVariation.Finset.sup_measurableSetSubtype_eq_biUnion, MeasureTheory.IsStoppingTime.measurableSet_lt_of_pred, MeasureTheory.Measure.InnerRegularWRT.of_sigmaFinite, MeasurableSet.coe_bot, MeasurableSet.of_mem_nhdsGT_aux, MeasureTheory.IsStoppingTime.measurableSet_eq_le, MeasureTheory.measurable_image_of_fderivWithin, indepSets_comap_of_bcf, MeasurableSpace.measurableSet_succ_countablePartition, MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable', MeasureTheory.AECover.measurableSet, MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable, measurableSet_pi_polarCoord_target, MeasurableSpace.measurableSet_memPartition, measurableSet_range_inl, MeasureTheory.AEFinStronglyMeasurable.measurableSet, measurableSet_swap_iff, MeasureTheory.IsStoppingTime.measurableSet_le, measurableSet_prod_of_nonempty, MeasureTheory.NullMeasurableSet.measurable_of_complete, MeasureTheory.StronglyMeasurable.measurableSet_le, MeasurableSet.ite, MeasurableSpace.measurableSet_countablePartitionSet, MeasureTheory.measurableSet_spanningSets, measurableSet_integrable, MeasureTheory.OuterMeasure.exists_measurable_superset_forall_eq_trim, MeasureTheory.Measure.MeasureDense.indicatorConstLp_subset_closure, MeasurableSet.of_union_cover, MeasurableSet.coe_sdiff, MeasurableSpace.measurableSet_comap, MeasurableSpace.generateFrom_measurableSet, IsClosed.measurableSet, IsOpen.measurableSet, generateFrom_prod, Finset.measurableSet, MeasureTheory.JordanDecomposition.exists_compl_positive_negative, Finset.measurableSet_biInter, MeasureTheory.extend_mono, MeasurableSet.prod, IsGδ.measurableSet, StieltjesFunction.measurableSet_Ioi, MeasureTheory.measurableSet_sigmaFiniteSet, measurableSet_insert, measurableSet_Iic, measurableSet_region_between_co, MeasurableSpace.measurableSet_bot_iff, MeasurableSet.Subtype.instLawfulSingleton, MeasureTheory.measurableCylinders_nat, MeasurableSet.inf_eq_inter, MeasureTheory.SimpleFunc.measurableSet_fiber', measurableSet_region_between_oc, MeasureTheory.IsStoppingTime.measurableSet_eq_stopping_time, MeasureTheory.IsStoppingTime.measurableSet_ge, MeasureTheory.Measure.MeasureDense.measurable, MeasurableSpace.measurableSpace_iSup_eq, MeasurableSet.bihimp, measurableSet_sum_iff, MeasurableSet.measurableAtom_of_countable, MeasureTheory.Measure.WeaklyRegular.innerRegular_measurable, MeasurableSet.image_inclusion, measurable_indicator_const_iff, measurableSet_of_differentiableWithinAt_Ici_of_isComplete, MeasureTheory.Measure.MutuallySingular.measurableSet_nullSet, MeasurableSpace.CountablySeparated.subtype_iff, MeasureTheory.measure_sigmaFiniteSetWRT', MeasureTheory.StronglyMeasurable.exists_spanning_measurableSet_norm_le, measurableSet_uIoc, MeasureTheory.measurableSet_predictable_Ioc_prod, MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable, measurableSet_Ioi, generateFrom_piiUnionInter_measurableSet, MeasureTheory.OuterMeasure.isCaratheodory_iff_le, MeasureTheory.toOuterMeasure_eq_inducedOuterMeasure, MeasurableSet.himp, MeasureTheory.Measure.toSignedMeasure_apply, MeasurableSpace.CountablySeparated.countably_separated, measurableSet_frontier, ProbabilityTheory.Kernel.measurableSet_mutuallySingular, MeasurableSet.setOf_infinite, isFoelner_iff, MeasureTheory.IsStoppingTime.measurableSet_eq, MeasureTheory.tendstoUniformlyOn_of_ae_tendsto', MeasureTheory.measurableSet_preimage_stoppedValue_inter, MeasurableSet.compl, MeasureTheory.measurableSet_filtrationOfSet, MeasureTheory.VectorMeasure.measurable_of_not_restrict_le_zero, MeasurableSet.coe_himp, aeSeq.aeSeqSet_measurableSet, MeasureTheory.IsStoppingTime.measurableSet_min_iff, MeasurableSet.measurableSet_bliminf, ProbabilityTheory.Kernel.measurableSet_absolutelyContinuous, NumberField.mixedEmbedding.measurableSet_fundamentalCone, MeasurableSet.const, ProbabilityTheory.Kernel.measurableSet_mutuallySingularSet, ProbabilityTheory.measurableSet_partitionFiltration_memPartitionSet, MeasureTheory.IsStoppingTime.measurableSet_le', MeasureTheory.Measure.InnerRegularWRT.restrict_of_measure_ne_top, MeasurableSpace.measurableSet_generateFrom_memPartition_iff, MeasurableSet.inl_image, ProbabilityTheory.measurableSet_countableFiltration_countablePartitionSet, measurableSet_of_differentiableAt, MeasureTheory.IsStoppingTime.measurableSet_lt_le, MeasureTheory.SimpleFunc.measurableSet_support, MeasurableSpace.cardinal_measurableSet_le_continuum, MeasureTheory.Measure.InnerRegularCompactLTTop.innerRegular, measurableSet_interior, MeasurableSpace.measurableSet_generateFrom_memPartition, ProbabilityTheory.measurableSet_integrable, MeasureTheory.tendsto_measure_sigmaFiniteSetGE, MeasurableSet.symmDiff, measurableSet_uIcc, measurableSet_regionBetween, MeasurableEq.measurableSet_diagonal, MeasurableSet.of_mem_nhdsGT, VitaliFamily.FineSubfamilyOn.measurableSet_u, MeasurableSpace.measurableSet_generateFrom_countablePartition_iff, MeasureTheory.measurableSet_sigmaFiniteSetWRT', MeasurableSpace.measurableSet_copy, MeasurableSet.subtype_image, ProbabilityTheory.iIndep.iIndepSets', MeasureTheory.toMeasurable_def, MeasurableSet.coe_compl, MeasurableSet.neg, MeasurableSet.measurableSet_liminf, Set.Subsingleton.measurableSet, MeasurableSet.image_of_antitoneOn, MeasurableSet.const_smul₀, MeasurableSet.cylinder, MeasurableSet.image_inclusion', MeasureTheory.preVariation.sum_le, measurableSet_eq_fun_of_countable, MeasureTheory.measurableSet_toMeasurable, MeasurableSet.sep_finite, MeasureTheory.IsStoppingTime.measurableSet_inter_le, MeasureTheory.preVariation.sum_le_preVariationFun_iUnion', MeasureTheory.inducedOuterMeasure_eq_extend, mem_piiUnionInter_of_measurableSet, MeasurableEmbedding.measurableSet_range, indepSets_comap_pi_of_bcf, MeasureTheory.Content.outerMeasure_caratheodory, MeasurableSet.image_of_continuousOn_injOn, MeasurableSpace.exists_measurableSet_of_ne, indepSets_comap_pi_of_prod_bcf, MeasurableSet.imp, VitaliFamily.eventually_filterAt_measurableSet, MeasureTheory.measurableSet_of_filtration, measurableSet_range_inr, measurableSet_lineDifferentiableAt_uncurry, MeasurableSet.const_smul_of_ne_zero, MeasureTheory.tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist', MeasureTheory.measure_eq_iInf', MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable_range, MeasureTheory.Filtration.IsRightContinuous.measurableSet, Measurable.measurableSet_preimage_iff_preimage_val, MeasureTheory.StronglyMeasurable.measurableSet_eq_fun, MeasurableSpace.measurableSet_natGeneratingSequence, MeasurableSpace.cardinal_measurableSet_le, Filter.Eventually.exists_measurable_mem, MeasurableSet.biInter, measurableSet_Ioo, MeasureTheory.SimpleFunc.measurableSet_preimage, MeasurableSet.coe_empty, measurableSet_Icc, MeasurableSet.measurableSet_limsup, MeasureTheory.Egorov.notConvergentSeq_measurableSet, measurableSet_mem, measurableSet_le', MeasureTheory.StronglyMeasurable.measurableSet_mulSupport, measurableSet_of_differentiableWithinAt_Ioi, MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable_range', measurableSet_ball, ProbabilityTheory.measurableSet_kernel_integrable, MeasureTheory.exists_subordinate_pairwise_disjoint, MeasureTheory.exists_measurable_superset_iff_measure_eq_zero, MeasurableSpace.measurableSet_sInf, Set.Finite.measurableSet_sInter, MeasureTheory.measure_eq_iInf, indepSets_comap_process_of_bcf, measurableSet_of_continuousAt, MeasureTheory.SignedMeasure.exists_subset_restrict_nonpos, MeasurableSet.iInter_of_antitone, MeasureTheory.Measure.exists_positive_of_not_mutuallySingular, measurableSet_eq, MeasureTheory.innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group, MeasureTheory.innerRegular_isCompact_isClosed_measurableSet_of_finite, MeasureTheory.inducedOuterMeasure_eq, MeasureTheory.dirac_ne_dirac_iff_exists_measurableSet, MeasureTheory.AnalyticSet.measurableSet_of_compl, MeasureTheory.preVariation.exists_Finpartition_sum_ge, MeasureTheory.preVariation.exists_Finpartition_sum_gt, MeasurableSet.union, MeasureTheory.AEDisjoint.exists_disjoint_diff, MeasureTheory.IsStoppingTime.measurableSet_stopping_time_le_min, MeasureTheory.measurableSet_filtrationOfSet', measurableSet_lt, ProbabilityTheory.Kernel.measurableSet_mutuallySingularSetSlice, MeasureTheory.SimpleFunc.measurableSet_fiber, MeasurableSet.inv, measurableSet_eball, MeasureTheory.tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist, MeasureTheory.IsPredictable.measurableSet_prodMk_add_one_of_predictable, measurableSet_lineDifferentiableAt, measurableSet_inl_image, MeasurableSet.disjointed, MeasurableSet.measurableSet_blimsup, MeasurableSet.coe_top, ProbabilityTheory.Indep_iff_IndepSets, MeasureTheory.IsStoppingTime.measurableSet_gt', MeasurableSet.of_union_range_cover, MeasureTheory.UnifTight.exists_measurableSet_indicator, generateFrom_pi, MeasureTheory.generateFrom_squareCylinders, MeasurableEquiv.measurableSet_preimage, MeasureTheory.measurableSet_predictable_singleton_prod, Filter.IsMeasurablyGenerated.exists_measurable_subset, MeasurableSet.inr_image, MeasureTheory.Measure.isComplete_iff, MeasureTheory.Measure.exists_eq_disjoint_finiteSpanningSetsIn, MeasureTheory.comap_eval_le_generateFrom_squareCylinders_singleton, IsClosed.measurableSet_image_of_continuousOn_injOn, MeasureTheory.exists_measurable_superset_forall_eq, opensMeasurableSpace_iff_forall_measurableSet, ProbabilityTheory.measurableSet_countableFiltration_of_mem, MeasurableSet.iff, MeasureTheory.exists_setLIntegral_compl_lt, measurableSet_of_differentiableAt_of_isComplete_with_param, measurableSet_preimage_up, MeasurableSpace.measurableSet_injective, MeasureTheory.Measure.InnerRegularWRT.of_restrict, MeasurableSet.coe_insert, MeasureTheory.IsStoppingTime.measurableSet_eq_top, MeasureTheory.OuterMeasure.exists_measurable_superset_of_trim_eq_zero, MeasurableSet.sup_eq_union, MeasureTheory.measure_eq_inducedOuterMeasure, MeasurableSet.biUnion, MeasurableSet.iInter_of_antitone_of_frequently, Measurable.measurableSet_preimage_iff_inter_range, generateFrom_measurableSet_of_generatePiSystem, BoxIntegral.Box.measurableSet_Ioo, MeasureTheory.SimpleFunc.measurableSet_cut, MeasureTheory.Measure.IsComplete.out', MeasurableEmbedding.iff_comap_eq, MeasurableSet.const_smul, MeasurableSet.mem_coe, MeasurableSpace.measurableSet_top, MeasurableSpace.hasCountableSeparatingOn_of_countablySeparated, MeasurableSet.iUnion, MeasureTheory.measurableSet_sigmaFiniteSetWRT, ProbabilityTheory.condIndep_iff_condIndepSets, indepSets_comap_process_of_prod_bcf, MeasureTheory.measureDense_measurableSet, MeasureTheory.Egorov.iUnionNotConvergentSeq_measurableSet, NumberField.mixedEmbedding.measurableSet_negAt_plusPart, MeasurableSet.iUnion_of_monotone, measurableSet_region_between_cc, isPiSystem_pi, measurableSet_Ioc, measurableSet_closedBall, MeasureTheory.Measure.QuasiMeasurePreserving.exists_preimage_eq_of_preimage_ae, MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable_range, MeasureTheory.OuterMeasure.ofFunction_caratheodory, MeasureTheory.IsStoppingTime.measurableSet_min_const_iff, MeasureTheory.measure_eq_extend, ProbabilityTheory.measurableSet_isRatStieltjesPoint, MeasurableSet.image_of_monotoneOn, measurableSet_lt', measurableSet_preimage, RealRMK.range_cut_partition, ProbabilityTheory.iCondIndep_iff_iCondIndepSets, MeasurableSet.insert, MeasureTheory.exists_measurable_superset, MeasureTheory.isClopenable_iff_measurableSet, measurableSet_notMem, MeasureTheory.ProbabilityMeasure.measurableSet_isProbabilityMeasure, MeasurableSpace.hasCountableSeparatingOn_of_countablySeparated_subtype, MeasureTheory.FiniteMeasure.measurableSet_isFiniteMeasure, measurableSet_Ici, MeasureTheory.StronglyMeasurable.measurableSet_support, measurableSet_tendsto, MeasurableSpace.pi_eq_generateFrom_projections, MeasurableSpace.measurableSet_memPartitionSet, MeasureTheory.OuterMeasure.exists_measurable_superset_eq_trim, measurableSet_botSet, MeasureTheory.OuterMeasure.trim_eq_iInf, MeasureTheory.exists_measurable_superset_of_null, MeasureTheory.NullMeasurableSet.exists_measurable_superset_ae_eq, measurableSet_bddBelow_range, MeasureTheory.measurableCylinders.measurableSet, MeasureTheory.preVariation.sum_le_preVariationFun_of_subset, measurableSet_quotient, MeasurableSpace.measurableSet_succ_memPartition, MeasureTheory.innerRegularWRT_isCompact_isClosed_measure_ne_top_of_addGroup, Set.Finite.measurableSet, MeasureTheory.mem_measurableCylinders, NumberField.mixedEmbedding.fundamentalCone.measurableSet_paramSet, MeasureTheory.Measure.IsComplete.out, MeasurableSpace.generateFrom_le_iff, MeasurableSet.iInter, MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed_set_eq, MeasureTheory.Measure.innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_addGroup, MeasureTheory.PolishSpace.innerRegular_isCompact_isClosed_measurableSet, MeasurableSet.coe_inter, MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq, MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable', NumberField.mixedEmbedding.fundamentalCone.measurableSet_normLeOne, MeasurableSpace.measurableSet_inf, measurableSet_prod, MeasurableSet.iUnion_of_monotone_of_frequently, MeasurableSpace.measurableSet_sup, Finset.measurableSet_biUnion, measurableSet_of_differentiableWithinAt_Ici, MeasureTheory.Measure.lt_iff, MeasureTheory.IsStoppingTime.measurableSet_stopping_time_le, MeasurableSet.of_subtype_image, MeasureTheory.VectorMeasure.trim_apply, measurableSet_bddAbove_range, isAddFoelner_iff, measurableSet_of_tendsto_indicator, MeasurableSpace.DynkinSystem.generate_has_subset_generate_measurable, measurableSet_generateFrom_of_mem_supClosure, MeasureTheory.measurableSet_of_null, MeasurableSet.univ_pi, measurableSet_pi, MeasureTheory.IsStoppingTime.measurableSet_lt', MeasureTheory.Measure.InnerRegular.innerRegular, VitaliFamily.exists_measurable_supersets_limRatio, measurableSet_iSup_of_mem_piiUnionInter, MeasureTheory.IsHahnDecomposition.measurableSet, MeasurableSet.univ, VitaliFamily.measurableSet, MeasureTheory.SignedMeasure.toJordanDecomposition_spec, MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable_range', MeasureTheory.AEFinStronglyMeasurable.exists_set_sigmaFinite, IsCompact.measurableSet, MeasureTheory.measure_sigmaFiniteSetGE_ge, MeasurableSet.univ_pi', MeasureTheory.IsStoppingTime.measurableSet_eq', IndepFun.singleton_indepSets_of_indicator, MeasureTheory.IsStoppingTime.measurableSet_inter_eq_iff, MeasureTheory.Measure.InnerRegularWRT.measurableSet_of_isOpen, MeasurableSpace.measurableSet_countablePartition, MeasurableSpace.ext_iff, IsPreconnected.measurableSet, MeasureTheory.MemLp.exists_eLpNorm_indicator_compl_lt, MeasureTheory.VectorMeasure.exists_pos_measure_of_not_restrict_le_zero, MeasurableSpace.measurableSet_iSup, measurableSet_of_differentiableAt_with_param, MeasurableSet.const_vadd, MeasurableSet.pi, MeasureTheory.tendstoUniformlyOn_of_ae_tendsto, MeasurableSet.inter
MeasurableSingletonClass 📖	CompData	21 math math: eventuallyMeasurableSingleton, Subsingleton.measurableSingletonClass, ZMod.instMeasurableSingletonClass, DiscreteMeasurableSpace.toMeasurableSingletonClass, Bool.instMeasurableSingletonClass, measurableSingleton_of_standardBorel, Fin.instMeasurableSingletonClass, Prod.instMeasurableSingletonClass, Rat.instMeasurableSingletonClass, Int.instMeasurableSingletonClass, instMeasurableSingletonClassOfMeasurableEq, MeasurableSpace.MeasurableSingletonClass.of_separatesPoints, Set.instMeasurableSingletonClass, OpensMeasurableSpace.toMeasurableSingletonClass, Pi.instMeasurableSingletonClass, ENat.instMeasurableSingletonClass, Nat.instMeasurableSingletonClass, Subtype.instMeasurableSingletonClass, Prop.instMeasurableSingletonClass, MeasureTheory.NullMeasurableSet.instMeasurableSingletonClass, MeasurableSpace.measurableSingletonClass_of_countablySeparated
instMeasurableSpaceOrderDual 📖	CompOp	6 math math: OrderDual.instMeasurableSup₂, OrderDual.instMeasurableSup, OrderDual.borelSpace, OrderDual.instMeasurableInf₂, OrderDual.instMeasurableInf, OrderDual.opensMeasurableSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDiscreteMeasurableSpace 📖	mathematical	—	DiscreteMeasurableSpace Top.top MeasurableSpace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice MeasurableSpace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	MeasurableSpace.measurableSet_top
measurableSet_eq 📖	mathematical	—	MeasurableSet setOf	—	MeasurableSet.singleton
measurableSet_insert 📖	mathematical	—	MeasurableSet Set Set.instInsert	—	Set.insert_eq_of_mem MeasurableSet.diff MeasurableSet.singleton Set.insert_diff_self_of_notMem MeasurableSet.insert
measurable_const 📖	mathematical	—	Measurable	—	MeasurableSet.const
measurable_id 📖	mathematical	—	Measurable	—	—
measurable_id' 📖	mathematical	—	Measurable	—	measurable_id
nonempty_measurable_superset 📖	mathematical	—	Set Set.instHasSubset MeasurableSet	—	Set.subset_univ MeasurableSet.univ

---

← Back to Index