Constructions

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

Statistics

Metric	Count
Definitions MeasurableEq, pi, prod, instMeasurableSpace, instMeasurableSpace, instMeasurableSpace, measurableSpace, measurableSpace, instMeasurableSpace, instMeasurableSpace, instMeasurableSpace, instMeasurableSpace, instMeasurableSpace, instMeasurableSpace, measurableAtom	15
Theorems measurable_iff, measurable_restrict, measurable_restrict_apply, measurable_restrict₂, measurable_restrict₂_apply, and, codRestrict, const_eq, dite, eq, eq_const, eq_mp, eval, exists, find, forall, fst, iff, imp, not, of_uncurry_left, of_uncurry_right, or, prod, prodMap, prodMk, rangeFactorization, setOf, snd, subset, subtype_coe, subtype_map, subtype_mk, subtype_val, sumElim, sumMap, measurableSet_diagonal, disjointed, image_inclusion, image_inclusion', inl_image, inr_image, measurableAtom_of_countable, mem, of_subtype_image, of_union_cover, pi, prod, sep_finite, sep_infinite, setOf_finite, setOf_infinite, subtype_image, tProd, univ_pi, univ_pi', comap_le_comap_pi, instMeasurableSingletonClass, instMeasurableSingletonClass, instDiscreteMeasurableSpace, instDiscreteMeasurableSpace, measurable_coe, measurable_from_quotient, instDiscreteMeasurableSpace, measurable_coe, measurable_from_quotient, instMeasurableSingletonClass, measurable_restrict, measurable_restrict_apply, measurable_restrict₂, measurable_restrict₂_apply, instMeasurableSingletonClass, disjoint_measurableAtom_of_notMem, exists_measurable_piecewise, instMeasurableEqOfMeasurableSingletonClassOfCountable, instMeasurableSingletonClassOfMeasurableEq, measurableAtom_eq_of_mem, measurableAtom_of_measurableSingletonClass, measurableAtom_subset, measurableAtom_subset_of_mem, measurableSet_eq_fun, measurableSet_inl_image, measurableSet_inr_image, measurableSet_mem, measurableSet_notMem, measurableSet_pi, measurableSet_pi_of_nonempty, measurableSet_preimage_down, measurableSet_preimage_up, measurableSet_prod, measurableSet_prod_of_nonempty, measurableSet_quotient, measurableSet_range_inl, measurableSet_range_inr, measurableSet_setOf, measurableSet_sum_iff, measurableSet_swap_iff, measurable_compl, measurable_curry, measurable_down, measurable_eq_mp, measurable_equivCurry, measurable_equivCurry_symm, measurable_find, measurable_findGreatest, measurable_findGreatest', measurable_from_nat, measurable_from_prod_countable_left, measurable_from_prod_countable_left', measurable_from_prod_countable_right, measurable_from_prod_countable_right', measurable_from_quotient, measurable_fst, measurable_fun_prod, measurable_fun_sum, measurable_iUnionLift, measurable_inclusion, measurable_inl, measurable_inr, measurable_liftCover, measurable_mem, measurable_of_measurable_on_compl_finite, measurable_of_measurable_on_compl_singleton, measurable_of_measurable_union_cover, measurable_of_restrict_of_restrict_compl, measurable_piCongrLeft, measurable_piCurry, measurable_piCurry_symm, measurable_piEquivPiSubtypeProd, measurable_piEquivPiSubtypeProd_symm, measurable_pi_apply, measurable_pi_iff, measurable_pi_lambda, measurable_prodMk_left, measurable_prodMk_right, measurable_quot_mk, measurable_quotient_mk', measurable_quotient_mk'', measurable_setOf, measurable_set_iff, measurable_set_mem, measurable_set_notMem, measurable_sigmaCurry, measurable_sigmaUncurry, measurable_snd, measurable_subtype_coe, measurable_swap, measurable_swap_iff, measurable_tProd_elim, measurable_tProd_elim', measurable_tProd_mk, measurable_to_bool, measurable_to_countable, measurable_to_countable', measurable_to_nat, measurable_to_prop, measurable_uncurry, measurable_uniqueElim, measurable_unit, measurable_up, measurable_update, measurable_update', measurable_updateFinset, measurable_updateFinset', measurable_updateFinset_left, measurable_update_left, mem_measurableAtom_self, mem_of_mem_measurableAtom	168
Total	183

ENat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_iff 📖	mathematical	—	Measurable ENat instMeasurableSpace MeasurableSet Set.preimage Set Set.instSingletonSet instNatCast	—	MeasurableSingletonClass.measurableSet_singleton instMeasurableSingletonClass measurable_to_countable' instCountable WithTop.none_eq_top Set.compl_range_some Set.preimage_compl Set.iUnion_singleton_eq_range Set.preimage_iUnion MeasurableSet.compl MeasurableSet.iUnion instCountableNat

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_restrict 📖	mathematical	—	Measurable MeasurableSpace.pi Finset SetLike.instMembership instSetLike restrict	—	measurable_pi_lambda measurable_pi_apply
measurable_restrict_apply 📖	mathematical	Measurable	Measurable Finset SetLike.instMembership instSetLike Subtype.instMeasurableSpace restrict	—	Measurable.comp measurable_subtype_coe
measurable_restrict₂ 📖	mathematical	Finset instHasSubset	Measurable MeasurableSpace.pi Finset SetLike.instMembership instSetLike restrict₂	—	measurable_pi_lambda measurable_pi_apply
measurable_restrict₂_apply 📖	mathematical	Finset instHasSubset Measurable SetLike.instMembership instSetLike Subtype.instMeasurableSpace	Measurable Finset SetLike.instMembership instSetLike Subtype.instMeasurableSpace restrict₂	—	Measurable.comp measurable_inclusion

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
and 📖	mathematical	Measurable Prop.instMeasurableSpace	Measurable Prop.instMeasurableSpace	—	measurableSet_setOf MeasurableSet.inter setOf
codRestrict 📖	mathematical	Measurable Set Set.instMembership	Measurable Set.Elem Subtype.instMeasurableSpace Set Set.instMembership Set.codRestrict	—	—
const_eq 📖	mathematical	Measurable	Measurable Prop.instMeasurableSpace	—	eq_const
dite 📖	mathematical	Measurable Set.Elem Subtype.instMeasurableSpace Set Set.instMembership Compl.compl Set.instCompl MeasurableSet	Measurable Set Set.instMembership Compl.compl Set.instCompl	—	measurable_of_restrict_of_restrict_compl Set.restrict_dite Subtype.coe_eta Set.restrict_dite_compl
eq 📖	mathematical	Measurable	Measurable Prop.instMeasurableSpace	—	measurableSet_setOf measurableSet_eq_fun
eq_const 📖	mathematical	Measurable	Measurable Prop.instMeasurableSpace	—	measurableSet_setOf MeasurableSet.preimage measurableSet_eq
eq_mp 📖	mathematical	Measurable	Measurable	—	comp measurable_eq_mp
eval 📖	mathematical	Measurable MeasurableSpace.pi	Measurable	—	comp measurable_pi_apply
exists 📖	mathematical	Measurable Prop.instMeasurableSpace	Measurable Prop.instMeasurableSpace	—	measurableSet_setOf Set.setOf_exists MeasurableSet.iUnion setOf
find 📖	mathematical	Measurable MeasurableSet setOf	Measurable Nat.find	—	measurable_from_prod_countable_left instCountableNat Nat.instMeasurableSingletonClass comp prodMk measurable_id measurable_find
forall 📖	mathematical	Measurable Prop.instMeasurableSpace	Measurable Prop.instMeasurableSpace	—	measurableSet_setOf Set.setOf_forall MeasurableSet.iInter setOf
fst 📖	mathematical	Measurable Prod.instMeasurableSpace	Measurable	—	comp measurable_fst
iff 📖	mathematical	Measurable Prop.instMeasurableSpace	Measurable Prop.instMeasurableSpace	—	measurableSet_setOf MeasurableSet.bihimp setOf
imp 📖	mathematical	Measurable Prop.instMeasurableSpace	Measurable Prop.instMeasurableSpace	—	measurableSet_setOf MeasurableSet.himp setOf
not 📖	mathematical	Measurable Prop.instMeasurableSpace	Measurable Prop.instMeasurableSpace	—	measurableSet_setOf MeasurableSet.compl setOf
of_uncurry_left 📖	mathematical	Measurable Prod.instMeasurableSpace	Measurable	—	comp measurable_prodMk_left
of_uncurry_right 📖	mathematical	Measurable Prod.instMeasurableSpace	Measurable	—	comp measurable_prodMk_right
or 📖	mathematical	Measurable Prop.instMeasurableSpace	Measurable Prop.instMeasurableSpace	—	measurableSet_setOf MeasurableSet.union setOf
prod 📖	mathematical	Measurable	Measurable Prod.instMeasurableSpace	—	of_le_map sup_le MeasurableSpace.comap_le_iff_le_map MeasurableSpace.map_comp
prodMap 📖	mathematical	Measurable	Measurable Prod.instMeasurableSpace	—	prodMk comp measurable_fst measurable_snd
prodMk 📖	mathematical	Measurable	Measurable Prod.instMeasurableSpace	—	prod
rangeFactorization 📖	mathematical	Measurable	Measurable Set.Elem Set.range Subtype.instMeasurableSpace Set Set.instMembership Set.rangeFactorization	—	Set.mem_range_self
setOf 📖	mathematical	Measurable Prop.instMeasurableSpace	MeasurableSet setOf	—	measurableSet_setOf
snd 📖	mathematical	Measurable Prod.instMeasurableSpace	Measurable	—	comp measurable_snd
subset 📖	mathematical	Measurable Set Set.instMeasurableSpace	Measurable Prop.instMeasurableSpace Set Set.instHasSubset	—	forall imp fun_comp measurable_set_mem
subtype_coe 📖	mathematical	Measurable Subtype.instMeasurableSpace	Measurable	—	comp measurable_subtype_coe
subtype_map 📖	mathematical	Measurable	Measurable Subtype.instMeasurableSpace Subtype.map	—	comp measurable_subtype_coe
subtype_mk 📖	mathematical	Measurable	Measurable Subtype.instMeasurableSpace	—	—
subtype_val 📖	mathematical	Measurable Subtype.instMeasurableSpace	Measurable	—	subtype_coe
sumElim 📖	mathematical	Measurable	Measurable Sum.instMeasurableSpace	—	measurable_fun_sum
sumMap 📖	mathematical	Measurable	Measurable Sum.instMeasurableSpace	—	sumElim comp measurable_inl measurable_inr

MeasurableEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableSet_diagonal 📖	mathematical	—	MeasurableSet Prod.instMeasurableSpace Set.diagonal	—	—

MeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjointed 📖	mathematical	MeasurableSet	MeasurableSet disjointed Set BooleanAlgebra.toGeneralizedBooleanAlgebra Set.instBooleanAlgebra Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	—	disjointedRec diff
image_inclusion 📖	mathematical	Set Set.instHasSubset MeasurableSet Set.Elem Subtype.instMeasurableSpace Set.instMembership	MeasurableSet Set.Elem Subtype.instMeasurableSpace Set Set.instMembership Set.image Set.inclusion	—	image_inclusion' measurable_subtype_coe
image_inclusion' 📖	mathematical	Set Set.instHasSubset MeasurableSet Set.Elem Subtype.instMeasurableSpace Set.instMembership Set.preimage	MeasurableSet Set.Elem Subtype.instMeasurableSpace Set Set.instMembership Set.image Set.inclusion	—	Set.ext inter measurable_subtype_coe
inl_image 📖	mathematical	MeasurableSet	MeasurableSet Sum.instMeasurableSpace Set.image	—	measurableSet_inl_image
inr_image 📖	mathematical	MeasurableSet	MeasurableSet Sum.instMeasurableSpace Set.image	—	measurableSet_inr_image
measurableAtom_of_countable 📖	mathematical	—	MeasurableSet measurableAtom	—	Set.Subset.antisymm Set.iInter_congr_Prop mem_of_mem_measurableAtom Set.compl_subset_compl Set.compl_iInter biInter Set.to_countable SetCoe.countable Function.sometimes_spec
mem 📖	mathematical	MeasurableSet	Measurable Prop.instMeasurableSpace Set Set.instMembership	—	measurable_mem
of_subtype_image 📖	mathematical	MeasurableSet Set.image Set Set.instMembership	MeasurableSet Set.Elem Subtype.instMeasurableSpace Set Set.instMembership	—	Set.preimage_image_eq Subtype.val_injective
of_union_cover 📖	mathematical	MeasurableSet Set Set.instHasSubset Set.univ Set.instUnion Set.instMembership Subtype.instMeasurableSpace Set.preimage	MeasurableSet	—	Set.image_preimage_eq_inter_range Subtype.range_coe_subtype Set.univ_subset_iff Set.inter_univ union subtype_image
pi 📖	mathematical	MeasurableSet	MeasurableSet MeasurableSpace.pi Set.pi	—	Set.pi_def biInter measurable_pi_apply
prod 📖	mathematical	MeasurableSet	MeasurableSet Prod.instMeasurableSpace SProd.sprod Set Set.instSProd	—	inter measurable_fst measurable_snd
sep_finite 📖	mathematical	MeasurableSet Set Set.instMeasurableSpace	MeasurableSet Set Set.instMeasurableSpace setOf Set.instMembership Set.Finite	—	inter setOf_finite
sep_infinite 📖	mathematical	MeasurableSet Set Set.instMeasurableSpace	MeasurableSet Set Set.instMeasurableSpace setOf Set.instMembership Set.Infinite	—	inter setOf_infinite
setOf_finite 📖	mathematical	—	MeasurableSet Set Set.instMeasurableSpace setOf Set.Finite	—	Set.Countable.measurableSet Set.instMeasurableSingletonClass Set.Countable.setOf_finite
setOf_infinite 📖	mathematical	—	MeasurableSet Set Set.instMeasurableSpace setOf Set.Infinite	—	compl setOf_finite
subtype_image 📖	mathematical	MeasurableSet Set.Elem Subtype.instMeasurableSpace Set Set.instMembership	MeasurableSet Set.image Set Set.instMembership	—	Subtype.image_preimage_coe inter
tProd 📖	mathematical	MeasurableSet	MeasurableSet List.TProd TProd.instMeasurableSpace Set.tprod	—	univ prod
univ_pi 📖	mathematical	MeasurableSet	MeasurableSet MeasurableSpace.pi Set.pi Set.univ	—	pi Set.to_countable SetCoe.countable
univ_pi' 📖	mathematical	MeasurableSet	MeasurableSet MeasurableSpace.pi setOf	—	congr univ_pi

MeasurableSpace

Definitions

Name	Category	Theorems
pi 📖	CompOp	535 math, 4 bridge math: indepFun_process_of_bcf, MeasureTheory.volume_preserving_arrowCongr', MeasureTheory.Measure.pi_pi_finset, MeasureTheory.Measure.univ_pi_Ioc_ae_eq_Icc, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, ProbabilityTheory.Kernel.IndepFun.process_congr_left, MeasurableEquiv.piCurry_apply, measurable_sigmaUncurry, ProbabilityTheory.IndepFun.process_congr_left, ProbabilityTheory.IndepFun.indepFun_process₀, Preorder.measurable_restrictLe, ProbabilityTheory.Kernel.isProbabilityMeasure_trajFun, BoxIntegral.Prepartition.measure_iUnion_toReal, MeasureTheory.volume_preserving_pi, MeasureTheory.Integrable.fin_nat_prod, Measure.eq_prod_of_integral_prod_mul_prod_boundedContinuousFunction, NumberField.mixedEmbedding.measurable_polarCoordReal_symm, MeasureTheory.lmarginal_univ, aemeasurable_pi_lambda, measurableSet_pi_of_nonempty, MeasureTheory.measurePreserving_funUnique, ProbabilityTheory.Kernel.partialTraj_succ_of_le, ProbabilityTheory.Kernel.condExp_traj', ZLattice.covolume_eq_det_inv, MeasureTheory.Measure.pi_Ioc_ae_eq_pi_Icc, ProbabilityTheory.isGaussian_multivariateGaussian, ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀, MeasureTheory.measurable_restrict_cylinderEvents, pi_indepFun_pi_of_prod_bcf, ProbabilityTheory.Kernel.map_frestrictLe_trajMeasure_compProd_eq_map_trajMeasure, ProbabilityTheory.covarianceBilin_multivariateGaussian, BoxIntegral.Box.measurableSet_Icc, indicator_indepFun_pi_of_prod_bcf, MeasureTheory.Measure.pi'_pi, ProbabilityTheory.Kernel.trajContent_cylinder, GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace, Pi.instMeasurableConstSMul, measurable_update', ProbabilityTheory.measurePreserving_restrict₂_multivariateGaussian, MeasureTheory.integral_fintype_prod_eq_prod, MeasureTheory.volume_measurePreserving_piCongrLeft, MeasureTheory.Measure.ae_le_set_pi, NumberField.mixedEmbedding.measurableSet_plusPart, ProbabilityTheory.IsGaussianProcess.iIndepFun_of_covariance_eq_zero, ProbabilityTheory.variance_sum_pi, ProbabilityTheory.Kernel.partialTraj_comp_partialTraj', ProbabilityTheory.iIndepFun_infinitePi, measurable_pi_iff, MeasureTheory.Measure.pi_map_piCongrLeft, MeasureTheory.Measure.pi.isInvInvariant, ProbabilityTheory.HasGaussianLaw.toLp_pi, MeasurableEquiv.finTwoArrow_apply, MeasureTheory.lintegral_prod_lintegral_pow_le, MeasureTheory.lintegral_le_of_lmarginal_le, MeasureTheory.Measure.pi_of_empty, MeasureTheory.Measure.pi_eval_preimage_null, MeasureTheory.Measure.pi.sigmaFinite, MeasureTheory.measurable_uniqueElim_cylinderEvents, MeasureTheory.isProjectiveLimit_nat_iff, MeasureTheory.integral_infinitePi_of_piFinset, MeasureTheory.measurePreserving_pi, measurable_pi_lambda, Real.smul_map_diagonal_volume_pi, BoxIntegral.Box.measurableSet_coe, ProbabilityTheory.Kernel.traj_map_updateFinset, Finset.measurable_restrict, MeasureTheory.lintegral_restrict_infinitePi, ProbabilityTheory.Kernel.map_partialTraj_succ_self, MeasureTheory.ProbabilityMeasure.continuous_pi, UnitAddTorus.coe_symm_measurableEquivPiIoc, MeasurableEquiv.piFinTwo_symm_apply, OrthonormalBasis.measurePreserving_repr, MeasureTheory.instSFiniteForallValNatMemFinsetInducedFamilyOfForallIic, MeasureTheory.volume_preserving_piFinsetUnion, measurable_uncurry, instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast, Finset.measurable_restrict₂, Pi.measurableAdd, ProbabilityTheory.IndepFun.process_congr_right, MeasureTheory.Measure.pi_hyperplane, MeasureTheory.Measure.univ_pi_Ioo_ae_eq_Icc, generateFrom_eq_pi, Complex.measurableEquivPi_apply, ProbabilityTheory.IsGaussianProcess.hasGaussianLaw, MeasureTheory.integral_fintype_prod_eq_pow, Set.OrdConnected.nullMeasurableSet, MeasureTheory.Measure.pi_noAtoms, MeasureTheory.measurePreserving_finTwoArrow_vec, ProbabilityTheory.IsRatCondKernelCDFAux.measurable, MeasureTheory.piContent_cylinder, MeasureTheory.integrable_comp_eval, ProbabilityTheory.charFun_multivariateGaussian, aemeasurable_pi_iff, MeasureTheory.charFunDual_pi', MeasureTheory.measurable_cylinderEvents_lambda, ProbabilityTheory.Kernel.partialTraj_comp_partialTraj'', ProbabilityTheory.covarianceBilin_apply_basisFun_self, measurable_tProd_elim', GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace, MeasurableEquiv.funUnique_symm_apply, MeasurableEquiv.coe_sumPiEquivProdPi, MeasureTheory.Measure.pi_pi_aux, EuclideanSpace.volume_closedBall_fin_three, MeasureTheory.lintegral_eq_lmarginal_univ, MeasurableEquiv.piEquivPiSubtypeProd_apply, MeasureTheory.Measure.infinitePi_map_piCongrLeft, MeasureTheory.hausdorffMeasure_measurePreserving_piFinTwo, MeasureTheory.Measure.infinitePi_map_piCurry, MeasurableSet.of_mem_measurableCylinders, ProbabilityTheory.stieltjesOfMeasurableRat_unit_prod, MeasureTheory.lintegral_infinitePi_of_piFinset, Real.map_matrix_volume_pi_eq_smul_volume_pi, MeasureTheory.IsProjectiveMeasureFamily.measure_univ_eq_of_subset, ProbabilityTheory.IndepFun.process_congr, ZLattice.covolume.tendsto_card_div_pow, MeasureTheory.Measure.infinitePi_pi, MeasurableEquiv.coe_IicProdIoc_symm, SimpleGraph.binomialRandom_apply, generateFrom_pi_eq, MeasureTheory.IsProjectiveMeasureFamily.congr_cylinder_of_subset, PiLp.volume_preserving_toLp, Pi.measurableSub₂, ProbabilityTheory.Kernel.integral_traj_partialTraj', ProbabilityTheory.iIndepFun_pi, BoxIntegral.Box.measure_coe_lt_top, MeasureTheory.Measure.map_piSingleton, ProbabilityTheory.IndepFun.indepFun_process, ProbabilityTheory.setBernoulli_apply', NumberField.mixedEmbedding.fundamentalDomain_idealLattice, BoxIntegral.Box.measure_Icc_lt_top, ZLattice.covolume_div_covolume_eq_relIndex, MeasureTheory.FiniteMeasure.pi_pi, MeasureTheory.AEContinuous.hasBoxIntegral, MeasureTheory.ProbabilityMeasure.pi_pi, MeasureTheory.integral_comp_eval, Measure.eq_prod_of_integral_mul_prod_boundedContinuousFunction, ProbabilityTheory.Kernel.aestronglyMeasurable_traj, MeasureTheory.Measure.pi_prod_map_IocProdIoc, MeasureTheory.lintegral_mul_prod_lintegral_pow_le, ProbabilityTheory.multivariateGaussian_of_not_posSemidef, MeasureTheory.hausdorffMeasure_pi_real, MeasureTheory.volume_preserving_piFinSuccAbove, ProbabilityTheory.Kernel.instIsProbabilityMeasureForallTrajMeasure, EuclideanSpace.volume_closedBall_fin_two, MeasureTheory.Measure.pi.isLocallyFiniteMeasure, ProbabilityTheory.IsGaussianProcess.indepFun_of_covariance_strongDual, MeasureTheory.measurePreserving_eval, MeasureTheory.Measure.pi_ball, MeasureTheory.measurePreserving_piCongrLeft, MeasureTheory.IsProjectiveLimit.measure_univ_eq, measurable_sigmaCurry, Pi.opensMeasurableSpace, ProbabilityTheory.Kernel.partialTraj_compProd_traj, ProbabilityTheory.map_pi_eq_stdGaussian, ProbabilityTheory.integral_id_multivariateGaussian, measurableSet_pi_polarCoord_target, MeasureTheory.projectiveFamilyContent_cylinder, MeasureTheory.measurePreserving_arrowCongr', MeasureTheory.Measure.pi.isHaarMeasure, MeasureTheory.measurePreserving_arrowProdEquivProdArrow, MeasureTheory.Measure.pi_map_eval, ProbabilityTheory.Kernel.partialTraj_succ_eq_comp, Preorder.measurable_frestrictLe₂, Measure.eq_prod_of_integral_prod_mul_prod_boundedContinuousFunction', UnitAddTorus.measurePreserving_equivPiIoc, measurable_pi_apply, ProbabilityTheory.Kernel.partialTraj_le_def, MeasureTheory.Measure.restrict_pi_pi, MeasureTheory.charFun_pi, MeasureTheory.Measure.pi_Ico_ae_eq_pi_Icc, MeasureTheory.volume_preserving_pi_empty, MeasureTheory.Measure.pi.isAddRightInvariant, MeasureTheory.IsProjectiveMeasureFamily.eq_zero_of_isEmpty, MeasureTheory.Measure.pi_singleton, ProbabilityTheory.Kernel.condDistrib_trajMeasure, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, MeasureTheory.projectiveFamilyContent_congr, MeasureTheory.Integrable.fintype_prod_dep, ProbabilityTheory.iCondIndepFun.condIndepFun_finset, MeasureTheory.piContent_eq_measure_pi, Pi.measurableDiv, NumberField.mixedEmbedding.covolume_idealLattice, indep_comap_pi_of_bcf, NumberField.mixedEmbedding.volume_preserving_negAt, measurable_update_left, ProbabilityTheory.Kernel.traj_comp_partialTraj, MeasureTheory.Measure.infinitePiNat_map_piCongrLeft, MeasureTheory.measurePreserving_piFinTwo, MeasurableEquiv.curry_symm_apply, MeasureTheory.Measure.pi_prod_map_IicProdIoc, MeasureTheory.measurableCylinders_nat, ProbabilityTheory.Kernel.IndepFun.process_congr_right, Preorder.measurable_restrictLe₂, ProbabilityTheory.variance_eval_multivariateGaussian, MeasureTheory.Measure.pi_univ, ProbabilityTheory.Kernel.measurable_trajFun, ProbabilityTheory.Kernel.partialTraj_map_frestrictLe₂_apply, MeasureTheory.Measure.pi_Ioi_ae_eq_pi_Ici, Pi.measurableInv, MeasureTheory.Measure.pi_caratheodory, ProbabilityTheory.Kernel.lintegral_traj, MeasureTheory.ProbabilityMeasure.toMeasure_pi, NumberField.Units.regOfFamily_of_isMaxRank, MeasureTheory.instIsProbabilityMeasureForallValNatMemFinsetInducedFamilyOfForallIic, ProbabilityTheory.Kernel.instIsSFiniteKernelForallValNatMemFinsetIicPartialTraj, PiLp.volume_preserving_ofLp, ProbabilityTheory.Kernel.partialTraj_succ_map_frestrictLe₂, StandardBorelSpace.pi_countable, MeasureTheory.Measure.pi_map_pi, measurable_setOf, MeasureTheory.Measure.univ_pi_Ico_ae_eq_Icc, process_indepFun_process_of_bcf, ProbabilityTheory.Kernel.condExp_traj, MeasureTheory.partialTraj_const, ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_increments, indicator_indepFun_pi_of_bcf, MeasureTheory.Measure.pi_Ioo_ae_eq_pi_Icc, ProbabilityTheory.Kernel.IndepFun.process_indepFun, ProbabilityTheory.Kernel.partialTraj_le, ProbabilityTheory.IsGaussianProcess.iIndepFun_of_covariance_strongDual, ProbabilityTheory.Kernel.IndepFun.process_indepFun₀, MeasurableEquiv.curry_apply, NumberField.mixedEmbedding.volume_preserving_mixedSpaceToRealMixedSpace_symm, MeasureTheory.Measure.univ_pi_Ioi_ae_eq_Ici, BoxIntegral.norm_integral_le_of_le_const, MeasureTheory.Measure.infinitePi_singleton_of_fintype, indicator_indepFun_process_of_bcf, ProbabilityTheory.Kernel.partialTraj_succ_self, MeasureTheory.Measure.volume_pi_eq_dirac, indepFun_pi_of_bcf, measurable_updateFinset, ProbabilityTheory.charFun_map_sum_pi_eq_prod, Set.measurable_restrict₂, ProbabilityTheory.measurable_preCDF', MeasureTheory.instIsFiniteMeasureForallValNatMemFinsetInducedFamilyOfForallIic, ProbabilityTheory.IsGaussianProcess.indepFun_of_covariance_eq_zero, MeasureTheory.Measure.pi.isMulRightInvariant, measurable_IicProdIoc, MeasureTheory.measurePreserving_piFinSuccAbove, MeasureTheory.Measure.infinitePi_map_eval, measurable_tProd_mk, ProbabilityTheory.condCDF_eq_stieltjesOfMeasurableRat_unit_prod, MeasurableEquiv.piUnique_symm_apply, Pi.measurableMul₂, MeasurableEquiv.piUnique_apply, NumberField.mixedEmbedding.fundamentalDomain_stdBasis, MeasurableEquiv.piCongrLeft_apply_apply, PiLp.borelSpace, process_indepFun_process_of_prod_bcf, MeasurableEquiv.coe_IicProdIoc, ProbabilityTheory.Kernel.isProjectiveLimit_trajFun, NumberField.mixedEmbedding.measurableSet_fundamentalCone, ProbabilityTheory.isProjectiveMeasureFamily_map_restrict, measurePreserving_eval_infinitePi, pi_indepFun_pi_of_bcf, indep_comap_process_of_bcf, measurable_updateFinset_left, process_indepFun_of_prod_bcf, ProbabilityTheory.Kernel.IndepFun.process_congr, Pi.borelSpace, Measure.eq_prod_of_integral_prod_mul_boundedContinuousFunction', MeasureTheory.Measure.infinitePi_dirac, ProbabilityTheory.Kernel.traj_map_frestrictLe_of_le, ProbabilityTheory.HasGaussianLaw.indepFun_of_covariance_eval, ProbabilityTheory.iIndepFun_iff_charFunDual_pi, MeasurableEquiv.coe_piCongrLeft, ProbabilityTheory.Kernel.instIsFiniteKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat, MeasurableEquiv.funUnique_apply, ProbabilityTheory.covarianceBilin_apply_pi, MeasureTheory.measurePreserving_piUnique, NumberField.mixedEmbedding.covolume_integerLattice, MeasureTheory.Measure.pi.isMulLeftInvariant, MeasureTheory.Measure.infinitePi_map_curry_symm, MeasureTheory.Measure.pi_Ioo_ae_eq_pi_Ioc, ProbabilityTheory.Kernel.partialTraj_comp_partialTraj, EuclideanSpace.volume_ball_fin_three, ProbabilityTheory.covarianceBilin_apply_basisFun, ProbabilityTheory.measurable_toRatCDF, MeasureTheory.hausdorffMeasure_measurePreserving_funUnique, ProbabilityTheory.Kernel.instIsMarkovKernelForallValNatMemFinsetIicForallTraj, ProbabilityTheory.Kernel.iIndepFun.iIndepFun_process₀, ProbabilityTheory.identDistrib_iff_forall_finset_identDistrib, MeasureTheory.Measure.pi_closedBall, pi_indepFun_of_prod_bcf, OrthonormalBasis.measurePreserving_repr_symm, MeasureTheory.ContinuousOn.hasBoxIntegral, ProbabilityTheory.Kernel.integral_traj_partialTraj, indep_comap_process_of_prod_bcf, MeasurableSet.cylinder, MeasureTheory.addHaarMeasure_eq_volume_pi, MeasurableEquiv.piEquivPiSubtypeProd_symm_apply, MeasureTheory.Filtration.piFinset_eq_comap_restrict, Measurable.lmarginal, measurable_equivCurry_symm, ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat, MeasureTheory.IsProjectiveLimit.measure_cylinder, measurable_updateFinset', ProbabilityTheory.iIndepFun.hasGaussianLaw, ZLattice.volume_image_eq_volume_div_covolume, Real.map_linearMap_volume_pi_eq_smul_volume_pi, MeasureTheory.volume_preserving_piFinTwo, indepSets_comap_pi_of_bcf, process_indepFun_of_bcf, Pi.measurableSMul, Complex.measurableEquivPi_symm_apply, pi_le_borel_pi, Pi.measurableNeg, indepSets_comap_pi_of_prod_bcf, MeasureTheory.Measure.map_linearMap_addHaar_pi_eq_smul_addHaar, MeasureTheory.Measure.instIsProbabilityMeasureForallInfinitePi, MeasureTheory.Measure.quasiMeasurePreserving_eval, UnitAddTorus.coe_measurableEquivPiIoc_apply, MeasurableEquiv.piMeasurableEquivTProd_apply, indepFun_pi_of_prod_bcf, ProbabilityTheory.Kernel.isProjectiveMeasureFamily_partialTraj, EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp, MeasureTheory.integral_fin_nat_prod_eq_prod, MeasureTheory.charFunDual_eq_pi_iff, ZLattice.covolume.tendsto_card_le_div, Set.measurable_restrict, Complex.volume_preserving_equiv_pi, ProbabilityTheory.charFunDual_map_sum_pi_eq_prod, ProbabilityTheory.IndepFun.process_indepFun_process, measurable_uniqueElim, NumberField.mixedEmbedding.volume_preserving_homeoRealMixedSpacePolarSpace, EuclideanSpace.volume_ball_fin_two, pi_indepFun_of_bcf, ProbabilityTheory.Kernel.partialTraj_self, ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀', ProbabilityTheory.Kernel.traj_apply, MeasureTheory.IsProjectiveMeasureFamily.congr_cylinder, ProbabilityTheory.IsGaussianProcess.iIndepFun_of_covariance_inner, ContinuousLinearMap.measurable_coe, ProbabilityTheory.IndepFun.process_indepFun, MeasurableEquiv.piCurry_symm_apply, EuclideanSpace.volume_ball, MeasureTheory.cylinderEvents_le_pi, ProbabilityTheory.IdentDistrib.pi, Pi.instMeasurableConstVAdd, ProbabilityTheory.iIndepFun_uncurry_infinitePi, MeasurableEquiv.coe_curry_symm, MeasurableEquiv.coe_sumPiEquivProdPi_symm, MeasureTheory.IsProjectiveMeasureFamily.measure_univ_eq, ProbabilityTheory.iIndepFun_iff_charFunDual_pi', Pi.measurableSub, MeasureTheory.Measure.ae_le_pi, indepSets_comap_process_of_bcf, MeasureTheory.Measure.univ_pi_Iio_ae_eq_Iic, ProbabilityTheory.measurePreserving_eval_multivariateGaussian, measurableEquiv_nat_bool_of_countablyGenerated, UnitAddTorus.coe_measurableEquivPiIoc, indepFun_process_of_prod_bcf, ProbabilityTheory.Kernel.IndepFun.indepFun_process, MeasureTheory.Measure.infinitePi_map_pi, MeasurableEquiv.finTwoArrow_symm_apply, NumberField.mixedEmbedding.measurable_polarCoord_symm, ProbabilityTheory.iIndepFun_iff_charFun_pi, MeasureTheory.measurePreserving_piFinsetUnion, MeasureTheory.Measure.toBoxAdditive_apply, ProbabilityTheory.Kernel.integrable_traj, MeasureTheory.volume_measurePreserving_arrowProdEquivProdArrow, ProbabilityTheory.map_eq_iff_forall_finset_map_restrict_eq, ProbabilityTheory.Kernel.traj_map_frestrictLe, MeasureTheory.Measure.pi.isNegInvariant, ProbabilityTheory.Kernel.integral_traj, ProbabilityTheory.IsGaussianProcess.indepFun_of_covariance_inner, MeasurableEquiv.coe_setOf, MeasureTheory.charFunDual_eq_pi_iff', ProbabilityTheory.Kernel.traj_map_frestrictLe_apply, generateFrom_pi, ProbabilityTheory.isProjectiveLimit_map, MeasureTheory.generateFrom_squareCylinders, MeasureTheory.Measure.infinitePiNat_map_restrict, MeasureTheory.Measure.infinitePi_cylinder, Pi.measurableAdd₂, MeasureTheory.projectiveFamilyFun_congr, Preorder.measurable_frestrictLe, ProbabilityTheory.uniformOn_pi, ProbabilityTheory.map_eq_of_forall_ae_eq, MeasureTheory.partialTraj_const_restrict₂, IsUnifLocDoublingMeasure.pi, MeasureTheory.Filtration.piLE_eq_comap_frestrictLe, MeasureTheory.volume_preserving_piUnique, MeasureTheory.Measure.pi_def, ProbabilityTheory.iIndepFun_uncurry_infinitePi', indep_comap_pi_of_prod_bcf, volume_euclideanSpace_eq_dirac, MeasureTheory.Measure.ae_eq_pi, ProbabilityTheory.stdGaussian_eq_map_pi_orthonormalBasis, MeasurableEquiv.piFinTwo_apply, ProbabilityTheory.Kernel.map_traj_succ_self, measurable_piEquivPiSubtypeProd_symm, measurable_piCurry_symm, ProbabilityTheory.Kernel.iIndepFun.indepFun_finset, MeasureTheory.Integrable.fintype_prod, ProbabilityTheory.Kernel.measurable_lmarginalPartialTraj, MeasureTheory.IsProjectiveLimit.measure_univ_unique, ProbabilityTheory.Kernel.setIntegral_traj_partialTraj, MeasurableEquiv.setOf_symm_apply, MeasurableEquiv.coe_piCurry, BoxIntegral.Box.measurableSet_Ioo, ContinuousLinearMap.measurable_apply', ProbabilityTheory.integral_id_multivariateGaussian', ProbabilityTheory.map_restrict_eq_of_forall_ae_eq, MeasureTheory.Measure.infinitePi_singleton, ProbabilityTheory.iIndepFun.process_congr, ProbabilityTheory.IsRatCondKernelCDF.measurable, Pi.measurableDiv₂, ProbabilityTheory.IsMeasurableRatCDF.measurable, MeasureTheory.Measure.pi.isAddHaarMeasure, ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map, MeasureTheory.Measure.infinitePi_map_restrict, ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_eval, ProbabilityTheory.Kernel.IndepFun.process_indepFun_process₀, measurable_mapNatBool, ProbabilityTheory.Kernel.partialTraj_map_frestrictLe₂, MeasureTheory.integral_eval, Pi.instMeasurableSingletonClass, indicator_indepFun_process_of_prod_bcf, ProbabilityTheory.Kernel.iIndepFun.process_congr, MeasureTheory.charFunDual_pi, SimpleGraph.measurable_adj, indepSets_comap_process_of_prod_bcf, ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map, EuclideanSpace.coe_measurableEquiv, measurable_IocProdIoc, ProbabilityTheory.multivariateGaussian_zero_one, MeasureTheory.Measure.tendsto_eval_ae_ae, ProbabilityTheory.Kernel.IndepFun.process_indepFun_process, MeasureTheory.measurePreserving_sumPiEquivProdPi_symm, NumberField.mixedEmbedding.measurableSet_negAt_plusPart, ProbabilityTheory.Kernel.IndepFun.indepFun_process₀, MeasurableEquiv.coe_piCurry_symm, ProbabilityTheory.iIndepFun.iIndepFun_process₀, MeasureTheory.Measure.pi_empty_univ, MeasureTheory.generateFrom_measurableCylinders, MeasureTheory.integral_restrict_infinitePi, Measure.eq_prod_of_integral_mul_prod_boundedContinuousFunction', NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, ProbabilityTheory.iIndepFun.iIndepFun_process, ProbabilityTheory.Kernel.lintegral_traj₀, MeasureTheory.measurePreserving_piEquivPiSubtypeProd, MeasureTheory.volume_preserving_finTwoArrow, MeasureTheory.GridLines.T_univ, MeasureTheory.Measure.pi_map_piOptionEquivProd, MeasureTheory.FiniteMeasure.pi_map_pi, MeasureTheory.FiniteMeasure.toMeasure_pi, comap_le_comap_pi, EuclideanSpace.measurableEquiv_toEquiv, EuclideanSpace.euclideanHausdorffMeasure_eq_volume, ProbabilityTheory.Kernel.iIndepFun.indepFun_finset₀, ProbabilityTheory.Kernel.iIndepFun.iIndepFun_process, measurable_piCurry, MeasureTheory.measurePreserving_pi_empty, MeasureTheory.Measure.ae_pi_le_pi, measurable_injection_nat_bool_of_countablySeparated, ProbabilityTheory.IndepFun.process_indepFun₀, MeasureTheory.Measure.ae_eq_set_pi, ProbabilityTheory.Kernel.lmarginalPartialTraj_succ, MeasureTheory.Measure.pi_Iio_ae_eq_pi_Iic, MeasureTheory.Measure.pi.instIsFiniteMeasure, Pi.opensMeasurableSpace_of_subsingleton, pi_eq_generateFrom_projections, ProbabilityTheory.IndepFun.process_indepFun_process₀, MeasureTheory.Measure.instIsProbabilityMeasureForallInfinitePiNat, MeasureTheory.measurableCylinders.measurableSet, MeasureTheory.measurePreserving_finTwoArrow, MeasureTheory.Measure.pi_pi, OrthonormalBasis.measurePreserving_measurableEquiv, MeasureTheory.mem_measurableCylinders, measurable_equivCurry, MeasureTheory.Measure.pi.isAddLeftInvariant, NumberField.mixedEmbedding.fundamentalCone.measurableSet_paramSet, ProbabilityTheory.Kernel.partialTraj_zero, MeasurableEquiv.setOf_apply, MeasureTheory.volume_measurePreserving_sumPiEquivProdPi, Pi.measurableVAdd, Pi.measurableMul, MeasureTheory.volume_preserving_piEquivPiSubtypeProd, ProbabilityTheory.Kernel.lmarginalPartialTraj_eq_lintegral_map, ProbabilityTheory.setBernoulli_apply, NumberField.mixedEmbedding.fundamentalCone.measurableSet_normLeOne, MeasureTheory.charFun_eq_pi_iff, Real.volume_preserving_transvectionStruct, ProbabilityTheory.Kernel.partialTraj_compProd_eq_map_traj, MeasureTheory.volume_measurePreserving_sumPiEquivProdPi_symm, ProbabilityTheory.covariance_eval_multivariateGaussian, ProbabilityTheory.Kernel.setIntegral_traj_partialTraj', MeasureTheory.Measure.infinitePi_map_piCurry_symm, measurable_curry, Pi.borelSpace_of_subsingleton, MeasureTheory.Measure.pi.isOpenPosMeasure, UnitAddTorus.coe_symm_measurableEquivPiIoc_apply, MeasureTheory.integrable_eval, MeasureTheory.Measure.pi.instIsProbabilityMeasure, EuclideanSpace.volume_closedBall, ProbabilityTheory.iIndepFun.indepFun_finset₀, NumberField.mixedEmbedding.measurable_polarSpaceCoord_symm, MeasureTheory.volume_preserving_funUnique, EuclideanSpace.coe_measurableEquiv_symm, MeasureTheory.Measure.infinitePi_pi_univ, MeasurableSet.univ_pi, measurableSet_pi, MeasureTheory.Measure.ae_eval_ne, measurable_piCongrLeft, MeasureTheory.IsProjectiveLimit.isFiniteMeasure, MeasureTheory.cylinderEvents_univ, MeasureTheory.Measure.infinitePi_map_restrict', MeasureTheory.Measure.infinitePi_pi_of_countable, MeasureTheory.measurePreserving_sumPiEquivProdPi, MeasureTheory.Measure.euclideanHausdorffMeasure_def, MeasureTheory.lintegral_eq_of_lmarginal_eq, MeasurableSet.univ_pi', MeasurableEquiv.coe_curry, MeasureTheory.Measure.infinitePi_map_curry, MeasureTheory.isProjectiveLimit_nat_iff', ProbabilityTheory.Kernel.partialTraj_eq_prod, MeasurableEquiv.piMeasurableEquivTProd_symm_apply, MeasureTheory.FiniteMeasure.mass_pi, ProbabilityTheory.Kernel.instIsMarkovKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat, MeasureTheory.IsProjectiveLimit.isProbabilityMeasure, MeasureTheory.Measure.piContent_eq_infinitePiNat, ProbabilityTheory.iIndepFun.indepFun_finset, measurable_piEquivPiSubtypeProd, ZLattice.covolume_eq_det, MeasurableSet.pi, MeasureTheory.Measure.pi.isFiniteMeasureOnCompacts, ProbabilityTheory.setBernoulli_eq_map, MeasureTheory.instIsZeroOrProbabilityMeasureForallValNatMemFinsetInducedFamilyOfForallIic, measurable_update, MeasurableEquiv.piFinSuccAbove_symm_apply, MeasureTheory.Measure.pi_noAtoms', Measure.eq_prod_of_integral_prod_mul_boundedContinuousFunction, ProbabilityTheory.Kernel.traj_eq_prod, MeasurableEquiv.piFinSuccAbove_apply bridge: BoxIntegral.hasIntegralIndicatorConst, MeasureTheory.SimpleFunc.hasBoxIntegral, MeasureTheory.IntegrableOn.hasBoxIntegral, MeasureTheory.SimpleFunc.box_integral_eq_integral
prod 📖	CompOp	8 math math: ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_comp_trim, ProbabilityTheory.Kernel.measurable_densityProcess_countableFiltration_aux, MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_id, comap_prodMk, MeasureTheory.measurable_update_cylinderEvents', comap_prodMap, ProbabilityTheory.compProd_trim_condExpKernel, MeasureTheory.Integrable.comp_snd_map_prod_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_le_comap_pi 📖	mathematical	—	MeasurableSpace instLE comap pi	—	comap_iSup le_iSup_of_le comap_comp le_refl

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableSingletonClass 📖	mathematical	MeasurableSingletonClass	MeasurableSingletonClass MeasurableSpace.pi	—	MeasurableSet.univ_pi MeasurableSingletonClass.measurableSet_singleton Set.univ_pi_singleton

Prod

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	856 math math: MeasureTheory.quasiMeasurePreserving_add, MeasureTheory.Measure.prod_apply_symm, ProbabilityTheory.Kernel.measurable_rnDerivAux, MeasureTheory.lintegral_prod_swap, MeasureTheory.quasiMeasurePreserving_add_swap, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, MeasureTheory.StronglyMeasurable.integral_kernel_prod_right'', associator_inv_hom, ProbabilityTheory.Kernel.integral_fn_integral_add, ProbabilityTheory.stieltjesOfMeasurableRat_ae_eq, MeasureTheory.setLIntegral_prod_symm, ProbabilityTheory.Kernel.swapLeft_zero, ProbabilityTheory.Kernel.instIsMarkovKernelProdSwap, ProbabilityTheory.Kernel.prod_apply', MeasureTheory.NullMeasurable.comp_snd, ProbabilityTheory.indepFun_prod, ProbabilityTheory.Kernel.sectR_apply, ProbabilityTheory.lintegral_condCDF, MeasureTheory.Measure.ae_compProd_of_ae_fst, ProbabilityTheory.condDistrib_apply_of_ne_zero, ProbabilityTheory.Kernel.lintegral_swapRight, NumberField.mixedEmbedding.measurable_polarCoordReal_symm, ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelBorel, ProbabilityTheory.Kernel.integral_integral_sub, ProbabilityTheory.Kernel.instIsMarkovKernelProdCopy, ProbabilityTheory.IsCondKernelCDF.toKernel_Iic, ProbabilityTheory.Kernel.parallelComp_comp_parallelComp, ProbabilityTheory.Kernel.parallelComp_comp_prod, MeasureTheory.ProbabilityMeasure.map_prod_map, MeasureTheory.Measure.swap_comp, MeasureTheory.measurePreserving_prod_mul_swap, MeasureTheory.quasiMeasurePreserving_inv_mul, ProbabilityTheory.lintegral_toKernel_univ, leftUnitor_hom_hom, measurable_deriv_with_param, MeasureTheory.measurePreserving_prod_neg_add, ProbabilityTheory.Kernel.partialTraj_succ_of_le, ProbabilityTheory.Kernel.ae_compProd_of_ae_ae, MeasureTheory.Measure.prod.instNoAtoms_fst, MeasurableAdd₂.measurable_add, MeasureTheory.MemLp.comp_snd, ProbabilityTheory.Kernel.swapRight_apply', ProbabilityTheory.Kernel.map_frestrictLe_trajMeasure_compProd_eq_map_trajMeasure, MeasureTheory.Measure.AbsolutelyContinuous.prod, ProbabilityTheory.Kernel.parallelComp_of_not_isSFiniteKernel_left, MeasureTheory.quasiMeasurePreserving_div_of_right_invariant, ProbabilityTheory.Kernel.swap_swap, MeasureTheory.measure_preimage_fst_singleton_eq_tsum, MeasureTheory.Measure.prod.instSigmaFinite, ProbabilityTheory.Kernel.IsMarkovKernel.compProd, measurable_update', ProbabilityTheory.iCondIndepFun.condIndepFun_prodMk, MeasureTheory.ProbabilityMeasure.prod_prod, ProbabilityTheory.Kernel.ae_null_of_compProd_null, ProbabilityTheory.setIntegral_condCDF, NumberField.mixedEmbedding.measurableSet_plusPart, MeasureTheory.Integrable.mul_prod, ProbabilityTheory.setIntegral_condKernel_univ_left, InformationTheory.rnDeriv_compProd_mul_log_eq_mul_add, MeasureTheory.Measure.comp_compProd_comm, integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux1, HasCompactSupport.measurable_of_prod, ProbabilityTheory.compProd_posterior_eq_map_swap, ProbabilityTheory.Kernel.parallelComp_comm, MeasureTheory.ProbabilityMeasure.prod_swap, ProbabilityTheory.Kernel.apply_eq_measure_condKernel_of_compProd_eq, MeasurableEquiv.finTwoArrow_apply, MeasureTheory.measurePreserving_prod_mul_swap_right, ProbabilityTheory.Kernel.HasSubgaussianMGF.add_compProd, MeasureTheory.hasFiniteIntegral_prod_iff', ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk_prodMk, MeasureTheory.Measure.condKernel_def, ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat_rat, MeasureTheory.setIntegral_prod_swap, MeasureTheory.Measure.nullMeasurable_comp_snd, MeasureTheory.Measure.snd_map_swap, ProbabilityTheory.Kernel.compProd_null, ProbabilityTheory.Kernel.lintegral_id_prod, ProbabilityTheory.Kernel.IsSFiniteKernel.prodMkLeft, ProbabilityTheory.IsRatCondKernelCDF.setIntegral, ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_comp_trim, ProbabilityTheory.setLIntegral_condKernel_univ_right, measurable_fun_prod, ProbabilityTheory.IsCondKernelCDF.integral, Real.integrable_prod_sub, MeasureTheory.Measure.map_fst_prod, ProbabilityTheory.Kernel.swapRight_apply, ProbabilityTheory.Kernel.lintegral_fst, MeasurableMul₂.measurable_mul, ProbabilityTheory.setIntegral_condKernel_univ_right, ProbabilityTheory.Kernel.IsCondKernel.isProbabilityMeasure_ae, measurableSet_graph, ProbabilityTheory.Kernel.fst_comp, MeasureTheory.measurePreserving_prod_div_swap, MeasurableEquiv.piFinTwo_symm_apply, MeasureTheory.Measure.snd_zero, MeasureTheory.measurePreserving_prod_inv_mul_swap, ProbabilityTheory.Kernel.isSFiniteKernel_prodMkRight_iff, MeasureTheory.volume_preserving_piFinsetUnion, ProbabilityTheory.Kernel.ae_compProd_iff, MeasureTheory.StronglyMeasurable.prod_swap, MeasureTheory.Measure.prod.instIsOpenPosMeasure, MeasureTheory.AEStronglyMeasurable.ae_integrable_condKernel_iff, MeasureTheory.MeasurePreserving.prod, ProbabilityTheory.Kernel.swap_apply, ProbabilityTheory.Kernel.measurable_densityProcess_countableFiltration_aux, ProbabilityTheory.Kernel.deterministic_prod_apply', nullMeasurableSet_region_between_co, ProbabilityTheory.Kernel.snd_comp, ProbabilityTheory.Kernel.snd_zero, MeasureTheory.setIntegral_prod_mul, MeasureTheory.ProbabilityMeasure.measurable_fun_prod, ProbabilityTheory.Kernel.compProd_restrict_left, ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_add_compProd, MeasureTheory.Measure.setIntegral_condKernel, measurable_lt, MeasurableEmbedding.prodMap, ProbabilityTheory.integral_stieltjesOfMeasurableRat, MeasureTheory.Measure.nullMeasurableSet_prod, MeasureTheory.measurePreserving_finTwoArrow_vec, nullMeasurableSet_regionBetween, aemeasurable_lineDeriv_uncurry, MeasureTheory.Measure.prod.instIsAddLeftInvariant, ProbabilityTheory.IsRatCondKernelCDFAux.measurable, MeasureTheory.measurePreserving_mul_prod_inv_right, ProbabilityTheory.Kernel.HasSubgaussianMGF.add_comp, ProbabilityTheory.Kernel.fst_prodMkRight, ProbabilityTheory.Kernel.parallelComp_apply_prod, MeasureTheory.Integrable.comp_snd, ProbabilityTheory.Kernel.compProd_zero_right, MeasureTheory.QuasiMeasurePreserving.prod_of_left, MeasurableSpace.instCountablyGeneratedProd, ProbabilityTheory.Kernel.compProd_fst_borelMarkovFromReal_eq_comapRight_compProd, MeasureTheory.Measure.setIntegral_condKernel_univ_left, ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_right, MeasureTheory.Measure.prod_prod_le, ProbabilityTheory.covariance_fst_snd_prod, MeasurableEquiv.coe_sumPiEquivProdPi, MeasureTheory.ProbabilityMeasure.toMeasure_prod, MeasureTheory.prod_withDensity₀, WithLp.borelSpace, ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk₀, MeasurableEquiv.piEquivPiSubtypeProd_apply, MeasureTheory.Measure.lintegral_conv_eq_lintegral_sum, ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelUnitReal, MeasureTheory.Integrable.ae_of_compProd, MeasureTheory.hausdorffMeasure_measurePreserving_piFinTwo, ProbabilityTheory.Kernel.prodMkRight_add, Complex.measurableEquivRealProd_apply, nullMeasurableSet_region_between_cc, MeasureTheory.FiniteMeasure.mass_prod, associator_hom_hom, ProbabilityTheory.Kernel.fst_real_apply, ProbabilityTheory.stieltjesOfMeasurableRat_unit_prod, MeasureTheory.Measure.nullMeasurableSet_preimage_fst, MeasureTheory.TendstoInDistribution.prodMk_of_tendstoInMeasure_const, ProbabilityTheory.Kernel.compProd_deterministic_apply, MeasurableSup₂.measurable_sup, ProbabilityTheory.Kernel.swap_prod, ProbabilityTheory.Kernel.setIntegral_densityProcess_of_mem, MeasureTheory.volume_preserving_prodAssoc, MeasureTheory.lintegral_lintegral_symm, ProbabilityTheory.Kernel.map_prod_eq, tensorObj_str, MeasureTheory.Measure.snd_map_prodMk₀, MeasureTheory.Integrable.comp_snd_map_prodMk, MeasureTheory.prod_withDensity_left, ProbabilityTheory.Kernel.compProd_eq_tsum_compProd, ProbabilityTheory.Kernel.prodMkLeft_apply, MeasurableEquiv.coe_IicProdIoc_symm, ProbabilityTheory.Kernel.comapRight_compProd_id_prod, MeasureTheory.charFunDual_prod, ContinuousLinearMap.measurable_apply₂, MeasureTheory.Measure.fst_map_swap, MeasureTheory.Measure.instSFiniteProdCompProd, borelSpace, MeasureTheory.integral_integral_symm, ProbabilityTheory.Kernel.ae_ae_of_ae_compProd, Module.Basis.prod_addHaar, MeasureTheory.Measure.MutuallySingular.compProd_of_left, MeasureTheory.charFun_eq_prod_iff, measurable_from_prod_countable_right, MeasureTheory.Measure.integral_condKernel, AEMeasurable.comp_snd, MeasureTheory.quasiMeasurePreserving_neg_add_swap, ProbabilityTheory.rnDeriv_measure_compProd_left, ProbabilityTheory.condDistrib_ae_eq_iff_measure_eq_compProd, ProbabilityTheory.Kernel.measurable_density, ProbabilityTheory.Kernel.instIsCondKernel_zero, ProbabilityTheory.compProd_map_condDistrib, aemeasurable_deriv_with_param, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, MeasureTheory.Measure.mutuallySingular_compProd_right_iff, MeasureTheory.FiniteMeasure.prod_swap, ProbabilityTheory.Kernel.prod_apply, ProbabilityTheory.Kernel.isSFiniteKernel_prodMkRight_unit, AEMeasurable.prod_swap, ProbabilityTheory.Kernel.prod_const_comp, ProbabilityTheory.Kernel.setIntegral_densityProcess_of_le, MeasureTheory.Measure.ae_prod_iff_ae_ae, MeasureTheory.Measure.compProd_id, ProbabilityTheory.isRatCondKernelCDF_preCDF, ProbabilityTheory.Kernel.IsMarkovKernel.swapRight, MeasureTheory.Measure.prod_apply_le, ProbabilityTheory.Kernel.le_compProd_apply, ProbabilityTheory.Kernel.prodMkLeft_add, MeasurablePow.measurable_pow, ProbabilityTheory.Kernel.fst_apply, MeasureTheory.Measure.pi_prod_map_IocProdIoc, MeasureTheory.Measure.setIntegral_compProd, MeasureTheory.FiniteMeasure.map_fst_prod, ProbabilityTheory.setLIntegral_condKernel, ProbabilityTheory.lintegral_condKernel, MeasurableDiv₂.measurable_div, ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_map_map, ProbabilityTheory.Kernel.compProd_eq_sum_compProd, MeasureTheory.charFunDual_eq_prod_iff, MeasureTheory.measurePreserving_prod_add_right, MeasureTheory.volume_preserving_piFinSuccAbove, ProbabilityTheory.IsCondKernelCDF.setIntegral, ProbabilityTheory.bayesRisk_compProd_le_bayesRisk, MeasureTheory.Measure.setIntegral_condKernel_univ_right, MeasureTheory.Measure.prod.instIsMulRightInvariant, ProbabilityTheory.Kernel.ae_kernel_lt_top, ProbabilityTheory.Kernel.prod_prodMkRight_comp_deterministic_prod, MeasureTheory.Measure.condKernel_apply_of_ne_zero, ProbabilityTheory.Kernel.copy_apply, ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk_prodMk₀, MeasureTheory.Measure.prod_apply, MeasureTheory.Measure.compProd_assoc', ProbabilityTheory.Kernel.parallelComp_def, ProbabilityTheory.Kernel.prod_of_not_isSFiniteKernel_right, MeasureTheory.Measure.compProd_apply_univ, MeasureTheory.Measure.AbsolutelyContinuous.compProd_right, MeasureTheory.Measure.ae_prod_mem_iff_ae_ae_mem, ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_left, MeasureTheory.Measure.compProd_apply, ProbabilityTheory.Kernel.fst_prodMkLeft, ProbabilityTheory.Kernel.partialTraj_compProd_traj, ProbabilityTheory.Kernel.IsMarkovKernel.prod, ProbabilityTheory.Kernel.lintegral_prodMkRight, ProbabilityTheory.Kernel.integral_integral_add', MeasureTheory.ProbabilityMeasure.map_fst_prod, ProbabilityTheory.Kernel.measurable_densityProcess, MeasureTheory.Measure.ext_prod₃_iff', MeasurableSub₂.measurable_sub, ProbabilityTheory.IsCondKernelCDF.setLIntegral, ProbabilityTheory.Kernel.condKernelCountable_apply, measurableSet_pi_polarCoord_target, MeasureTheory.Measure.comap_swap, MeasureTheory.measurePreserving_add_prod_neg_right, MeasurableVAdd₂.measurable_vadd, MeasureTheory.measurePreserving_arrowProdEquivProdArrow, measurableSet_swap_iff, MeasureTheory.Measure.FiniteAtFilter.prod, MeasureTheory.Measure.snd_sum, ProbabilityTheory.Kernel.measurable_rnDeriv, measurableSet_prod_of_nonempty, MeasureTheory.Measure.compProd_map, MeasureTheory.Measure.AbsolutelyContinuous.compProd, ProbabilityTheory.Kernel.condKernel_apply_eq_condKernel, ProbabilityTheory.Kernel.partialTraj_le_def, ProbabilityTheory.Kernel.meas_countablePartitionSet_le_of_fst_le, StandardBorelSpace.prod, ProbabilityTheory.Kernel.IsMarkovKernel.swapLeft, ProbabilityTheory.Kernel.tendsto_integral_density_of_monotone, ProbabilityTheory.condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map, ProbabilityTheory.Kernel.parallelComp_sum_left, ProbabilityTheory.Kernel.prodMkRight_zero, Measurable.lintegral_kernel_prod_right'', ProbabilityTheory.Kernel.id_prod_apply', ProbabilityTheory.Kernel.instIsSFiniteKernelProdParallelComp, ProbabilityTheory.Kernel.snd_prodMkRight, MeasureTheory.Measure.AbsolutelyContinuous.compProd_of_compProd, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, volume_regionBetween_eq_lintegral', measurable_prodMk_right, generateFrom_prod, ProbabilityTheory.Kernel.lintegral_compProd₀, ProbabilityTheory.Kernel.prodAssoc_symm_prod, MeasureTheory.measurePreserving_prod_sub_swap, ProbabilityTheory.posterior_prod_id_comp, Measurable.prodMk, MeasurableSet.prod, NumberField.mixedEmbedding.covolume_idealLattice, MeasurableEmbedding.prodMk_right, NumberField.mixedEmbedding.volume_preserving_negAt, InformationTheory.integrable_llr_compProd_iff, MeasureTheory.Measure.map_prod_map, MeasureTheory.Measure.compProd_id_eq_copy_comp, ProbabilityTheory.hasFiniteIntegral_compProd_iff', MeasureTheory.measurePreserving_piFinTwo, measurableSet_region_between_co, MeasureTheory.quasiMeasurePreserving_neg_add, MeasureTheory.Measure.pi_prod_map_IicProdIoc, ProbabilityTheory.Kernel.prodAssoc_prod, ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat, MeasureTheory.hausdorffMeasure_prod_real, MeasureTheory.Measure.prod_swap, MeasurableInf₂.measurable_inf, measurableSet_region_between_oc, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left', MeasureTheory.Measure.measure_prod_null_of_ae_null, ProbabilityTheory.Kernel.isSFiniteKernel_prodMkLeft_unit, MeasureTheory.Measure.lintegral_condKernel, MeasureTheory.measurePreserving_prod_div, MeasureTheory.Measure.prod_restrict, ProbabilityTheory.Kernel.IsFiniteKernel.prodMkRight, MeasureTheory.Measure.zero_prod, MeasureTheory.Measure.prod_prod, ProbabilityTheory.Kernel.snd_map_prod, ProbabilityTheory.setLIntegral_condKernel_univ_left, MeasureTheory.Measure.compProd_withDensity, MeasureTheory.QuasiMeasurePreserving.prod_of_right, WithLp.volume_preserving_toLp, MeasureTheory.Measure.compProd_sum_left, MeasureTheory.Measure.prod.instIsAddRightInvariant, ProbabilityTheory.Kernel.setLIntegral_compProd_univ_left, ProbabilityTheory.Kernel.compProd_prodMkLeft_eq_comp, MeasureTheory.Integrable.integral_compProd, MeasureTheory.AEStronglyMeasurable.integral_kernel_condKernel, MeasureTheory.Measure.parallelComp_comp_compProd, ProbabilityTheory.Kernel.setIntegral_density_of_measurableSet, ProbabilityTheory.Kernel.prod_of_not_isSFiniteKernel_left, MeasureTheory.integrable_prod_iff, MeasureTheory.Measure.prod.instIsProbabilityMeasure, ProbabilityTheory.Kernel.parallelComp_id_right_comp_parallelComp, ProbabilityTheory.Kernel.IsFiniteKernel.swapLeft, ProbabilityTheory.aestronglyMeasurable_comp_snd_map_prodMk_iff, MeasureTheory.partialTraj_const, ProbabilityTheory.Kernel.swap_copy, MeasureTheory.Measure.mutuallySingular_compProd_iff, ProbabilityTheory.Kernel.compProd_eq_zero_iff, MeasureTheory.Measure.quasiMeasurePreserving_fst, MeasureTheory.measurePreserving_prodAssoc, ProbabilityTheory.Kernel.lintegral_compProd', measurable_from_prod_countable_right', ProbabilityTheory.IdentDistrib.prodMk, MeasureTheory.continuous_integral_integral, stronglyMeasurable_lineDeriv_uncurry, ProbabilityTheory.Kernel.prodMkRight_apply, MeasureTheory.Measure.fst_apply, ProbabilityTheory.setIntegral_compProd_univ_right, ProbabilityTheory.charFun_map_add_prod_eq_mul, ProbabilityTheory.Kernel.IsSFiniteKernel.prod, MeasureTheory.Measure.fst_univ, NumberField.mixedEmbedding.volume_preserving_mixedSpaceToRealMixedSpace_symm, ProbabilityTheory.Kernel.measurable_singularPart_fun, MeasureTheory.integral_prod_mul, ProbabilityTheory.Kernel.comap_prod, ProbabilityTheory.Kernel.partialTraj_succ_self, MeasureTheory.quasiMeasurePreserving_sub_of_right_invariant, ProbabilityTheory.Kernel.instIsMarkovKernelProdOfSectL, MeasureTheory.Measure.integrable_compProd_iff, ProbabilityTheory.Kernel.continuous_integral_integral, ProbabilityTheory.Kernel.id_parallelComp_id, MeasureTheory.Measure.instIsZeroOrProbabilityMeasureProdCompProdOfIsZeroOrMarkovKernel, ENNReal.measurable_of_measurable_nnreal_prod, ProbabilityTheory.indepFun_iff_charFunDual_prod', ProbabilityTheory.setLIntegral_toKernel_univ, MeasureTheory.lintegral_rnDeriv_compProd, InformationTheory.klDiv_compProd_eq_add, MeasureTheory.Measure.prod.instIsMulLeftInvariant, ProbabilityTheory.Kernel.parallelComp_comp_copy, ProbabilityTheory.integrable_comp_snd_map_prodMk_iff, ProbabilityTheory.Kernel.lintegral_prod, ProbabilityTheory.condDistrib_snd_prod, ProbabilityTheory.Kernel.exists_measurable_map_eq_unitInterval, ProbabilityTheory.Kernel.setIntegral_densityProcess, MeasureTheory.AEStronglyMeasurable.compProd_mk_left, aestronglyMeasurable_lineDeriv_uncurry, ENNReal.measurable_of_measurable_nnreal_nnreal, instMeasurableSingletonClass, MeasureTheory.prod_withDensity_left₀, ProbabilityTheory.Kernel.swap_comp_eq_map, MeasureTheory.Measure.setLIntegral_condKernel, MeasureTheory.Measure.compProd_eq_comp_prod, measurable_IicProdIoc, MeasureTheory.measurePreserving_piFinSuccAbove, MeasureTheory.FiniteMeasure.prod_apply, ProbabilityTheory.Kernel.integral_densityProcess, MeasureTheory.Measure.dirac_prod_dirac, MeasureTheory.Measure.MutuallySingular.compProd_of_right', ProbabilityTheory.condCDF_eq_stieltjesOfMeasurableRat_unit_prod, MeasureTheory.measure_preimage_snd_singleton_eq_sum, ProbabilityTheory.Kernel.snd_map_prod_id, MeasureTheory.prod_withDensity_right₀, MeasureTheory.Measure.IicSnd_apply, MeasureTheory.Integrable.integral_norm_compProd, MeasureTheory.Measure.dirac_unit_compProd_const, ProbabilityTheory.Kernel.integral_fn_integral_sub, ProbabilityTheory.indepFun_iff_charFun_prod, MeasurableEquiv.coe_IicProdIoc, ProbabilityTheory.IsCondKernelCDF.measurable, MeasureTheory.Measure.compProd_deterministic, MeasureTheory.Measure.quasiMeasurePreserving_snd, ProbabilityTheory.lintegral_toKernel_mem, NumberField.mixedEmbedding.measurableSet_fundamentalCone, ProbabilityTheory.Kernel.snd_prodMkLeft, ProbabilityTheory.Kernel.parallelComp_apply', MeasureTheory.Measure.prod.instIsLocallyFiniteMeasure, MeasureTheory.Measure.integrable_compProd_snd_iff, ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelUnitBorel, MeasureTheory.Measure.absolutelyContinuous_compProd_left_iff, MeasureTheory.integral_continuousLinearMap_prod, ProbabilityTheory.Kernel.id_parallelComp_comp_parallelComp_id, Measurable.prodMap, integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2, ProbabilityTheory.Kernel.measurableSet_mutuallySingularSet, MeasureTheory.Measure.fst_add, ProbabilityTheory.Kernel.setLIntegral_density, MeasureTheory.Measure.nullMeasurableSet_prod_of_ne_zero, Complex.measurableEquivRealProd_symm_polarCoord_symm_apply, Complex.volume_preserving_equiv_real_prod, ProbabilityTheory.variance_add_prod, ProbabilityTheory.Kernel.lintegral_snd, ProbabilityTheory.IsGaussian.map_rotation_eq_self, ProbabilityTheory.hasFiniteIntegral_prodMk_left, ProbabilityTheory.Kernel.deterministic_comp_copy, MeasureTheory.Measure.lintegral_condKernel_mem, ProbabilityTheory.Kernel.integral_integral_sub', MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd, MeasureTheory.Integrable.convolution_integrand, ProbabilityTheory.Kernel.IsSFiniteKernel.swapLeft, MeasureTheory.lintegral_prod, ProbabilityTheory.isCondKernelCDF_stieltjesOfMeasurableRat, ProbabilityTheory.Kernel.parallelComp_sum_right, NumberField.mixedEmbedding.covolume_integerLattice, ProbabilityTheory.Kernel.comap_sectL, ProbabilityTheory.Kernel.lintegral_prod_symm, InformationTheory.integral_llr_compProd_eq_add, leftUnitor_inv_hom, MeasureTheory.integral_continuousLinearMap_prod', MeasureTheory.Measure.dirac_prod, MeasureTheory.Measure.MutuallySingular.compProd_of_right, MeasureTheory.pdf.indepFun_iff_pdf_prod_eq_pdf_mul_pdf, ProbabilityTheory.Kernel.integral_density, MeasureTheory.integral_integral, MeasureTheory.Measure.absolutelyContinuous_compProd_of_compProd, MeasureTheory.Measure.integral_compProd, ProbabilityTheory.Kernel.compProd_apply_univ_le, measurableSet_regionBetween, ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.swapRight, ProbabilityTheory.Kernel.IsSFiniteKernel.prodMkRight, ProbabilityTheory.Kernel.lintegral_density, MeasurableEq.measurableSet_diagonal, ProbabilityTheory.Kernel.sectR_zero, ProbabilityTheory.iIndepFun.indepFun_prodMk, MeasureTheory.quasiMeasurePreserving_mul_swap, ProbabilityTheory.Kernel.compProd_sum_left, ProbabilityTheory.Kernel.compProd_fst_borelMarkovFromReal, ProbabilityTheory.Kernel.swapRight_eq, ProbabilityTheory.Kernel.measurable_densityProcess_aux, ProbabilityTheory.integrable_compProd_iff, ProbabilityTheory.rnDeriv_compProd, MeasureTheory.Measure.prod.instIsAddHaarMeasure, MeasureTheory.Measure.compProd_zero_left, ProbabilityTheory.Kernel.sectL_zero, MeasureTheory.Measure.instIsFiniteMeasureProdCompProdOfIsFiniteKernel, MeasureTheory.Integrable.comp_fst_iff, MeasurableEquiv.piEquivPiSubtypeProd_symm_apply, ProbabilityTheory.Kernel.prodComm_prod, ProbabilityTheory.Kernel.prodMkLeft_apply', ProbabilityTheory.Kernel.const_prod_comp, rightUnitor_inv_hom, ProbabilityTheory.Kernel.snd_eq, ProbabilityTheory.iCondIndepFun.condIndepFun_prodMk_prodMk, measurable_swap, MeasureTheory.AEStronglyMeasurable.prod_swap, MeasureTheory.AEEqFun.comp₂Measurable_eq_mk, MeasureTheory.Measure.prod_dirac, measurable_lineDeriv_uncurry, ProbabilityTheory.condDistrib_def, MeasureTheory.StronglyMeasurable.comp_snd, MeasureTheory.Integrable.comp_fst, ProbabilityTheory.Kernel.deterministic_prod_deterministic, measurable_le, ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_prodMk, measurable_updateFinset', MeasureTheory.Measure.compProd_apply_prod, ProbabilityTheory.parallelProd_posterior_comp_copy_comp, ProbabilityTheory.Kernel.isFiniteKernel_of_isFiniteKernel_snd, ProbabilityTheory.Kernel.fst_apply', MeasureTheory.integrable_continuousLinearMap_prod', MeasureTheory.volume_preserving_piFinTwo, ProbabilityTheory.setIntegral_condKernel, EReal.measurable_of_real_prod, generateFrom_prod_eq, ProbabilityTheory.Kernel.IsMarkovKernel.prodMkRight, MeasureTheory.Measure.set_prod_ae_eq, MeasureTheory.AEStronglyMeasurable.ae_integrable_condDistrib_map_iff, ProbabilityTheory.Kernel.fst_eq, ProbabilityTheory.setLIntegral_toKernel_prod, ProbabilityTheory.HasGaussianLaw.prodMk, ProbabilityTheory.Kernel.lintegral_deterministic_prod, ProbabilityTheory.setIntegral_compProd, MeasureTheory.measurePreserving_prod_sub, MeasureTheory.Measure.snd_univ, MeasureTheory.MemLp.comp_fst, measurableSet_lineDifferentiableAt_uncurry, MeasureTheory.Measure.snd_map_prodMk, ProbabilityTheory.Kernel.setLIntegral_compProd, MeasureTheory.Measure.ext_prod₃_iff, ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.prod, ProbabilityTheory.Kernel.snd_apply', MeasureTheory.Integrable.swap, MeasureTheory.ProbabilityMeasure.continuous_prod, ProbabilityTheory.Kernel.snd_apply, MeasureTheory.integral_prod_swap, AEMeasurable.prodMk, MeasureTheory.measurePreserving_prod_add, nullMeasurableSet_lt', ProbabilityTheory.Kernel.deterministic_parallelComp_deterministic, MeasureTheory.measurePreserving_mul_prod, ProbabilityTheory.swap_compProd_posterior, WithLp.volume_preserving_symm_measurableEquiv_toLp_prod, MeasureTheory.Measure.prod_sum_right, MeasureTheory.Measure.iInf_rat_gt_prod_Iic, MeasurableSMul₂.measurable_smul, MeasurableEmbedding.prodMk_left, measurable_snd, MeasureTheory.Measure.prod_add, ProbabilityTheory.Kernel.integral_integral_add, MeasureTheory.integrable_prod_iff', ProbabilityTheory.Kernel.compProd_preimage_fst, ProbabilityTheory.integral_condCDF, ProbabilityTheory.Kernel.instIsMarkovKernelCondKernel, ProbabilityTheory.Kernel.compProd_eq_sum_compProd_left, NumberField.mixedEmbedding.volume_preserving_homeoRealMixedSpacePolarSpace, MeasureTheory.quasiMeasurePreserving_sub, MeasureTheory.measurePreserving_prod_add_swap_right, MeasureTheory.Measure.compProd_assoc, ProbabilityTheory.Kernel.prodMkRight_apply', ProbabilityTheory.Kernel.compProd_add_right, ProbabilityTheory.Kernel.parallelComp_of_not_isSFiniteKernel_right, MeasurableEquiv.coe_sumPiEquivProdPi_symm, ProbabilityTheory.variance_dual_prod', measurableSet_le', generateFrom_eq_prod, ProbabilityTheory.Kernel.prod_prodMkLeft_comp_prod_deterministic, ProbabilityTheory.isRatCondKernelCDFAux_preCDF, ProbabilityTheory.Kernel.swapRight_zero, MeasureTheory.StronglyMeasurable.integral_kernel_prod_left'', MeasureTheory.Measure.prod_smul_right, ProbabilityTheory.integrable_kernel_prodMk_left, ProbabilityTheory.Kernel.compProd_apply_univ, MeasureTheory.measurePreserving_add_prod, MeasureTheory.charFunDual_prod', MeasureTheory.Measure.setLIntegral_condKernel_univ_left, MeasureTheory.integral_prod_symm, MeasureTheory.Measure.fst_map_prodMk₀, volume_regionBetween_eq_integral', ProbabilityTheory.isCondKernelCDF_condCDF, ProbabilityTheory.Kernel.instIsMarkovKernelProdOfSectR, MeasureTheory.integrable_swap_iff, MeasurableEquiv.finTwoArrow_symm_apply, NumberField.mixedEmbedding.measurable_polarCoord_symm, MeasureTheory.Measure.compProd_add_left, MeasureTheory.Measure.prod_sum, MeasureTheory.Integrable.comp_snd_iff, ProbabilityTheory.Kernel.lintegral_parallelComp_symm, MeasureTheory.Measure.prod.instIsHaarMeasure, MeasureTheory.Measure.mutuallySingular_compProd_left_iff, MeasureTheory.measurePreserving_piFinsetUnion, ProbabilityTheory.instIsMarkovKernel_toKernel, MeasureTheory.integral_fun_fst, MeasureTheory.FiniteMeasure.prod_apply_symm, MeasureTheory.volume_measurePreserving_arrowProdEquivProdArrow, WithLp.volume_preserving_ofLp, ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.compProd, ProbabilityTheory.charFunDual_map_add_prod_eq_mul, MeasureTheory.Integrable.op_fst_snd, MeasureTheory.ae_eq_of_setLIntegral_prod_eq, ProbabilityTheory.Kernel.setLIntegral_compProd_univ_right, ProbabilityTheory.Kernel.parallelComp_zero_right, ProbabilityTheory.Kernel.compProd_zero_left, MeasureTheory.Measure.prod_comp_left, MeasureTheory.AEStronglyMeasurable.comp_snd_iff, ProbabilityTheory.Kernel.map_prodMkRight, MeasureTheory.Measure.prod.instSFinite, MeasureTheory.lintegral_prod_le, ProbabilityTheory.Kernel.prod_zero, MeasureTheory.hasFiniteIntegral_prod_iff, MeasureTheory.Measure.absolutelyContinuous_compProd_iff', ProbabilityTheory.iIndepFun.indepFun_prodMk_prodMk, ProbabilityTheory.Kernel.compProd_restrict, MeasureTheory.Measure.prod.instIsFiniteMeasure, MeasureTheory.FiniteMeasure.prod_prod, ProbabilityTheory.Kernel.compProd_assoc, ProbabilityTheory.setLIntegral_condKernel_eq_measure_prod, Measurable.map_prodMk_right, ProbabilityTheory.Kernel.compProd_def, ProbabilityTheory.Kernel.fst_map_id_prod, MeasureTheory.Measure.prod.instNoAtoms_snd, ProbabilityTheory.Kernel.IsFiniteKernel.prod, measurable_fderiv_with_param, ProbabilityTheory.IndepFun.hasGaussianLaw, ProbabilityTheory.iIndepFun.indepFun_prodMk_prodMk₀, MeasureTheory.Measure.prod.instIsFiniteMeasureOnCompacts, ProbabilityTheory.Kernel.lintegral_prod_deterministic, measurableSet_of_differentiableAt_of_isComplete_with_param, ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral_iInf_rat_gt, MeasureTheory.Measure.setLIntegral_compProd, MeasureTheory.prod_withDensity, MeasurableEquiv.piFinTwo_apply, ProbabilityTheory.Kernel.condKernel_def, measurable_piEquivPiSubtypeProd_symm, MeasureTheory.AEStronglyMeasurable.comp_fst, MeasureTheory.Measure.compProd_sum_right, ProbabilityTheory.Kernel.compProd_add_left, MeasureTheory.IntegrableOn.swap, MeasureTheory.lintegral_prod_symm, ProbabilityTheory.Kernel.indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map, ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelReal, ProbabilityTheory.hasFiniteIntegral_compProd_iff, ProbabilityTheory.setIntegral_compProd_univ_left, ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight, MeasureTheory.Measure.compProd_of_not_sfinite, ProbabilityTheory.Kernel.sectL_apply, measurable_from_prod_countable_left, MeasureTheory.Measure.nullMeasurableSet_preimage_snd, MeasureTheory.measureReal_prod_prod, MeasureTheory.integrable_continuousLinearMap_prod, MeasureTheory.Measure.instIsProbabilityMeasureProdCompProdOfIsMarkovKernel, ProbabilityTheory.IsRatCondKernelCDF.measurable, ProbabilityTheory.Kernel.lintegral_prodMkLeft, MeasureTheory.MeasurePreserving.skew_product, MeasureTheory.Measure.dirac_compProd_apply, measurableEmbedding_prodMk_left, MeasureTheory.lintegral_prod_symm', MeasureTheory.Measure.prod_comp_right, MeasureTheory.Measure.measure_prod_null, ProbabilityTheory.Kernel.setIntegral_density, MeasureTheory.Measure.compProd_zero_right, measurable_nndist, ProbabilityTheory.condDistrib_fst_prod, MeasureTheory.lintegral_prod_mul, MeasureTheory.Measure.compProd_of_not_isSFiniteKernel, ProbabilityTheory.variance_dual_prod, volume_regionBetween_eq_integral, MeasureTheory.Measure.prod_sum_left, ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map', ProbabilityTheory.setLIntegral_condCDF, MeasureTheory.QuasiMeasurePreserving.prodMap, MeasureTheory.AEStronglyMeasurable.integral_kernel_compProd, MeasureTheory.measurePreserving_prod_add_swap, measurableEmbedding_prod_mk_right, nullMeasurableSet_region_between_oc, MeasureTheory.measurePreserving_prod_mul, prod_le_borel_prod, MeasureTheory.Measure.ae_compProd_of_ae_ae, MeasureTheory.Measure.prodAssoc_prod, HasCompactSupport.exists_simpleFunc_approx_of_prod, ProbabilityTheory.lintegral_stieltjesOfMeasurableRat, ProbabilityTheory.Kernel.map_prodMkLeft, MeasureTheory.Measure.compProd_eq_zero_iff, MeasureTheory.Measure.IicSnd_univ, MeasureTheory.Integrable.smul_prod, MeasureTheory.stronglyMeasurable_uncurry_of_continuous_of_stronglyMeasurable, MeasureTheory.Measure.copy_comp_map, MeasureTheory.prod_withDensity_right, MeasureTheory.lintegral_lintegral, ProbabilityTheory.rnDeriv_compProd_withDensity_rnDeriv, HasCompactSupport.stronglyMeasurable_of_prod, measurable_IocProdIoc, ProbabilityTheory.Kernel.parallelComp_apply, ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectR, ProbabilityTheory.Kernel.map_prod_map, ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft, MeasureTheory.Measure.add_prod, MeasureTheory.measurePreserving_prod_inv_mul, ProbabilityTheory.HasGaussianLaw.toLp_prodMk, MeasureTheory.measurePreserving_sumPiEquivProdPi_symm, NumberField.mixedEmbedding.measurableSet_negAt_plusPart, MeasureTheory.measurePreserving_snd, MeasureTheory.measurePreserving_mul_prod_inv, ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.prodMkLeft, ProbabilityTheory.Kernel.isSFiniteKernel_prodMkLeft_iff, MeasureTheory.Measure.compProd_smul_left, MeasureTheory.ProbabilityMeasure.map_snd_prod, MeasureTheory.Measure.snd_add, MeasureTheory.Measure.setLIntegral_condKernel_univ_right, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, whiskerRight_hom, measurableSet_region_between_cc, stronglyMeasurable_deriv_with_param, MeasureTheory.AEStronglyMeasurable.comp_fst_iff, ProbabilityTheory.Kernel.compProd_apply, ProbabilityTheory.IsCondKernelCDF.lintegral, MeasureTheory.Measure.fst_map_prodMk, ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelProdParallelComp, ProbabilityTheory.Kernel.prod_const, MeasureTheory.Measure.compProd_add_right, ProbabilityTheory.Kernel.IsFiniteKernel.compProd, MeasureTheory.measurePreserving_piEquivPiSubtypeProd, ProbabilityTheory.instIsGaussianProdProdOfSecondCountableTopologyEither, MeasureTheory.Measure.measurePreserving_swap, MeasureTheory.volume_preserving_finTwoArrow, measurableSet_lt', rightUnitor_hom_hom, MeasureTheory.AEEqFun.comp₂Measurable_eq_pair, MeasureTheory.Measure.pi_map_piOptionEquivProd, ProbabilityTheory.eq_condKernel_of_kernel_eq_compProd, Measurable.prod, MeasureTheory.Measure.prod_zero, MeasureTheory.Measure.nullMeasurable_comp_fst, ProbabilityTheory.Kernel.compProd_eq_sum_compProd_right, MeasureTheory.Measure.ae_compProd_iff, ProbabilityTheory.integral_condKernel, MeasureTheory.Measure.prod_def, measurable_from_prod_countable_left', MeasureTheory.Measure.absolutelyContinuous_compProd_right_iff, ProbabilityTheory.Kernel.fst_map_prod, ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map, MeasureTheory.Measure.snd_apply, MeasureTheory.Measure.dirac_unit_compProd, MeasureTheory.Measure.fst_zero, measurable_edist, ProbabilityTheory.Kernel.sum_prodMkRight, measurable_swap_iff, ProbabilityTheory.Kernel.swapLeft_apply', MeasureTheory.ProbabilityMeasure.prod_apply_symm, ProbabilityTheory.indepFun_prod₀, MeasureTheory.AEStronglyMeasurable.comp_snd_map_prodMk, ProbabilityTheory.lintegral_condKernel_mem, ProbabilityTheory.compProd_posterior_eq_swap_comp, ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.prodMkRight, ProbabilityTheory.Kernel.lintegral_fn_integral_sub, ProbabilityTheory.integral_compProd, MeasureTheory.Measure.prodMkLeft_comp_compProd, MeasureTheory.integral_prod_smul, MeasureTheory.Measure.fst_sum, ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral, MeasureTheory.FiniteMeasure.measurable_fun_prod, MeasureTheory.FiniteMeasure.map_snd_prod, ConvexOn.apply_rnDeriv_ae_le_integral, ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat_rat, ProbabilityTheory.Kernel.compProd_sum_right, MeasureTheory.AEStronglyMeasurable.convolution_integrand', ProbabilityTheory.rnDeriv_posterior_ae_prod, Complex.measurableEquivRealProd_symm_apply, MeasureTheory.quasiMeasurePreserving_mul, ProbabilityTheory.condKernel_const, Measurable.map_prodMk_left, ProbabilityTheory.Kernel.lintegral_compProd, MeasureTheory.measurePreserving_finTwoArrow, ProbabilityTheory.Kernel.comap_prod_swap, ProbabilityTheory.Kernel.id_prod_eq, ProbabilityTheory.Kernel.HasSubgaussianMGF.prodMkLeft_compProd, MeasureTheory.integral_fun_snd, ProbabilityTheory.Kernel.comap_sectR, MeasureTheory.AEStronglyMeasurable.convolution_integrand, MeasureTheory.measure_preimage_snd_singleton_eq_tsum, ProbabilityTheory.Kernel.parallelComp_apply_univ, ProbabilityTheory.Kernel.swap_parallelComp, ProbabilityTheory.Kernel.lintegral_parallelComp, MeasureTheory.StronglyMeasurable.comp_fst, ProbabilityTheory.Kernel.map_prod_swap, ProbabilityTheory.Kernel.isFiniteKernel_of_isFiniteKernel_fst, ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk, MeasureTheory.volume_measurePreserving_sumPiEquivProdPi, MeasureTheory.Measure.AbsolutelyContinuous.compProd_left, ProbabilityTheory.Kernel.densityProcess_def, MeasureTheory.ProbabilityMeasure.prod_apply, MeasureTheory.volume_preserving_piEquivPiSubtypeProd, MeasureTheory.Measure.compProd_eq_parallelComp_comp_copy_comp, MeasureTheory.NullMeasurableSet.prod, ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat, ProbabilityTheory.Kernel.lintegral_swapLeft, NumberField.mixedEmbedding.fundamentalCone.measurableSet_normLeOne, measurableSet_prod, measurable_fderiv_apply_const_with_param, aestronglyMeasurable_deriv_with_param, ProbabilityTheory.Kernel.prodMkLeft_zero, MeasureTheory.FiniteMeasure.map_prod_map, ProbabilityTheory.Kernel.compProd_apply_prod, IsUnifLocDoublingMeasure.prod, MeasureTheory.Measure.lintegral_mconv_eq_lintegral_prod, ProbabilityTheory.Kernel.partialTraj_compProd_eq_map_traj, MeasureTheory.Measure.AbsolutelyContinuous.mutuallySingular_compProd_iff, MeasureTheory.volume_measurePreserving_sumPiEquivProdPi_symm, MeasureTheory.measurePreserving_div_prod, MeasureTheory.FiniteMeasure.zero_prod, MeasureTheory.charFun_prod, MeasureTheory.Measure.condKernel_apply, measurable_fst, whiskerLeft_hom, volume_regionBetween_eq_lintegral, MeasureTheory.charFunDual_eq_prod_iff', MeasureTheory.integral_prod, MeasureTheory.AEStronglyMeasurable.comp_snd, MeasureTheory.Measure.lintegral_compProd, ProbabilityTheory.Kernel.IsSFiniteKernel.compProd, ProbabilityTheory.Kernel.IsMarkovKernel.prodMkLeft, MeasureTheory.Measure.restrict_prod_eq_prod_univ, NumberField.mixedEmbedding.measurable_polarSpaceCoord_symm, ProbabilityTheory.Kernel.IsFiniteKernel.prodMkLeft, measurable_prodMk_left, MeasureTheory.Measure.absolutelyContinuous_compProd_iff, MeasureTheory.Measure.setLIntegral_condKernel_eq_measure_prod, ProbabilityTheory.Kernel.instIsFiniteKernelProdParallelComp, MeasureTheory.measurePreserving_prod_neg_add_swap, MeasureTheory.Measure.ae_eq_compProd_of_ae_eq_fst, ProbabilityTheory.Kernel.sum_prodMkLeft, ProbabilityTheory.iIndepFun.indepFun_prodMk₀, ProbabilityTheory.Kernel.condKernelCountable.instIsMarkovKernel, MeasureTheory.Measure.map_snd_prod, MeasureTheory.measurePreserving_add_prod_neg, MeasureTheory.AEEqFun.comp₂Measurable_mk_mk, ProbabilityTheory.Kernel.swap_apply', MeasureTheory.Measure.IsCondKernel.apply_of_ne_zero, MeasureTheory.measure_preimage_fst_singleton_eq_sum, MeasureTheory.measurePreserving_sumPiEquivProdPi, InformationTheory.klDiv_compProd_left, MeasureTheory.setIntegral_prod, ProbabilityTheory.Kernel.fst_zero, ProbabilityTheory.Kernel.instIsMarkovKernelProdParallelComp, MeasureTheory.NullMeasurable.comp_fst, ProbabilityTheory.Kernel.compProd_restrict_right, MeasureTheory.FiniteMeasure.toMeasure_prod, ProbabilityTheory.Kernel.parallelComp_id_left_comp_parallelComp, MeasureTheory.Measure.ext_prod_iff, ProbabilityTheory.Kernel.swapLeft_apply, ProbabilityTheory.Kernel.fst_compProd_apply, ProbabilityTheory.Kernel.partialTraj_eq_prod, MeasureTheory.FiniteMeasure.prod_zero, ProbabilityTheory.Kernel.parallelComp_zero_left, MeasureTheory.measurable_uncurry_of_continuous_of_measurable, MeasureTheory.quasiMeasurePreserving_div, ProbabilityTheory.setLIntegral_toKernel_Iic, ProbabilityTheory.IsCondKernelCDF.toKernel_apply, MeasureTheory.setLIntegral_prod, AEMeasurable.comp_fst, ProbabilityTheory.Kernel.IsFiniteKernel.swapRight, MeasureTheory.measurePreserving_sub_prod, MeasureTheory.measurePreserving_prod_mul_right, measurableSet_of_differentiableAt_with_param, ProbabilityTheory.IsGaussian.map_rotation_eq_self_of_forall_strongDual_eq_zero, measurable_piEquivPiSubtypeProd, MeasureTheory.Measure.prod_smul_left, MeasureTheory.Measure.measure_prod_compl_eq_zero, ProbabilityTheory.Kernel.prod_apply_prod, ProbabilityTheory.Kernel.zero_prod, EReal.measurable_of_real_real, MeasurableEquiv.piFinSuccAbove_symm_apply, ProbabilityTheory.indepFun_iff_charFunDual_prod, ProbabilityTheory.integrable_stieltjesOfMeasurableRat, ProbabilityTheory.Kernel.lintegral_prod_id, ProbabilityTheory.Kernel.IsSFiniteKernel.swapRight, ProbabilityTheory.Kernel.traj_eq_prod, MeasurableEquiv.piFinSuccAbove_apply, opensMeasurableSpace, MeasureTheory.quasiMeasurePreserving_inv_mul_swap, MeasureTheory.measurePreserving_fst, ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib, measurable_dist

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableSingletonClass 📖	mathematical	—	MeasurableSingletonClass instMeasurableSpace	—	MeasurableSet.prod MeasurableSet.singleton Set.singleton_prod_singleton

Quot

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	1 math math: measurable_quot_mk

Quotient

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	28 math math: MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_of_zero, MeasureTheory.instSigmaFiniteQuotientOrbitRelOfHasFundamentalDomainOfQuotientMeasureEqMeasurePreimageVolume, MeasureTheory.instSigmaFiniteAddQuotientOrbitRelInstMeasurableSpaceToMeasurableSpace, MeasureTheory.IsAddFundamentalDomain.addQuotientMeasure_eq, MeasureTheory.IsFundamentalDomain.quotientMeasure_eq, MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addProjection_respects_measure', MeasureTheory.QuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient, MeasureTheory.addMeasure_map_restrict_apply, MeasureTheory.IsAddFundamentalDomain.measurePreserving_add_quotient_mk, MeasureTheory.QuotientMeasureEqMeasurePreimage.projection_respects_measure', MeasureTheory.QuotientMeasureEqMeasurePreimage.isFiniteMeasure_quotient, MeasureTheory.measure_map_restrict_apply, measurable_from_quotient, MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_of_zero, measurable_quotient_mk', MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_addQuotientMeasure, MeasureTheory.AddQuotientMeasureEqMeasurePreimage.isFiniteMeasure_quotient, MeasureTheory.AddQuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient, MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure_apply, MeasureTheory.IsFundamentalDomain.projection_respects_measure, MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_quotientMeasure, measurableSet_quotient, MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure, instDiscreteMeasurableSpace, MeasureTheory.IsFundamentalDomain.measurePreserving_quotient_mk, measurable_quotient_mk'', MeasureTheory.IsFundamentalDomain.projection_respects_measure_apply, borelSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDiscreteMeasurableSpace 📖	mathematical	—	DiscreteMeasurableSpace instMeasurableSpace	—	measurableSet_quotient MeasurableSet.of_discrete

QuotientAddGroup

Definitions

Name	Category	Theorems
measurableSpace 📖	CompOp	36 math math: AddCircle.volume_eq_smul_haarAddCircle, AddCircle.isAddFundamentalDomain_of_ae_ball, AddCircle.integral_haarAddCircle, measurableVAdd, UnitAddTorus.coe_symm_measurableEquivPiIoc, MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addInvariantMeasure_quotient, orthonormal_fourier, MeasureTheory.memLp_haarAddCircle_iff, Polynomial.toAddCircle.integrable, hasSum_fourier_series_L2, UnitAddTorus.measurePreserving_equivPiIoc, measurable_from_quotient, AddCircle.instIsProbabilityMeasureRealHaarAddCircle, fourierCoeff_toLp, coe_fourierBasis, measurable_coe, instDiscreteMeasurableSpace, UnitAddCircle.measurePreserving_mk, UnitAddTorus.coe_measurableEquivPiIoc_apply, span_fourierLp_closure_eq_top, MeasureTheory.MemLp.haarAddCircle, UnitAddTorus.coe_measurableEquivPiIoc, AddCircle.measurePreserving_mk, AddCircle.measurable_mk', hasSum_sq_fourierCoeff, fourierBasis_repr, measurePreserving_quotientAddGroup_mk_of_AddQuotientMeasureEqMeasurePreimage, MeasureTheory.Integrable.fourier_smul, tsum_sq_fourierCoeff, borelSpace, MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addHaarMeasure_quotient, MeasureTheory.AddQuotientMeasureEqMeasurePreimage.vaddInvariantMeasure_quotient, UnitAddTorus.coe_symm_measurableEquivPiIoc_apply, coeFn_fourierLp, AddCosetSpace.borelSpace, IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_vaddAddHaarMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDiscreteMeasurableSpace 📖	mathematical	—	DiscreteMeasurableSpace HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup measurableSpace	—	Quotient.instDiscreteMeasurableSpace
measurable_coe 📖	mathematical	—	Measurable HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup measurableSpace	—	measurable_quotient_mk''
measurable_from_quotient 📖	mathematical	—	Measurable HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup measurableSpace	—	measurable_from_quotient

QuotientGroup

Definitions

Name	Category	Theorems
measurableSpace 📖	CompOp	11 math math: borelSpace, instDiscreteMeasurableSpace, MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient, MeasureTheory.QuotientMeasureEqMeasurePreimage.haarMeasure_quotient, measurableSMul, MeasureTheory.QuotientMeasureEqMeasurePreimage.smulInvariantMeasure_quotient, IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_smulHaarMeasure, measurable_coe, CosetSpace.borelSpace, measurable_from_quotient, measurePreserving_quotientGroup_mk_of_QuotientMeasureEqMeasurePreimage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDiscreteMeasurableSpace 📖	mathematical	—	DiscreteMeasurableSpace HasQuotient.Quotient Subgroup instHasQuotientSubgroup measurableSpace	—	Quotient.instDiscreteMeasurableSpace
measurable_coe 📖	mathematical	—	Measurable HasQuotient.Quotient Subgroup instHasQuotientSubgroup measurableSpace	—	measurable_quotient_mk''
measurable_from_quotient 📖	mathematical	—	Measurable HasQuotient.Quotient Subgroup instHasQuotientSubgroup measurableSpace	—	measurable_from_quotient

Set

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	34 math math: MeasurableSet.sep_infinite, SimpleGraph.measurable_edgeSet, SimpleGraph.binomialRandom_apply', ProbabilityTheory.setBernoulli_one, ProbabilityTheory.setBernoulli_singleton, ProbabilityTheory.setBernoulli_apply', MeasurableSet.setOf_finite, SimpleGraph.binomialRandom_eq_map, measurable_encard, measurable_setOf, MeasurableSet.setOf_infinite, SimpleGraph.measurable_fromEdgeSet, measurable_set_iff, ProbabilityTheory.setBernoulli_zero, ProbabilityTheory.measurable_countablePartitionSet, MeasurableSet.sep_finite, SimpleGraph.measurableEmbedding_edgeSet, measurable_set_mem, measurableSet_mem, measurable_compl, measurable_set_notMem, MeasurableEquiv.coe_setOf, MeasurableEquiv.setOf_symm_apply, instMeasurableSingletonClass, ProbabilityTheory.instIsProbabilityMeasureSetSetBernoulli, ProbabilityTheory.setBernoulli_ae_subset, ProbabilityTheory.measurable_partitionFiltration_memPartitionSet, measurableSet_notMem, MeasurableEquiv.setOf_apply, ProbabilityTheory.setBernoulli_apply, ProbabilityTheory.measurable_countableFiltration_countablePartitionSet, ProbabilityTheory.measurable_memPartitionSet, ProbabilityTheory.setBernoulli_eq_map, measurable_ncard

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableSingletonClass 📖	mathematical	—	MeasurableSingletonClass Set instMeasurableSpace	—	—
measurable_restrict 📖	mathematical	—	Measurable MeasurableSpace.pi Elem Set instMembership restrict	—	measurable_pi_lambda measurable_pi_apply
measurable_restrict_apply 📖	mathematical	Measurable	Measurable Elem Subtype.instMeasurableSpace Set instMembership restrict	—	Measurable.comp measurable_subtype_coe
measurable_restrict₂ 📖	mathematical	Set instHasSubset	Measurable MeasurableSpace.pi Elem Set instMembership restrict₂	—	measurable_pi_lambda measurable_pi_apply
measurable_restrict₂_apply 📖	mathematical	Set instHasSubset Measurable Elem Subtype.instMeasurableSpace instMembership	Measurable Elem Subtype.instMeasurableSpace Set instMembership restrict₂	—	Measurable.comp measurable_inclusion

Sigma

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	—

Subtype

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	89 math math: measurable_subtype_coe, measurable_iUnionLift, MeasurableSpace.Subtype.separatesPoints, volume_set_coe_def, ProbabilityTheory.unitInterval.cdf_eq_real, MeasureTheory.Measure.measure_subtype_coe_le_comap, MeasurableSet.standardBorel, unitInterval.coe_symmMeasurableEquiv, MeasureTheory.Measure.toSphere_real_apply_univ, UnitAddTorus.coe_symm_measurableEquivPiIoc, Submonoid.instMeasurableSMul, opensMeasurableSpace, unitInterval.symmMeasurableEquiv_apply, Measurable.subtype_mk, Measurable.codRestrict, MeasureTheory.Measure.exists_measurable_map_eq, aemeasurable_restrict_iff_comap_subtype, measurableEmbedding_sigmoid, measurableEmbedding_sigmoid_comp_embeddingReal, MeasureTheory.exists_subset_real_measurableEquiv, MeasureTheory.Measure.toSphere_apply_univ, MeasurableEmbedding.equivRange_apply, MeasureTheory.measurableEmbedding_of_fderivWithin, MeasureTheory.Measure.instIsFiniteMeasureElemSphereOfNatRealToSphere, MeasurableEmbedding.measurable_rangeSplitting, unitInterval.measurable_symm, UnitAddTorus.measurePreserving_equivPiIoc, MeasureTheory.lintegral_subtype_comap, MeasureTheory.integrableOn_iff_comap_subtypeVal, MeasurableSpace.Subtype.countablySeparated, MeasurableSet.exists_measurable_proj, AddSubgroup.instMeasurableVAdd, MeasurableSet.image_inclusion, MeasurableSpace.CountablySeparated.subtype_iff, comap_subtype_coe_apply, unitInterval.symmMeasurableEquiv_symm_apply, ContinuousOn.measurableEmbedding, MeasureTheory.Measure.toSphere_apply', ProbabilityTheory.Kernel.exists_measurable_map_eq_unitInterval, ae_restrict_iff_subtype, MeasureTheory.measurableEquiv_range_coe_nat_of_infinite_of_countable, MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd, MeasureTheory.Measure.instSigmaFiniteElemRealIoiOfNatVolumeIoiPow, AddCircle.measurePreserving_equivIoc, MeasurableSpace.instCountablyGeneratedSubtype, instBorelSpaceSubtypeMemOpens, MeasurableSet.image_inclusion', Set.measurable_restrict_apply, MeasureTheory.Measure.toSphereBallBound_mul_measureReal_unitBall_le_toSphere_ball, MeasureTheory.measurePreserving_subtype_coe, UnitAddTorus.coe_measurableEquivPiIoc_apply, MeasureTheory.setLIntegral_subtype, Subgroup.instMeasurableSMul, MeasureTheory.integral_subtype_comap, Measurable.measurableSet_preimage_iff_preimage_val, Measurable.rangeFactorization, Set.measurable_restrict₂_apply, MeasureTheory.locallyIntegrable_comap, MeasureTheory.exists_nat_measurableEquiv_range_coe_fin_of_finite, MeasurableSpace.measurableEquiv_nat_bool_of_countablyGenerated, MeasureTheory.restrict_map_withDensity_abs_det_fderiv_eq_addHaar, UnitAddTorus.coe_measurableEquivPiIoc, MeasurableEmbedding.equivRange_symm_apply_mk, MeasurableSpace.countablySeparated_subtype_of_hasCountableSeparatingOn, instCountablySeparatedElemOfHasCountableSeparatingOnIsOpen, Measurable.subtype_map, MeasureTheory.hausdorffMeasure_orthogonalProjection_le, unitInterval.measurableEmbedding_coe, Finset.measurable_restrict_apply, MeasureTheory.Measure.volumeIoiPow_apply_Iio, MeasureTheory.Measure.toSphereBallBound_mul_measure_unitBall_le_toSphere_ball, AddSubmonoid.instMeasurableVAdd, borelSpace, map_comap_subtype_coe, MeasureTheory.Measure.toSphere_eq_zero_iff_finrank, Finset.measurable_restrict₂_apply, instMeasurableSingletonClass, AEMeasurable.subtype_mk, MeasurableSet.of_subtype_image, AffineSubspace.euclideanHausdorffMeasure_coe_image, MeasureTheory.Measure.toSphere.instIsOpenPosMeasure, UnitAddTorus.coe_symm_measurableEquivPiIoc_apply, LinearMap.exists_map_addHaar_eq_smul_addHaar', MeasureTheory.Measure.toSphere_apply_univ', unitInterval.symm_symmMeasurableEquiv, MeasurableEmbedding.subtype_coe, measurable_inclusion, MeasureTheory.Measure.toSphere_eq_zero_iff, Measurable.measurable_comp_iff_restrict

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableSingletonClass 📖	mathematical	—	MeasurableSingletonClass instMeasurableSpace	—	MeasurableSingletonClass.measurableSet_singleton Set.image_singleton Set.preimage_image_eq val_injective

Sum

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	12 math math: measurable_inl, Measurable.sumMap, measurableSet_inr_image, measurable_inr, measurableSet_range_inl, measurable_fun_sum, measurableSet_sum_iff, MeasurableSet.inl_image, measurableSet_range_inr, measurableSet_inl_image, MeasurableSet.inr_image, Measurable.sumElim

TProd

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	9 math math: MeasureTheory.Measure.sigmaFinite_tprod, measurable_tProd_elim', MeasurableSet.tProd, measurable_tProd_elim, measurable_tProd_mk, MeasurableEquiv.piMeasurableEquivTProd_apply, MeasureTheory.Measure.tprod_cons, MeasureTheory.Measure.tprod_tprod, MeasurableEquiv.piMeasurableEquivTProd_symm_apply

ULift

Definitions

Name	Category	Theorems
instMeasurableSpace 📖	CompOp	7 math math: measurable_down, measurableSet_preimage_down, measurable_up, instBorelSpace, MeasureTheory.isProbabilityMeasure_comap_down, MeasureTheory.isProbabilityMeasure_map_up, measurableSet_preimage_up

(root)

Definitions

Name	Category	Theorems
MeasurableEq 📖	CompData	4 math math: instMeasurableEqOfMeasurableSingletonClassOfCountable, instMeasurableEqOfMeasurableSingletonClassOfMeasurableSub₂, instMeasurableEqOfCanonicallyOrderedAddOfOrderedSubOfMeasurableSub₂OfMeasurableSingletonClass, instMeasurableEqOfSecondCountableTopologyOfT2Space
measurableAtom 📖	CompOp	8 math math: mem_measurableAtom_self, measurableAtom_subset_of_mem, measurableAtom_eq_of_mem, MeasurableSet.measurableAtom_of_countable, disjoint_measurableAtom_of_notMem, MeasureTheory.Measure.exists_sum_smul_dirac, measurableAtom_subset, measurableAtom_of_measurableSingletonClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjoint_measurableAtom_of_notMem 📖	mathematical	Set Set.instMembership measurableAtom	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 measurableAtom	—	Set.disjoint_iff_inter_eq_empty Set.ext measurableAtom_eq_of_mem mem_measurableAtom_self
exists_measurable_piecewise 📖	mathematical	MeasurableSet Measurable Pairwise Set.EqOn Set Set.instInter	Measurable Set.EqOn	—	eq_or_ne Set.Subset.rfl measurable_iUnionLift Measurable.comp measurable_subtype_coe Measurable.dite MeasurableSet.iUnion Set.mem_iUnion Set.iUnionLift_of_mem
instMeasurableEqOfMeasurableSingletonClassOfCountable 📖	mathematical	—	MeasurableEq	—	Set.range_eq_iUnion Set.iUnion_singleton_eq_range Set.range_diag MeasurableSet.of_discrete MeasurableSingletonClass.toDiscreteMeasurableSpace Prod.instMeasurableSingletonClass instCountableProd
instMeasurableSingletonClassOfMeasurableEq 📖	mathematical	—	MeasurableSingletonClass	—	Measurable.eq measurable_id' measurable_const
measurableAtom_eq_of_mem 📖	mathematical	Set Set.instMembership measurableAtom	measurableAtom	—	subset_antisymm Set.instAntisymmSubset measurableAtom_subset_of_mem MeasurableSet.compl
measurableAtom_of_measurableSingletonClass 📖	mathematical	—	measurableAtom Set Set.instSingletonSet	—	Set.Subset.antisymm measurableAtom_subset MeasurableSingletonClass.measurableSet_singleton
measurableAtom_subset 📖	mathematical	MeasurableSet Set Set.instMembership	Set Set.instHasSubset measurableAtom	—	Set.iInter₂_subset_of_subset Set.iInter_congr_Prop Set.iInter_true
measurableAtom_subset_of_mem 📖	mathematical	Set Set.instMembership measurableAtom	Set Set.instHasSubset measurableAtom	—	—
measurableSet_eq_fun 📖	mathematical	Measurable	MeasurableSet setOf	—	MeasurableSet.preimage MeasurableEq.measurableSet_diagonal Measurable.prodMk
measurableSet_inl_image 📖	mathematical	—	MeasurableSet Sum.instMeasurableSpace Set.image	—	Function.Injective.preimage_image Sum.inl_injective Set.preimage_inr_image_inl
measurableSet_inr_image 📖	mathematical	—	MeasurableSet Sum.instMeasurableSpace Set.image	—	Set.preimage_inl_image_inr Function.Injective.preimage_image Sum.inr_injective
measurableSet_mem 📖	mathematical	—	MeasurableSet Set Set.instMeasurableSpace setOf Set.instMembership	—	measurableSet_setOf measurable_set_mem
measurableSet_notMem 📖	mathematical	—	MeasurableSet Set Set.instMeasurableSpace setOf Set.instMembership	—	measurableSet_setOf measurable_set_notMem
measurableSet_pi 📖	mathematical	—	MeasurableSet MeasurableSpace.pi Set.pi Set Set.instEmptyCollection	—	Set.eq_empty_or_nonempty measurableSet_pi_of_nonempty
measurableSet_pi_of_nonempty 📖	mathematical	Set.Nonempty Set.pi	MeasurableSet MeasurableSpace.pi Set.pi	—	Set.update_preimage_pi measurable_update MeasurableSet.pi
measurableSet_preimage_down 📖	mathematical	—	MeasurableSet ULift.instMeasurableSpace Set.preimage	—	—
measurableSet_preimage_up 📖	mathematical	—	MeasurableSet Set.preimage ULift.instMeasurableSpace	—	—
measurableSet_prod 📖	mathematical	—	MeasurableSet Prod.instMeasurableSpace SProd.sprod Set Set.instSProd Set.instEmptyCollection	—	Set.eq_empty_or_nonempty Set.prod_eq_empty_iff measurableSet_prod_of_nonempty Set.prod_nonempty_iff
measurableSet_prod_of_nonempty 📖	mathematical	Set.Nonempty SProd.sprod Set Set.instSProd	MeasurableSet Prod.instMeasurableSpace SProd.sprod Set Set.instSProd	—	measurable_prodMk_right measurable_prodMk_left Set.mk_preimage_prod_left Set.mk_preimage_prod_right MeasurableSet.prod
measurableSet_quotient 📖	mathematical	—	MeasurableSet Quotient.instMeasurableSpace Set.preimage Quotient.mk''	—	—
measurableSet_range_inl 📖	mathematical	—	MeasurableSet Sum.instMeasurableSpace Set.range	—	Set.image_univ MeasurableSet.inl_image MeasurableSet.univ
measurableSet_range_inr 📖	mathematical	—	MeasurableSet Sum.instMeasurableSpace Set.range	—	Set.image_univ MeasurableSet.inr_image MeasurableSet.univ
measurableSet_setOf 📖	mathematical	—	MeasurableSet setOf Measurable Prop.instMeasurableSpace	—	measurable_to_prop Set.preimage_singleton_true MeasurableSingletonClass.measurableSet_singleton Prop.instMeasurableSingletonClass
measurableSet_sum_iff 📖	mathematical	—	MeasurableSet Sum.instMeasurableSpace Set.preimage	—	—
measurableSet_swap_iff 📖	mathematical	—	MeasurableSet Prod.instMeasurableSpace Set.preimage	—	measurable_swap
measurable_compl 📖	mathematical	—	Measurable Set Set.instMeasurableSpace Compl.compl Set.instCompl	—	measurable_set_iff measurable_set_notMem
measurable_curry 📖	mathematical	—	Measurable MeasurableSpace.pi	—	measurable_pi_lambda measurable_pi_apply
measurable_down 📖	mathematical	—	Measurable ULift.instMeasurableSpace	—	—
measurable_eq_mp 📖	mathematical	—	Measurable	—	measurable_id
measurable_equivCurry 📖	mathematical	—	Measurable MeasurableSpace.pi DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.curry	—	measurable_curry
measurable_equivCurry_symm 📖	mathematical	—	Measurable MeasurableSpace.pi DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Equiv.curry	—	measurable_uncurry
measurable_find 📖	mathematical	MeasurableSet setOf	Measurable Nat.instMeasurableSpace Nat.find	—	measurable_to_nat preimage_find_eq_disjointed MeasurableSet.disjointed
measurable_findGreatest 📖	mathematical	MeasurableSet setOf	Measurable Nat.instMeasurableSpace Nat.findGreatest	—	measurable_findGreatest' Set.setOf_forall Set.iInter_congr_Prop MeasurableSet.inter MeasurableSet.const MeasurableSet.iInter Prop.countable instCountableNat MeasurableSet.compl
measurable_findGreatest' 📖	mathematical	MeasurableSet setOf Nat.findGreatest	Measurable Nat.instMeasurableSpace Nat.findGreatest	—	measurable_to_nat Nat.findGreatest_le
measurable_from_nat 📖	mathematical	—	Measurable Nat.instMeasurableSpace	—	measurable_from_top
measurable_from_prod_countable_left 📖	mathematical	Measurable	Measurable Prod.instMeasurableSpace	—	measurable_from_prod_countable_left' measurableAtom_of_measurableSingletonClass
measurable_from_prod_countable_left' 📖	mathematical	Measurable	Measurable Prod.instMeasurableSpace	—	Set.ext mem_measurableAtom_self MeasurableSet.iUnion MeasurableSet.prod MeasurableSet.measurableAtom_of_countable
measurable_from_prod_countable_right 📖	mathematical	Measurable	Measurable Prod.instMeasurableSpace	—	measurable_from_prod_countable_right' measurableAtom_of_measurableSingletonClass
measurable_from_prod_countable_right' 📖	mathematical	Measurable	Measurable Prod.instMeasurableSpace	—	Measurable.comp measurable_from_prod_countable_left' measurable_swap
measurable_from_quotient 📖	mathematical	—	Measurable Quotient.instMeasurableSpace Quotient.mk''	—	—
measurable_fst 📖	mathematical	—	Measurable Prod.instMeasurableSpace	—	Measurable.of_comap_le le_sup_left
measurable_fun_prod 📖	mathematical	—	Measurable Prod.instMeasurableSpace	—	Measurable.comp measurable_fst measurable_snd Measurable.prod
measurable_fun_sum 📖	mathematical	Measurable	Measurable Sum.instMeasurableSpace	—	Measurable.of_comap_le le_inf MeasurableSpace.comap_le_iff_le_map
measurable_iUnionLift 📖	mathematical	Set Set.instMembership Set.instHasSubset Set.iUnion MeasurableSet Measurable Set.Elem Subtype.instMeasurableSpace	Measurable Set.Elem Subtype.instMeasurableSpace Set Set.instMembership Set.iUnionLift	—	Set.subset_iUnion Set.preimage_iUnionLift MeasurableSet.preimage MeasurableSet.iUnion MeasurableSet.image_inclusion measurable_inclusion
measurable_inclusion 📖	mathematical	Set Set.instHasSubset	Measurable Set.Elem Subtype.instMeasurableSpace Set Set.instMembership Set.inclusion	—	Measurable.subtype_map measurable_id
measurable_inl 📖	mathematical	—	Measurable Sum.instMeasurableSpace	—	Measurable.of_le_map inf_le_left
measurable_inr 📖	mathematical	—	Measurable Sum.instMeasurableSpace	—	Measurable.of_le_map inf_le_right
measurable_liftCover 📖	mathematical	MeasurableSet Measurable Set.Elem Subtype.instMeasurableSpace Set Set.instMembership Set.iUnion Set.univ	Measurable Set.liftCover	—	Set.preimage_liftCover MeasurableSet.iUnion MeasurableSet.subtype_image
measurable_mem 📖	mathematical	—	Measurable Prop.instMeasurableSpace Set Set.instMembership MeasurableSet	—	measurableSet_setOf
measurable_of_measurable_on_compl_finite 📖	mathematical	Measurable Set.Elem Compl.compl Set Set.instCompl Subtype.instMeasurableSpace Set.instMembership Set.restrict	Measurable	—	Set.Finite.to_subtype measurable_of_restrict_of_restrict_compl Set.Finite.measurableSet measurable_of_finite Subtype.instMeasurableSingletonClass
measurable_of_measurable_on_compl_singleton 📖	mathematical	Measurable Set.Elem setOf Subtype.instMeasurableSpace Set Set.instMembership Set.restrict	Measurable	—	measurable_of_measurable_on_compl_finite Set.finite_singleton
measurable_of_measurable_union_cover 📖	mathematical	MeasurableSet Set Set.instHasSubset Set.univ Set.instUnion Measurable Set.Elem Subtype.instMeasurableSpace Set.instMembership	Measurable	—	MeasurableSet.of_union_cover
measurable_of_restrict_of_restrict_compl 📖	mathematical	MeasurableSet Measurable Set.Elem Subtype.instMeasurableSpace Set Set.instMembership Set.restrict Compl.compl Set.instCompl	Measurable	—	measurable_of_measurable_union_cover MeasurableSet.compl Eq.ge Set.union_compl_self
measurable_piCongrLeft 📖	mathematical	—	Measurable MeasurableSpace.pi DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.piCongrLeft	—	measurable_pi_iff Equiv.apply_symm_apply Equiv.piCongrLeft_apply_eq_cast Measurable.eq_mp measurable_pi_apply
measurable_piCurry 📖	mathematical	—	Measurable MeasurableSpace.pi DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.piCurry	—	measurable_sigmaCurry
measurable_piCurry_symm 📖	mathematical	—	Measurable MeasurableSpace.pi DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Equiv.piCurry	—	measurable_sigmaUncurry
measurable_piEquivPiSubtypeProd 📖	mathematical	—	Measurable MeasurableSpace.pi Prod.instMeasurableSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.piEquivPiSubtypeProd	—	Measurable.prodMk measurable_pi_iff measurable_pi_apply
measurable_piEquivPiSubtypeProd_symm 📖	mathematical	—	Measurable Prod.instMeasurableSpace MeasurableSpace.pi DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Equiv.piEquivPiSubtypeProd	—	measurable_pi_iff measurable_pi_apply Measurable.comp measurable_fst measurable_snd
measurable_pi_apply 📖	mathematical	—	Measurable MeasurableSpace.pi	—	measurable_pi_iff measurable_id
measurable_pi_iff 📖	mathematical	—	Measurable MeasurableSpace.pi	—	MeasurableSpace.comap_iSup MeasurableSpace.comap_comp
measurable_pi_lambda 📖	mathematical	Measurable	Measurable MeasurableSpace.pi	—	measurable_pi_iff
measurable_prodMk_left 📖	mathematical	—	Measurable Prod.instMeasurableSpace	—	Measurable.prodMk measurable_const measurable_id
measurable_prodMk_right 📖	mathematical	—	Measurable Prod.instMeasurableSpace	—	Measurable.prodMk measurable_id measurable_const
measurable_quot_mk 📖	mathematical	—	Measurable Quot.instMeasurableSpace	—	—
measurable_quotient_mk' 📖	mathematical	—	Measurable Quotient.instMeasurableSpace	—	—
measurable_quotient_mk'' 📖	mathematical	—	Measurable Quotient.instMeasurableSpace Quotient.mk''	—	—
measurable_setOf 📖	mathematical	—	Measurable Set MeasurableSpace.pi Prop.instMeasurableSpace Set.instMeasurableSpace setOf	—	measurable_id
measurable_set_iff 📖	mathematical	—	Measurable Set Set.instMeasurableSpace Prop.instMeasurableSpace Set.instMembership	—	measurable_pi_iff
measurable_set_mem 📖	mathematical	—	Measurable Set Set.instMeasurableSpace Prop.instMeasurableSpace Set.instMembership	—	measurable_pi_apply
measurable_set_notMem 📖	mathematical	—	Measurable Set Set.instMeasurableSpace Prop.instMeasurableSpace Set.instMembership	—	Measurable.comp Measurable.of_discrete instDiscreteMeasurableSpace measurable_set_mem
measurable_sigmaCurry 📖	mathematical	—	Measurable MeasurableSpace.pi Sigma.curry	—	measurable_pi_lambda measurable_pi_apply
measurable_sigmaUncurry 📖	mathematical	—	Measurable MeasurableSpace.pi Sigma.uncurry	—	measurable_pi_lambda Measurable.fun_comp measurable_pi_apply
measurable_snd 📖	mathematical	—	Measurable Prod.instMeasurableSpace	—	Measurable.of_comap_le le_sup_right
measurable_subtype_coe 📖	mathematical	—	Measurable Subtype.instMeasurableSpace	—	MeasurableSpace.le_map_comap
measurable_swap 📖	mathematical	—	Measurable Prod.instMeasurableSpace	—	Measurable.prod measurable_snd measurable_fst
measurable_swap_iff 📖	mathematical	—	Measurable Prod.instMeasurableSpace	—	Measurable.comp measurable_swap
measurable_tProd_elim 📖	mathematical	—	Measurable List.TProd TProd.instMeasurableSpace List.TProd.elim	—	List.TProd.elim_self measurable_fst List.TProd.elim_of_ne Measurable.comp measurable_snd
measurable_tProd_elim' 📖	mathematical	—	Measurable List.TProd TProd.instMeasurableSpace MeasurableSpace.pi List.TProd.elim'	—	measurable_pi_lambda measurable_tProd_elim
measurable_tProd_mk 📖	mathematical	—	Measurable List.TProd MeasurableSpace.pi TProd.instMeasurableSpace	—	measurable_const Measurable.prodMk measurable_pi_apply
measurable_to_bool 📖	mathematical	MeasurableSet Set.preimage Set Set.instSingletonSet	Measurable Bool.instMeasurableSpace	—	measurable_to_countable' Bool.countable Set.preimage_compl Bool.compl_singleton MeasurableSet.compl
measurable_to_countable 📖	mathematical	MeasurableSet Set.preimage Set Set.instSingletonSet	Measurable	—	Set.biUnion_preimage_singleton MeasurableSet.iUnion Prop.countable Set.preimage_singleton_eq_empty
measurable_to_countable' 📖	mathematical	MeasurableSet Set.preimage Set Set.instSingletonSet	Measurable	—	measurable_to_countable
measurable_to_nat 📖	mathematical	MeasurableSet Set.preimage Set Set.instSingletonSet	Measurable Nat.instMeasurableSpace	—	measurable_to_countable instCountableNat
measurable_to_prop 📖	mathematical	MeasurableSet Set.preimage Set Set.instSingletonSet	Measurable Prop.instMeasurableSpace	—	measurable_to_countable' Prop.countable' Set.preimage_singleton_true Set.preimage_singleton_false Prop.compl_singleton MeasurableSet.compl
measurable_uncurry 📖	mathematical	—	Measurable MeasurableSpace.pi	—	measurable_pi_lambda Measurable.fun_comp measurable_pi_apply
measurable_uniqueElim 📖	mathematical	—	Measurable Unique.instInhabited MeasurableSpace.pi uniqueElim	—	measurable_id
measurable_unit 📖	mathematical	—	Measurable PUnit.instMeasurableSpace	—	measurable_from_top
measurable_up 📖	mathematical	—	Measurable ULift.instMeasurableSpace	—	—
measurable_update 📖	mathematical	—	Measurable MeasurableSpace.pi Function.update	—	Measurable.comp measurable_update' measurable_prodMk_left
measurable_update' 📖	mathematical	—	Measurable Prod.instMeasurableSpace MeasurableSpace.pi Function.update	—	measurable_pi_iff measurable_snd measurable_fst
measurable_updateFinset 📖	mathematical	—	Measurable MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Function.updateFinset	—	Measurable.comp measurable_updateFinset' measurable_prodMk_left
measurable_updateFinset' 📖	mathematical	—	Measurable Prod.instMeasurableSpace MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Function.updateFinset	—	—
measurable_updateFinset_left 📖	mathematical	—	Measurable MeasurableSpace.pi Function.updateFinset	—	Measurable.comp measurable_updateFinset' measurable_prodMk_right
measurable_update_left 📖	mathematical	—	Measurable MeasurableSpace.pi Function.update	—	Measurable.comp measurable_update' measurable_prodMk_right
mem_measurableAtom_self 📖	mathematical	—	Set Set.instMembership measurableAtom	—	—
mem_of_mem_measurableAtom 📖	mathematical	Set Set.instMembership measurableAtom MeasurableSet	Set Set.instMembership	—	—

---

← Back to Index