Restrict

📁 Source: Mathlib/MeasureTheory/Measure/Restrict.lean

Statistics

Metric	Count
Definitions measureSpace, restrict, restrictₗ	3
Theorems restrict, ae_map_iff, comap_apply, comap_map, comap_preimage, comap_restrict, map_comap, restrict_comap, restrict_map, comap_apply, restrict_map, map_coe_volume, restrict, nullMeasurableSet_subtype_coe, subtype_coe, ae_eq_comp, restrict, volume_def, volume_univ, absolutelyContinuous_restrict, exists_mem_of_measure_ne_zero_of_ae, ext_iff_of_biUnion_eq_univ, ext_iff_of_iUnion_eq_univ, ext_iff_of_sUnion_eq_univ, ext_of_biUnion_eq_univ, ext_of_generateFrom_of_cover, ext_of_generateFrom_of_cover_subset, ext_of_generateFrom_of_iUnion, ext_of_iUnion_eq_univ, ext_of_sUnion_eq_univ, le_restrict_apply, map_eq_comap, measure_inter_eq_zero_of_restrict, measure_subtype_coe_eq_zero_of_comap_eq_zero, measure_subtype_coe_le_comap, neZero, restrict_add, restrict_add_restrict_compl, restrict_apply, restrict_apply', restrict_apply_eq_zero, restrict_apply_eq_zero', restrict_apply_le, restrict_apply_self, restrict_apply_superset, restrict_apply_univ, restrict_apply₀, restrict_apply₀', restrict_biUnion, restrict_biUnion_congr, restrict_biUnion_finset, restrict_biUnion_finset_congr, restrict_biUnion_le, restrict_comm, restrict_compl_add_restrict, restrict_congr_meas, restrict_congr_mono, restrict_congr_set, restrict_empty, restrict_eq_self, restrict_eq_self_of_ae_mem, restrict_eq_zero, restrict_finset_biUnion_congr, restrict_iUnion, restrict_iUnion_ae, restrict_iUnion_apply, restrict_iUnion_apply_ae, restrict_iUnion_apply_eq_iSup, restrict_iUnion_congr, restrict_iUnion_le, restrict_inter_add_diff, restrict_inter_add_diff₀, restrict_inter_toMeasurable, restrict_le_self, restrict_map, restrict_mono, restrict_mono', restrict_mono_ae, restrict_mono_measure, restrict_mono_set, restrict_restrict, restrict_restrict', restrict_restrict_of_subset, restrict_restrict₀, restrict_restrict₀', restrict_sInf_eq_sInf_restrict, restrict_sUnion_congr, restrict_smul, restrict_sum, restrict_sum_of_countable, restrict_toMeasurable, restrict_toOuterMeasure_eq_toOuterMeasure_restrict, restrict_union, restrict_union', restrict_union_add_inter, restrict_union_add_inter', restrict_union_add_inter₀, restrict_union_congr, restrict_union_le, restrict_union₀, restrict_univ, restrict_zero, restrict_zero_set, restrictₗ_apply, sum_restrict_le, volume_subtype_coe_eq_zero_of_volume_eq_zero, volume_subtype_coe_le_volume, measure_preimage_eq_measure_restrict_preimage_of_ae_compl_eq_const, ae_add_measure_iff, ae_eq_comp, ae_eq_comp', ae_eq_restrict_biUnion_finset_iff, ae_eq_restrict_biUnion_iff, ae_eq_restrict_iUnion_iff, ae_finsetSum_measure_iff, ae_imp_of_ae_restrict, ae_of_ae_restrict_of_ae_restrict_compl, ae_restrict_biUnion_eq, ae_restrict_biUnion_finset_eq, ae_restrict_biUnion_finset_iff, ae_restrict_biUnion_iff, ae_restrict_congr_set, ae_restrict_eq, ae_restrict_eq_bot, ae_restrict_iUnion_eq, ae_restrict_iUnion_iff, ae_restrict_iff, ae_restrict_iff', ae_restrict_iff'₀, ae_restrict_iff₀, ae_restrict_le, ae_restrict_mem, ae_restrict_mem₀, ae_restrict_neBot, ae_restrict_of_ae, ae_restrict_of_ae_eq_of_ae_restrict, ae_restrict_of_ae_restrict_of_subset, ae_restrict_of_forall_mem, ae_restrict_uIoc_eq, ae_restrict_uIoc_iff, ae_restrict_union_eq, ae_restrict_union_iff, div_ae_eq_one, le_ae_restrict, mem_map_restrict_ae_iff, nullMeasurableSet_restrict, nullMeasurableSet_restrict_of_subset, one_le_div_ae, self_mem_ae_restrict, sub_ae_eq_zero, sub_nonneg_ae, ae_eq_restrict_iff_indicator_ae_eq, ae_restrict_iff_subtype, comap_subtype_coe_apply, indicator_ae_eq_of_ae_eq_set, indicator_ae_eq_of_restrict_compl_ae_eq_zero, indicator_ae_eq_restrict, indicator_ae_eq_restrict_compl, indicator_ae_eq_zero_of_restrict_ae_eq_zero, indicator_meas_zero, map_comap_subtype_coe, map_restrict_ae_le_map_indicator_ae, mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem, mem_map_indicator_ae_iff_of_zero_notMem, piecewise_ae_eq_of_ae_eq_set, piecewise_ae_eq_restrict, piecewise_ae_eq_restrict_compl, volume_image_subtype_coe, volume_preimage_coe, volume_set_coe_def	170
Total	173

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrict 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.Measure.restrict	—	MeasureTheory.Measure.instOuterMeasureClass filter_mono MeasureTheory.Measure.ae_le_iff_absolutelyContinuous MeasureTheory.Measure.absolutelyContinuous_restrict

MeasurableEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_map_iff 📖	mathematical	MeasurableEmbedding	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.map	—	MeasureTheory.Measure.instOuterMeasureClass map_apply
comap_apply 📖	mathematical	MeasurableEmbedding	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.comap Set.image	—	Function.Injective.preimage_image injective map_apply map_comap MeasureTheory.Measure.restrict_apply' measurableSet_range Set.inter_eq_self_of_subset_left Set.image_subset_range
comap_map 📖	mathematical	MeasurableEmbedding	MeasureTheory.Measure.comap MeasureTheory.Measure.map	—	MeasureTheory.Measure.ext comap_apply map_apply Set.preimage_image_eq injective
comap_preimage 📖	mathematical	MeasurableEmbedding	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.comap Set.preimage Set.instInter Set.range	—	map_apply map_comap MeasureTheory.Measure.restrict_apply' measurableSet_range
comap_restrict 📖	mathematical	MeasurableEmbedding	MeasureTheory.Measure.comap MeasureTheory.Measure.restrict Set.preimage	—	MeasureTheory.Measure.ext MeasureTheory.Measure.restrict_apply comap_apply measurableSet_image Set.image_inter_preimage
map_comap 📖	mathematical	MeasurableEmbedding	MeasureTheory.Measure.map MeasureTheory.Measure.comap MeasureTheory.Measure.restrict Set.range	—	MeasureTheory.Measure.ext map_apply MeasureTheory.Measure.comap_apply injective measurableSet_image' measurable Set.image_preimage_eq_inter_range MeasureTheory.Measure.restrict_apply
restrict_comap 📖	mathematical	MeasurableEmbedding	MeasureTheory.Measure.restrict MeasureTheory.Measure.comap Set.image	—	comap_restrict Set.preimage_image_eq injective
restrict_map 📖	mathematical	MeasurableEmbedding	MeasureTheory.Measure.restrict MeasureTheory.Measure.map Set.preimage	—	MeasureTheory.Measure.ext MeasureTheory.Measure.restrict_apply map_apply measurable

MeasurableEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_apply 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.comap MeasurableEquiv EquivLike.toFunLike instEquivLike Set.preimage symm	—	MeasurableEmbedding.comap_apply measurableEmbedding image_eq_preimage_symm
restrict_map 📖	mathematical	—	MeasureTheory.Measure.restrict MeasureTheory.Measure.map DFunLike.coe MeasurableEquiv EquivLike.toFunLike instEquivLike Set.preimage	—	MeasurableEmbedding.restrict_map measurableEmbedding

MeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_coe_volume 📖	mathematical	MeasurableSet MeasureTheory.MeasureSpace.toMeasurableSpace	MeasureTheory.Measure.map Set Set.instMembership MeasureTheory.Measure.Subtype.measureSpace MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.restrict	—	volume_set_coe_def MeasurableEmbedding.map_comap MeasurableEmbedding.subtype_coe Subtype.range_coe

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_add_measure_iff 📖	mathematical	—	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.instAdd	—	add_eq_zero Unique.instSubsingleton
ae_eq_comp 📖	—	AEMeasurable Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.map	—	—	Measure.instOuterMeasureClass ae_eq_comp' Measure.AbsolutelyContinuous.rfl
ae_eq_comp' 📖	—	AEMeasurable Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.AbsolutelyContinuous Measure.map	—	—	Measure.instOuterMeasureClass Filter.Tendsto.mono_right Measure.tendsto_ae_map Measure.AbsolutelyContinuous.ae_le
ae_eq_restrict_biUnion_finset_iff 📖	mathematical	—	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict Set.iUnion Finset Finset.instMembership	—	ae_eq_restrict_biUnion_iff Finset.countable_toSet
ae_eq_restrict_biUnion_iff 📖	mathematical	—	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict Set.iUnion Set Set.instMembership	—	Measure.instOuterMeasureClass ae_restrict_biUnion_eq
ae_eq_restrict_iUnion_iff 📖	mathematical	—	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict Set.iUnion	—	Measure.instOuterMeasureClass ae_restrict_iUnion_eq
ae_finsetSum_measure_iff 📖	mathematical	—	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Finset.sum Measure.instAddCommMonoid	—	Finset.cons_induction Measure.instOuterMeasureClass ae_zero instIsEmptyFalse ae.congr_simp Finset.sum_cons
ae_imp_of_ae_restrict 📖	—	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict	—	—	Measure.instOuterMeasureClass Set.inter_comm Measure.measure_inter_eq_zero_of_restrict
ae_of_ae_restrict_of_ae_restrict_compl 📖	—	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict Compl.compl Set Set.instCompl	—	—	Measure.instOuterMeasureClass nonpos_iff_eq_zero ENNReal.instCanonicallyOrderedAdd measure_le_inter_add_diff add_le_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Measure.le_restrict_apply ae_iff zero_add
ae_restrict_biUnion_eq 📖	mathematical	—	ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict Set.iUnion Set Set.instMembership iSup Filter Filter.instSupSet	—	Measure.instOuterMeasureClass Set.biUnion_eq_iUnion ae_restrict_iUnion_eq Set.Countable.to_subtype iSup_subtype''
ae_restrict_biUnion_finset_eq 📖	mathematical	—	ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict Set.iUnion Finset Finset.instMembership iSup Filter Filter.instSupSet	—	ae_restrict_biUnion_eq Finset.countable_toSet
ae_restrict_biUnion_finset_iff 📖	mathematical	—	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict Set.iUnion Finset Finset.instMembership	—	Measure.instOuterMeasureClass ae_restrict_biUnion_finset_eq
ae_restrict_biUnion_iff 📖	mathematical	—	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict Set.iUnion Set Set.instMembership	—	Measure.instOuterMeasureClass ae_restrict_biUnion_eq
ae_restrict_congr_set 📖	mathematical	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass	Filter.Eventually Measure.restrict	—	Measure.instOuterMeasureClass ae_restrict_of_ae_eq_of_ae_restrict Filter.EventuallyEq.symm
ae_restrict_eq 📖	mathematical	MeasurableSet	ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict Filter Filter.instInf Filter.principal	—	Filter.ext Measure.instOuterMeasureClass Measure.restrict_apply_eq_zero'
ae_restrict_eq_bot 📖	mathematical	—	ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict Bot.bot Filter Filter.instBot DFunLike.coe Set ENNReal instZeroENNReal	—	Measure.instOuterMeasureClass ae_eq_bot Measure.restrict_eq_zero
ae_restrict_iUnion_eq 📖	mathematical	—	ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict Set.iUnion iSup Filter Filter.instSupSet	—	le_antisymm Measure.instOuterMeasureClass ae_mono Measure.restrict_iUnion_le Measure.ae_sum_eq iSup_le Measure.restrict_mono Set.subset_iUnion le_rfl
ae_restrict_iUnion_iff 📖	mathematical	—	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict Set.iUnion	—	Measure.instOuterMeasureClass ae_restrict_iUnion_eq
ae_restrict_iff 📖	mathematical	MeasurableSet setOf	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict	—	ae_restrict_iff₀ MeasurableSet.nullMeasurableSet
ae_restrict_iff' 📖	mathematical	MeasurableSet	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict	—	ae_restrict_iff'₀ MeasurableSet.nullMeasurableSet
ae_restrict_iff'₀ 📖	mathematical	NullMeasurableSet	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict	—	Measure.instOuterMeasureClass Measure.restrict_apply₀' Set.ext
ae_restrict_iff₀ 📖	mathematical	NullMeasurableSet setOf Measure.restrict	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Measure.instOuterMeasureClass Measure.restrict_apply₀ NullMeasurableSet.compl Set.ext
ae_restrict_le 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict	—	ae_mono Measure.restrict_le_self
ae_restrict_mem 📖	mathematical	MeasurableSet	Filter.Eventually Set Set.instMembership ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict	—	ae_restrict_mem₀ MeasurableSet.nullMeasurableSet
ae_restrict_mem₀ 📖	mathematical	NullMeasurableSet	Filter.Eventually Set Set.instMembership ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict	—	Measure.instOuterMeasureClass ae_restrict_iff'₀ Filter.Eventually.of_forall
ae_restrict_neBot 📖	mathematical	—	Filter.NeBot ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict	—	Measure.instOuterMeasureClass Filter.neBot_iff Iff.not ae_restrict_eq_bot
ae_restrict_of_ae 📖	mathematical	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass	Measure.restrict	—	Measure.instOuterMeasureClass Filter.Eventually.filter_mono ae_mono Measure.restrict_le_self
ae_restrict_of_ae_eq_of_ae_restrict 📖	—	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Filter.Eventually Measure.restrict	—	—	Measure.instOuterMeasureClass ae.congr_simp Measure.restrict_congr_set
ae_restrict_of_ae_restrict_of_subset 📖	—	Set Set.instHasSubset Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict	—	—	Measure.instOuterMeasureClass Filter.Eventually.filter_mono ae_mono Measure.restrict_mono le_refl
ae_restrict_of_forall_mem 📖	mathematical	MeasurableSet	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict	—	Filter.Eventually.mono Measure.instOuterMeasureClass ae_restrict_mem
ae_restrict_uIoc_eq 📖	mathematical	—	ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict Set.uIoc Filter Filter.instSup Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Measure.instOuterMeasureClass ae.congr_simp Set.uIoc_eq_union ae_restrict_union_eq
ae_restrict_uIoc_iff 📖	mathematical	—	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict Set.uIoc Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Measure.instOuterMeasureClass ae_restrict_uIoc_eq Filter.eventually_sup
ae_restrict_union_eq 📖	mathematical	—	ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict Set Set.instUnion Filter Filter.instSup	—	Measure.instOuterMeasureClass ae.congr_simp Set.union_eq_iUnion ae_restrict_iUnion_eq Bool.countable iSup_bool_eq
ae_restrict_union_iff 📖	mathematical	—	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict Set Set.instUnion	—	Measure.instOuterMeasureClass ae_restrict_union_eq
div_ae_eq_one 📖	mathematical	—	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Pi.instDiv DivInvMonoid.toDiv Group.toDivInvMonoid Pi.instOne InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Measure.instOuterMeasureClass Filter.Eventually.mono div_eq_one Pi.one_apply Pi.div_apply
le_ae_restrict 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.instInf ae Measure Measure.instFunLike Measure.instOuterMeasureClass Filter.principal Measure.restrict	—	Measure.instOuterMeasureClass Filter.eventually_inf_principal ae_imp_of_ae_restrict
mem_map_restrict_ae_iff 📖	mathematical	MeasurableSet	Set Filter Filter.instMembership Filter.map ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict DFunLike.coe ENNReal Set.instInter Compl.compl Set.instCompl Set.preimage instZeroENNReal	—	Measure.instOuterMeasureClass Filter.mem_map mem_ae_iff Measure.restrict_apply'
nullMeasurableSet_restrict 📖	mathematical	NullMeasurableSet	Measure.restrict Set Set.instInter	—	Measure.instOuterMeasureClass NullMeasurableSet.exists_measurable_superset_ae_eq ae_restrict_iff'₀ Filter.mp_mem Filter.univ_mem' ae_eq_set_inter Filter.EventuallyEq.refl NullMeasurableSet.congr MeasurableSet.nullMeasurableSet MeasurableSet.inter Filter.EventuallyEq.trans NullMeasurableSet.of_null Measure.restrict_apply₀' Set.diff_inter_self measure_empty NullMeasurableSet.mono_ac Measure.absolutelyContinuous_restrict Set.diff_union_inter NullMeasurableSet.union
nullMeasurableSet_restrict_of_subset 📖	mathematical	Set Set.instHasSubset	NullMeasurableSet Measure.restrict	—	Measure.instOuterMeasureClass NullMeasurableSet.exists_measurable_subset_ae_eq ae_imp_of_ae_restrict Filter.mp_mem Filter.univ_mem' NullMeasurableSet.congr MeasurableSet.nullMeasurableSet NullMeasurableSet.mono_ac Measure.absolutelyContinuous_restrict
one_le_div_ae 📖	mathematical	—	Filter.EventuallyLE ae Measure Measure.instFunLike Measure.instOuterMeasureClass Pi.instOne InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Pi.instDiv DivInvMonoid.toDiv Group.toDivInvMonoid	—	Measure.instOuterMeasureClass Filter.Eventually.mono one_le_div' Pi.div_apply Pi.one_apply
self_mem_ae_restrict 📖	mathematical	MeasurableSet	Set Filter Filter.instMembership ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict	—	Measure.instOuterMeasureClass ae_restrict_eq Filter.univ_mem Set.Subset.rfl Set.univ_inter
sub_ae_eq_zero 📖	mathematical	—	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	Measure.instOuterMeasureClass Filter.Eventually.mono sub_eq_zero Pi.zero_apply Pi.sub_apply
sub_nonneg_ae 📖	mathematical	—	Filter.EventuallyLE ae Measure Measure.instFunLike Measure.instOuterMeasureClass Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	Measure.instOuterMeasureClass Filter.Eventually.mono sub_nonneg Pi.sub_apply Pi.zero_apply

MeasureTheory.Measure

Definitions

Name	Category	Theorems
restrict 📖	CompOp	981 math, 3 bridge math: MeasureTheory.setIntegral_union, NumberField.mixedEmbedding.integral_comp_polarSpaceCoord_symm, MeasureTheory.setIntegral_tilted, Real.isFiniteMeasure_restrict_Ioc, MeasureTheory.LpToLpRestrictCLM_coeFn, Set.Countable.measure_restrict_compl, ProbabilityTheory.paretoCDFReal_eq_lintegral, restrict_singleton, QuasiMeasurePreserving.restrict, restrict_comm, MeasureTheory.setIntegral_compl₀, MeasureTheory.setIntegral_nonpos_ae, MeasureTheory.ae_withDensity_iff_ae_restrict, NumberField.mixedEmbedding.lintegral_comp_polarCoord_symm, MeasureTheory.withDensity_apply_le, MeasureTheory.Martingale.stoppedValue_ae_eq_restrict_eq, MeasureTheory.restrict_dirac', MeasureTheory.IsFundamentalDomain.absolutelyContinuous_map, tendsto_tsum_div_pow_atTop_integral, restrict_smul, MeasureTheory.SimpleFunc.integral_piecewise_zero, MeasureTheory.setIntegral_condExp, MeasureTheory.aecover_Ioi_of_Ici, Manifold.pathELength_eq_lintegral_mfderiv_Ioo, MeasureTheory.tendsto_setIntegral_of_L1', Filter.EventuallyEq.restrict, MeasureTheory.L2.inner_indicatorConstLp_eq_inner_setIntegral, UnitAddCircle.lintegral_preimage, MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul, MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum'', MeasureTheory.restrict_compl_singleton, MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable_of_sigmaFinite, MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum, HasCompactSupport.integral_Ioi_deriv_eq, MeasureTheory.IsFundamentalDomain.aestronglyMeasurable_on_iff, MeasureTheory.aecover_Ioi_of_Ioi, Complex.integral_comp_pi_polarCoord_symm, MeasureTheory.integral_Ici_eq_integral_Ioi, ProbabilityTheory.Kernel.setIntegral_deterministic', ProbabilityTheory.setLIntegral_preCDF_fst, restrict_mono', MeasureTheory.integral_indicator, MeasureTheory.setIntegral_eq_integral_of_forall_compl_eq_zero, MeasureTheory.MeasurePreserving.setLIntegral_comp_emb, MeasureTheory.setLIntegral_le_iSup_mul, ProbabilityTheory.gammaCDFReal_eq_lintegral, circleIntegral_def_Icc, restrict_sUnion_congr, integral_exp_mul_Iic, restrict_toMeasurable, intervalIntegral.intervalIntegral_eq_integral_uIoc, MeasureTheory.FinStronglyMeasurable.exists_set_sigmaFinite, ContinuousOn.aestronglyMeasurable_of_isCompact, MeasureTheory.Conservative.measureRestrict, MeasureTheory.ae_restrict_mem, MeasureTheory.lintegral_iUnion₀, MeasureTheory.setLIntegral_pos_iff, MeasureTheory.setIntegral_measure_zero, MeasureTheory.smul_le_stoppedValue_hittingBtwn, MeasureTheory.Integrable.tendsto_setIntegral_nhds_zero, MeasureTheory.lintegral_biUnion_finset₀, unitInterval.measurePreserving_coe, MeasureTheory.IsAddFundamentalDomain.aestronglyMeasurable_on_iff, AntitoneOn.memLp_isCompact, MeasureTheory.finStronglyMeasurable_iff_stronglyMeasurable_and_exists_set_sigmaFinite, MeasureTheory.integral_union_eq_left_of_forall, MeasureTheory.IsAddFundamentalDomain.sum_restrict, ProbabilityTheory.Kernel.setIntegral_restrict, MeasureTheory.MeasurePreserving.restrict_preimage, restrict_empty, MeasureTheory.IsAddFundamentalDomain.addQuotientMeasure_eq, Real.rpow_eq_const_mul_integral, MeasureTheory.ae_restrict_biUnion_iff, interval_average_eq_div, ProbabilityTheory.setIntegral_condCDF, lintegral_fderiv_lineMap_eq_edist, exists_eq_interval_average_of_noAtoms, restrict_congr_set, ProbabilityTheory.lintegral_gammaPDF_of_nonpos, ProbabilityTheory.setIntegral_condKernel_univ_left, MeasureTheory.restrict_compl_sigmaFiniteSet, ProbabilityTheory.Kernel.integral_restrict, InnerRegularWRT.restrict, restrict_add, MeasureTheory.exists_setLAverage_le, MeasureTheory.lintegral_biUnion_finset, ProbabilityTheory.cdf_paretoMeasure_eq_integral, ProbabilityTheory.Kernel.restrict_const, ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat_rat, MeasureTheory.average_mem_openSegment_compl_self, MeasureTheory.setIntegral_prod_swap, LocallyBoundedVariationOn.ae_differentiableWithinAt, restrict_sInf_eq_sInf_restrict, MeasureTheory.setLIntegral_trim, MeasureTheory.eLpNorm_top_piecewise, ProbabilityTheory.tilted_mul_apply_cgf, restrict_singleton', MeasureTheory.setLIntegral_eq_const, MeasureTheory.integral_union_ae, ProbabilityTheory.IsRatCondKernelCDF.setIntegral, restrict_apply_self, MeasureTheory.ae_restrict_biUnion_eq, ProbabilityTheory.setLIntegral_condKernel_univ_right, MeasureTheory.lintegral_abs_det_fderiv_eq_addHaar_image, MeasureTheory.IsFundamentalDomain.quotientMeasure_eq, MeasureTheory.lintegral_biUnion, abs_setIntegral_mulExpNegMulSq_comp_sub_le_mul_measure, rnDeriv_restrict, MeasureTheory.aecover_Iio_of_Iic, integral_exp_neg_mul_rpow, MeasureTheory.lintegral_singleton, ext_iff_of_sUnion_eq_univ, MeasureTheory.lintegral_countable, ProbabilityTheory.setIntegral_condKernel_univ_right, restrict_add_restrict_compl, intervalIntegral.continuousOn_primitive, Real.aestronglyMeasurable_rpowIntegrand₀₁, MeasureTheory.setIntegral_dirac, MeasurableSet.map_coe_volume, integral_Ioi_rpow_of_lt, MeasureTheory.intervalIntegral_tendsto_integral_Iic, tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_integrableOn, ProbabilityTheory.gammaCDFReal_eq_integral, MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul, MeasureTheory.withDensity_indicator, MeasureTheory.HasFiniteIntegral.tendsto_setIntegral_nhds_zero, setIntegral_Ioi_zero_rpow, MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg, integral_rpow_mul_exp_neg_rpow, MeasureTheory.lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn, MeasureTheory.setIntegral_prod_mul, MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonpos', setIntegral_condKernel, MeasureTheory.aecover_Ioo_of_Ioc, setLIntegral_rnDeriv, Complex.hasDerivAt_GammaIntegral, ApproximatesLinearOn.norm_fderiv_sub_le, MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae', MeasureTheory.setIntegral_compl, MeasureTheory.integral_Ioi_deriv_mul_eq_sub, MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto', MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq, MeasureTheory.setIntegral_mono_on_ae₀, IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div, MeasureTheory.aecover_Ioc_of_Ioo, ProbabilityTheory.Kernel.restrict_apply, MeasureTheory.setIntegral_trim, setIntegral_condKernel_univ_left, MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addProjection_respects_measure', MeasureTheory.restrict_Ico_eq_restrict_Ioc, curveIntegralFun_trans_aeeq_right, Complex.integral_comp_polarCoord_symm, MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le, MeasureTheory.setIntegral_congr_ae, Manifold.pathELength_def, restrict_mono, MeasureTheory.integral_Ioi_mul_deriv_eq_deriv_mul, MeasureTheory.integral_biUnion_finset, MeasureTheory.exists_isSigmaFiniteSet_measure_ge, restrict_sum_of_countable, integral_exp_mul_complex_Ioi, setIntegral_Ioi_zero_cpow, restrict_eq_zero, MeasureTheory.MeasurePreserving.setIntegral_image_emb, MeasureTheory.measure_sigmaFiniteSetGE_le, MeasureTheory.integral_condExpL2_eq, ContinuousOn.aestronglyMeasurable_of_subset_isCompact, MeasureTheory.setIntegral_support, MeasureTheory.IsAddFundamentalDomain.restrict_restrict, restrict_apply_superset, MeasureTheory.SimpleFunc.const_lintegral_restrict, MeasureTheory.setLAverage_congr_fun_ae, ProbabilityTheory.Kernel.setIntegral_densityProcess_of_mem, MeasureTheory.sigmaFinite_restrict_sigmaFiniteSetGE, MeasureTheory.MeasurePreserving.setIntegral_preimage_emb, MeasureTheory.setLIntegral_lt_top_of_le_nnreal, MeasureTheory.setIntegral_condExpL2_indicator, intervalIntegral.abs_intervalIntegral_eq, restrict_map, ContinuousLinearMap.setIntegral_compLp, MeasureTheory.addMeasure_map_restrict_apply, MeasureTheory.lintegral_union, Manifold.pathELength_eq_lintegral_mfderivWithin_Icc, MeasureTheory.eLpNorm_restrict_eq_of_support_subset, MeasureTheory.integral_singleton', VitaliFamily.ae_tendsto_lintegral_div, ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_mgf', restrict_toMeasurable_of_cover, MeasureTheory.IsAddFundamentalDomain.measurePreserving_add_quotient_mk, aemeasurable_restrict_iff_comap_subtype, finite_integral_rpow_sub_one_pow_aux, Complex.GammaIntegral_ofReal, singularPart_restrict, MeasureTheory.restrict_dirac, lintegral_comp_pi_polarCoord_symm, MeasureTheory.integral_integral_indicator, restrict_apply, MeasureTheory.aecover_Icc_of_Ioc, MeasureTheory.AECover.integral_tendsto_of_countably_generated, MeasureTheory.IntegrableOn.restrict_toMeasurable, MeasureTheory.setIntegral_condExpInd, ProbabilityTheory.lintegral_exponentialPDF_eq_antiDeriv, MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux1, MeasureTheory.integral_comp_rpow_Ioi_of_pos, MeasureTheory.Submartingale.setIntegral_le, MeasureTheory.lintegral_iUnion_le, MeasureTheory.IsFundamentalDomain.setLIntegral_eq, MonotoneOn.memLp_of_measure_ne_top, MeasureTheory.aecover_Ioc_of_Icc, map_restrict_ae_le_map_indicator_ae, MeasureTheory.setLIntegral_nnnorm_condExpL2_indicator_le, MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum_of_ac, MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum', MeasureTheory.setIntegral_le_integral, MeasureTheory.ae_withDensity_iff_ae_restrict', MeasureTheory.AEContinuous.hasBoxIntegral, restrict_biUnion_le, ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_mgf, ProbabilityTheory.Kernel.setIntegral_const, sum_mul_eq_sub_integral_mul', ProbabilityTheory.Kernel.setIntegral_densityProcess_of_le, MeasureTheory.ae_restrict_iUnion_eq, MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum', MeasureTheory.lintegral_rpow_eq_lintegral_meas_le_mul, singularPart_eq_restrict, restrict_inter_add_diff₀, MeasureTheory.ae_restrict_mem₀, aestronglyMeasurable_indicator_iff₀, setIntegral_compProd, MeasureTheory.integral_fintype_iUnion, MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum, MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image, ProbabilityTheory.setLIntegral_condKernel, MeasureTheory.Integrable.restrict, MeasureTheory.IsFundamentalDomain.sum_restrict, MeasureTheory.MeasurePreserving.setLIntegral_comp_preimage, MeasureTheory.ae_restrict_eq_bot, LSeries_eq_mul_integral_of_nonneg, MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul, MeasureTheory.lintegral_nnnorm_condExpL2_le, MeasureTheory.MeasurePreserving.restrict_image_emb, MeasurableEquiv.restrict_map, ProbabilityTheory.IsCondKernelCDF.setIntegral, IntervalIntegrable.aestronglyMeasurable', MeasurableEmbedding.restrict_map, setIntegral_condKernel_univ_right, MeasureTheory.norm_integral_sub_setIntegral_le, MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv_aux1, restrict_iUnion, MeasureTheory.setLIntegral_compl, MeasureTheory.QuotientMeasureEqMeasurePreimage.projection_respects_measure', MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq, MeasureTheory.setLIntegral_withDensity_eq_lintegral_mul₀, MeasureTheory.SimpleFunc.lintegral_restrict, MeasureTheory.lintegral_inter_add_diff, integral_exp_Iic, integral_mul_cexp_neg_mul_sq, intervalIntegral.continuousOn_primitive_Icc, MeasureTheory.integral_inter_add_diff, MeasureTheory.ae_restrict_of_forall_mem, MeasureTheory.aemeasurable_ofReal_abs_det_fderivWithin, AntitoneOn.memLp_top, MeasureTheory.integral_Iic_eq_integral_Iio', InnerRegularCompactLTTop.restrict, Regular.restrict_of_measure_ne_top, ProbabilityTheory.Kernel.setIntegral_deterministic, restrict_union, MeasureTheory.integral_Icc_eq_integral_Ioo, intervalIntegral.integral_cases, MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable, MeasureTheory.restrict_Iio_eq_restrict_Iic, ProbabilityTheory.Kernel.setLIntegral_restrict, restrict_union', MeasureTheory.setIntegral_map_equiv, restrict_mono_set, ProbabilityTheory.lintegral_exponentialPDF_of_nonpos, MeasureTheory.isFiniteMeasureRestrict, ContinuousMap.aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry, MeasureTheory.setIntegral_condExpIndSMul, MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivAt_of_le, MeasureTheory.setIntegral_mono_on₀, MeasureTheory.lintegral_rpow_eq_lintegral_meas_lt_mul, ProbabilityTheory.IsCondKernelCDF.setLIntegral, MeasureTheory.setIntegral_map, MeasureTheory.integral_diff, restrict_toOuterMeasure_eq_toOuterMeasure_restrict, MeasureTheory.setLIntegral_congr_fun, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable_of_equiv, MeasureTheory.setIntegral_rnDeriv_smul, MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul, ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_cgf', MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_eq_zero_aux, MeasureTheory.measureReal_restrict_apply', MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul', MeasureTheory.exists_measurable_le_forall_setLIntegral_eq, integral_rpow_mul_exp_neg_mul_rpow, restrict_restrict', MeasureTheory.measure_le_setAverage_pos, MeasureTheory.integral_image_eq_integral_abs_deriv_smul, absolutelyContinuous_restrict, integral_comp_polarCoord_symm, restrict_apply_eq_zero, VitaliFamily.ae_tendsto_average_norm_sub, MeasureTheory.tendsto_setIntegral_of_antitone, MeasureTheory.IsAddFundamentalDomain.setIntegral_eq_tsum, restrict_pi_pi, MeasureTheory.Martingale.condExp_stoppedValue_stopping_time_ae_eq_restrict_le, MeasureTheory.lintegral_subtype_comap, restrict.neZero, restrict_mono_measure, interval_average_symm, MeasureTheory.IsFundamentalDomain.restrict_restrict, MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum, MeasureTheory.setLIntegral_congr_fun_ae, interior_inter_support, MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum'', MeasureTheory.setIntegral_tsupport, volume_regionBetween_eq_lintegral', MeasureTheory.L2.inner_indicatorConstLp_one, MeasureTheory.restrict_Ioo_eq_restrict_Icc, restrict_iUnion_apply, ProbabilityTheory.setIntegral_tilted_mul_eq_mgf', restrict_apply_le, MeasureTheory.aemeasurable_fderivWithin, restrict_union_add_inter, piecewise_ae_eq_restrict_compl, MeasureTheory.restrict_withDensity, MeasureTheory.setLIntegral_eq_zero_iff, ENNReal.essSup_piecewise, ProbabilityTheory.lintegral_paretoPDF_of_le, MeasureTheory.setLAverage_eq', restrict_restrict₀', MeasureTheory.lintegral_deriv_eq_volume_image_of_antitoneOn, restrict_apply_univ, MeasureTheory.IntegrableOn.setLIntegral_lt_top, Real.integral_rpowIntegrand₀₁_one_pos, MeasureTheory.integral_Icc_eq_integral_Ioo', MutuallySingular.restrict_nullSet, HasCompactSupport.integral_Iic_deriv_eq, MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul, ProbabilityTheory.tilted_mul_apply_mgf', MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv_aux2, ProbabilityTheory.Kernel.setLIntegral_deterministic, MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq_tsum', integral_comp_abs, ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat, ContinuousOn.aestronglyMeasurable, enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc, MeasureTheory.integral_target_eq_integral_abs_det_fderiv_smul, setLIntegral_rnDeriv', ProbabilityTheory.cdf_gammaMeasure_eq_lintegral, MeasureTheory.setIntegral_congr_ae₀, restrict_restrict, MeasureTheory.ae_restrict_neBot, restrict_congr_meas, MeasureTheory.integral_Ioc_eq_integral_Ioo', MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum', MeasureTheory.IsAddFundamentalDomain.essSup_measure_restrict, MeasureTheory.ae_eq_restrict_biUnion_finset_iff, MeasureTheory.restrict_compl_sigmaFiniteSet_eq_zero_or_top, ProbabilityTheory.gaussianReal_apply, prod_restrict, MeasureTheory.eLpNormEssSup_piecewise, restrict_inter_toMeasurable, MeasureTheory.tilted_apply_eq_ofReal_integral, MeasureTheory.AEStronglyMeasurable.restrict, ProbabilityTheory.setLIntegral_condKernel_univ_left, ProbabilityTheory.condExp_set_generateFrom_singleton, MeasureTheory.integral_add_compl, MeasureTheory.lintegral_eq_lintegral_meas_le, MeasureTheory.setLAverage_congr, Topology.IsClosedEmbedding.setIntegral_map, MeasureTheory.lintegral_add_compl, setIntegral_toReal_rnDeriv', MeasureTheory.setIntegral_indicator, ProbabilityTheory.Kernel.setLIntegral_compProd_univ_left, MeasureTheory.lintegral_indicator_le, ProbabilityTheory.condExp_generateFrom_singleton, ProbabilityTheory.Kernel.setIntegral_density_of_measurableSet, MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum, Measurable.setLIntegral_kernel_prod_left, MeasureTheory.Lp_toLp_restrict_add, MeasureTheory.ae_eq_restrict_biUnion_iff, MeasureTheory.setAverage_eq', MeasureTheory.setIntegral_condExpL1, MeasureTheory.measure_sigmaFiniteSetWRT', HasCompactSupport.enorm_le_lintegral_Ici_deriv, MeasureTheory.intervalIntegral_tendsto_integral_Ioi, MeasureTheory.integral_posConvolution, sum_mul_eq_sub_integral_mul₀', MeasureTheory.setIntegral_mono_on_ae, continuous_parametric_integral_of_continuous, intervalIntegral.norm_intervalIntegral_eq, MeasureTheory.setAverage_congr, AEMeasurable.restrict, ProbabilityTheory.Fernique.lintegral_closedBall_diff_exp_logRatio_mul_sq_le, MeasureTheory.ae_restrict_union_iff, MeasureTheory.mem_map_restrict_ae_iff, MeasureTheory.Restrict.isFiniteMeasure, MeasureTheory.integral_Icc_eq_integral_Ico', ProbabilityTheory.setIntegral_compProd_univ_right, Measurable.setLIntegral_kernel, restrict_sum, MeasureTheory.integral_Ioc_eq_integral_Ioo, MeasureTheory.tilted_apply, intervalAverage_congr_codiscreteWithin, aestronglyMeasurable_iUnion_iff, MeasureTheory.setAverage_eq, MeasureTheory.smul_le_stoppedValue_hitting, MeasureTheory.isFiniteMeasure_restrict, MeasureTheory.integral_Ico_eq_integral_Ioo, MeasureTheory.IsFundamentalDomain.integral_eq_tsum'', MeasureTheory.norm_setIntegral_le_of_norm_le_const, MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable', ProbabilityTheory.setLIntegral_toKernel_univ, MeasureTheory.integral_condExpL2_eq_of_fin_meas_real, ProbabilityTheory.condExpKernel_singleton_ae_eq_cond, intervalIntegral.integral_Iio_add_Ici, ContinuousWithinAt.integral_sub_linear_isLittleO_ae, MeasureTheory.Martingale.setIntegral_eq, MeasureTheory.setAverage_sub_setAverage, Real.isFiniteMeasure_restrict_Ioo, MeasureTheory.aecover_Icc_of_Icc, MeasureTheory.setIntegral_empty, restrict_map_of_aemeasurable, MeasureTheory.ae_restrict_of_ae, restrict.instNoAtoms, MeasureTheory.IsAddFundamentalDomain.hasFiniteIntegral_on_iff, MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul, MeasureTheory.setLIntegral_mono, MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum', ProbabilityTheory.Kernel.setIntegral_densityProcess, MeasureTheory.integral_biUnion_eq_sum_powerset, ae_restrict_iff_subtype, MeasureTheory.instSigmaFiniteRestrictSigmaFiniteSetWRT, AbsolutelyContinuousOnInterval.tendsto_volume_restrict_totalLengthFilter_disjWithin_nhds_zero, MeasureTheory.setIntegral_abs_condExp_le, intervalIntegral.integral_of_ge, setLIntegral_condKernel, MeasureTheory.setIntegral_neg_eq_setIntegral_nonpos, aemeasurable_restrict_of_measurable_subtype, MeasureTheory.locallyIntegrableOn_iff_locallyIntegrable_restrict, ProbabilityTheory.setIntegral_tilted_mul_eq_cgf', MeasureTheory.restrict_Ioi_eq_restrict_Ici, MeasureTheory.Integrable.integral_eq_integral_meas_le, MeasurableEmbedding.gaussianReal_comap_apply, IntervalIntegrable.aestronglyMeasurable, MeasureTheory.AECover.inter_restrict, VitaliFamily.ae_tendsto_measure_inter_div, MeasureTheory.setLIntegral_rnDeriv_mul, MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le, MeasureTheory.setIntegral_condExpL1CLM_of_measure_ne_top, MeasureTheory.integral_comp_rpow_Ioi, MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum, Complex.lintegral_comp_polarCoord_symm, restrict_union₀, integral_exp_neg_rpow, Antitone.tendsto_setIntegral, MeasureTheory.map_eq_setLIntegral_pdf, MeasureTheory.Integrable.integral_eq_integral_meas_lt, MeasureTheory.IsHahnDecomposition.ge_on_compl, MeasureTheory.integral_fun_norm_addHaar, tendsto_sum_mul_atTop_nhds_one_sub_integral₀, MeasureTheory.ae_restrict_le, MeasureTheory.setIntegral_ge_of_const_le, MeasureTheory.measure_map_restrict_apply, StronglyMeasurableAtFilter.eventually, restrict_iUnion_apply_eq_iSup, MeasureTheory.restrict_Ico_eq_restrict_Icc, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le_real, MeasureTheory.lintegral_union_le, ProbabilityTheory.Kernel.setLIntegral_density, ProbabilityTheory.exponentialCDFReal_eq_integral, sum_mul_eq_sub_integral_mul₁, MeasureTheory.setLIntegral_lt_top_of_bddAbove, MeasureTheory.integral_Icc_eq_integral_Ico, MeasureTheory.average_union_mem_segment, ProbabilityTheory.cdf_expMeasure_eq_integral, MeasureTheory.setLIntegral_one, MeasureTheory.withDensity_apply₀, Besicovitch.ae_tendsto_measure_inter_div, Real.isFiniteMeasure_restrict_Icc, MeasureTheory.integral_Iic_eq_integral_Iio, intervalIntegral.integral_of_le, InnerRegularWRT.restrict_of_measure_ne_top, MeasureTheory.exists_pos_setLIntegral_lt_of_measure_lt, MeasureTheory.setLIntegral_const_lt_top, MeasureTheory.ae_restrict_biUnion_finset_iff, restrict_zero, MeasureTheory.setIntegral_nonpos, LSeries_eq_mul_integral, ProbabilityTheory.Kernel.setLIntegral_deterministic', ProbabilityTheory.paretoCDFReal_eq_integral, AntitoneOn.memLp_of_measure_ne_top, MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq_of_countable, MeasureTheory.setLAverage_one, MeasureTheory.Supermartingale.setIntegral_le, VitaliFamily.ae_tendsto_lintegral_div', MeasureTheory.lintegral_indicator, MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul, MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum'', aemeasurable_uIoc_iff, MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq_of_countable_range, MeasureTheory.setIntegral_congr_fun, MeasureTheory.setIntegral_rnDeriv_smul', MeasureTheory.restrict_Ioo_eq_restrict_Ioc, MeasureTheory.tendsto_measure_sigmaFiniteSetGE, MeasureTheory.setLIntegral_mono_ae', enorm_sub_le_lintegral_deriv_of_contDiffOn_Icc, MeasureTheory.Martingale.condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const, MeasureTheory.setLAverage_eq, MeasureTheory.integral_add_compl₀, MeasureTheory.lintegral_image_eq_lintegral_deriv_mul_of_antitoneOn, MeasureTheory.L2.inner_indicatorConstLp_eq_setIntegral_inner, MeasureTheory.lintegral_finset, MeasureTheory.memLp_indicator_iff_restrict, ProbabilityTheory.setIntegral_preCDF_fst, intervalIntegral.integral_Iic_sub_Iic, MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_le_const, Real.isFiniteMeasure_restrict_Ico, MeasureTheory.setLIntegral_tilted, MeasureTheory.ae_restrict_biUnion_finset_eq, MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum_of_ac, MeasureTheory.setLIntegral_map, MeasurableEmbedding.comap_restrict, MeasureTheory.setLIntegral_dirac', NumberField.mixedEmbedding.fundamentalCone.setLIntegral_paramSet_exp, restrict_restrict_of_subset, MeasureTheory.withDensityᵥ_apply, MeasureTheory.lintegral_singleton', MeasureTheory.ContinuousOn.hasBoxIntegral, restrict_biUnion_finset, integral_exp_neg_Ioi, MeasureTheory.ae_restrict_eq, UnitAddCircle.measurePreserving_mk, MeasureTheory.setLIntegral_strict_mono, MeasureTheory.setLIntegral_empty, AbsolutelyContinuous.restrict, MeasureTheory.tendsto_setIntegral_of_L1, integral_comp_neg_Iic, MeasureTheory.ofReal_setIntegral_one, aemeasurable_iUnion_iff, MeasureTheory.FiniteMeasure.restrict_measure_eq, ae_restrict_le_codiscreteWithin, restrict_mono_ae, tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos, singularPart_eq_restrict', MeasureTheory.setIntegral_indicatorConstLp, Real.Gamma_eq_integral, ContinuousMap.aeStronglyMeasurable_restrict_mkD_of_uncurry, MeasureTheory.lintegral_eq_lintegral_meas_lt, MeasureTheory.SimpleFunc.lintegral_restrict_iUnion_of_directed, MeasureTheory.IsFundamentalDomain.essSup_measure_restrict, MeasureTheory.integral_indicator₀, compProd_apply_prod, MeasureTheory.laverage_union_mem_segment, MeasureTheory.setLIntegral_const, MeasureTheory.instSigmaFiniteRestrictInterSet, setIntegral_withDensity_eq_setIntegral_smul, MeasureTheory.setIntegral_dirac', MeasureTheory.Restrict.sigmaFinite, ProbabilityTheory.setIntegral_condKernel, indicator_ae_eq_restrict_compl, aemeasurable_restrict_of_monotoneOn, MeasureTheory.setIntegral_nonpos_le, restrict_union_add_inter₀, MeasureTheory.measurePreserving_subtype_coe, MeasureTheory.ae_restrict_uIoc_iff, MeasureTheory.setLIntegral_dirac, ProbabilityTheory.Kernel.IsProper.setLIntegral_eq_indicator_mul_lintegral, MeasureTheory.nullMeasurableSet_restrict, ProbabilityTheory.Kernel.tendsto_setIntegral_densityProcess, LipschitzOnWith.ae_differentiableWithinAt_real, ProbabilityTheory.setLIntegral_toKernel_prod, ProbabilityTheory.setIntegral_compProd, MeasureTheory.integral_Ico_eq_integral_Ioo', setIntegral_toReal_rnDeriv_eq_withDensity', MeasureTheory.setLIntegral_subtype, restrict_iUnion_ae, MeasureTheory.laverage_union, ProbabilityTheory.Kernel.setLIntegral_compProd, Real.le_integral_rpowIntegrand₀₁_one, ProbabilityTheory.Kernel.IsProper.setLIntegral_eq_comp, MeasureTheory.Integrable.withDensityᵥ_trim_eq_integral, restrict_finset_biUnion_congr, MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_compl, aemeasurable_union_iff, MeasureTheory.integral_subtype_comap, restrict_le_self, MeasureTheory.instSigmaFiniteRestrictUnionSet, MeasureTheory.aecover_Ioo_of_Ioo, MeasureTheory.AEFinStronglyMeasurable.sigmaFinite_restrict, NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral, MeasureTheory.aecover_Ioc_of_Ioc, MeasureTheory.lintegral_max, MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq_tsum, MeasureTheory.setIntegral_gt_gt, MeasureTheory.setIntegral_nonneg_ae, MeasureTheory.setIntegral_nonpos_of_ae, MeasureTheory.setIntegral_eq_integral_of_ae_compl_eq_zero, MeasureTheory.HasFiniteIntegral.restrict, mem_support_restrict, restrict_biUnion_finset_congr, MeasureTheory.integral_image_eq_integral_deriv_smul_of_antitone, MeasureTheory.UnifIntegrable.restrict, MeasureTheory.SimpleFunc.restrict_lintegral_eq_lintegral_restrict, ProbabilityTheory.tilted_mul_apply_mgf, MeasureTheory.setLIntegral_max, MeasureTheory.setLIntegral_withDensity_eq_lintegral_mul₀', MeasureTheory.IsAddFundamentalDomain.sum_restrict_of_ac, MeasureTheory.setLIntegral_pdf_le_map, MeasureTheory.AECover.lintegral_tendsto_of_countably_generated, restrict_biUnion, MeasureTheory.setLIntegral_eq_of_support_subset, MeasureTheory.lintegral_iUnion, MeasureTheory.setIntegral_nonneg, MeasureTheory.setIntegral_tilted', ContinuousOn.integral_sub_linear_isLittleO_ae, integral_exp_mul_Ioi, MeasurableEmbedding.restrict_comap, MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv, CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁, MeasureTheory.restrict_Ioo_eq_restrict_Ico, MeasureTheory.setIntegral_ge_of_const_le_real, MeasureTheory.IsFundamentalDomain.integral_eq_tsum_of_ac, iSup_restrict_spanningSets, restrict_eq_self_of_ae_mem, MeasureTheory.hasSum_integral_iUnion, setIntegral_comp_smul, MeasureTheory.lintegral_indicator₀, MeasureTheory.setIntegral_eq_of_subset_of_forall_diff_eq_zero, MeasureTheory.setLIntegral_nnnorm_condExpIndSMul_le, setLIntegral_condKernel_univ_left, MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto, MeasureTheory.restrict_map_withDensity_abs_det_fderiv_eq_addHaar, ProbabilityTheory.setIntegral_condVar, ext_iff_of_iUnion_eq_univ, MeasureTheory.setAverage_congr_fun, MeasureTheory.exists_le_setAverage, MeasureTheory.laverage_mem_openSegment_compl_self, MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum_of_ac, MeasureTheory.ae_restrict_congr_set, restrict_zero_set, MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_le, NumberField.mixedEmbedding.lintegral_comp_polarCoordReal_symm, MeasureTheory.lintegral_mono_set', MeasureTheory.IsFundamentalDomain.sum_restrict_of_ac, restrict_biUnion_congr, MeasureTheory.integral_Icc_eq_integral_Ioc', MeasureTheory.setIntegral_one_eq_measureReal, MeasureTheory.IsFundamentalDomain.hasFiniteIntegral_on_iff, MeasureTheory.aecover_restrict_of_ae_imp, MeasureTheory.integral_inter_add_diff₀, MeasureTheory.eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict, MeasureTheory.aecover_Ico_of_Ioo, ContinuousOn.aemeasurable, MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonpos, ProbabilityTheory.Kernel.setLIntegral_compProd_univ_right, exists_eq_interval_average_of_measure, MeasureTheory.integral_comp_mul_right_Ioi, MeasureTheory.condExp_restrict_ae_eq_restrict, AddCircle.lintegral_preimage, MeasureTheory.BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt, Manifold.pathELength_eq_lintegral_mfderiv_Icc, ProbabilityTheory.Kernel.setLIntegral_rnDeriv, ProbabilityTheory.lintegral_betaPDF, MeasureTheory.integral_subtype, restrict_iUnion_apply_ae, Real.circleAverage_eq_intervalAverage, MeasureTheory.integral_countable, MeasureTheory.exists_setAverage_le, ENNReal.essSup_indicator_eq_essSup_restrict, MeasureTheory.AECover.restrict, MeasureTheory.lintegral_image_eq_lintegral_abs_deriv_mul, AddCircle.measurePreserving_mk, MeasureTheory.hasSum_integral_iUnion_ae, MeasureTheory.ofReal_setIntegral_one_of_measure_ne_top, MeasureTheory.MemLp.restrict, MeasureTheory.ae_restrict_iff, MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_addQuotientMeasure, lintegral_comp_polarCoord_symm, ProbabilityTheory.setIntegral_tilted_mul_eq_mgf, integral_comp_neg_Ioi, Isometry.map_hausdorffMeasure, ProbabilityTheory.setLIntegral_condKernel_eq_measure_prod, ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_cgf, MeasureTheory.lintegral_insert, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable, MeasureTheory.lintegral_mono_set, MeasureTheory.aemeasurable_toNNReal_abs_det_fderivWithin, MeasureTheory.maximal_ineq, ProbabilityTheory.Kernel.IsProper.setLIntegral_inter_eq_indicator_mul_setLIntegral, Filter.Tendsto.integral_sub_linear_isLittleO_ae, ProbabilityTheory.cdf_expMeasure_eq_lintegral, intervalIntegral.abs_integral_eq_abs_integral_uIoc, MeasureTheory.exists_setLIntegral_compl_lt, ENNReal.essSup_restrict_eq_of_support_subset, MeasureTheory.ae_restrict_iff', MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul', WeaklyRegular.restrict_of_measure_ne_top, restrict_apply_eq_zero', ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral_iInf_rat_gt, setLIntegral_compProd, curveIntegralFun_trans_aeeq_left, piecewise_ae_eq_restrict, ProbabilityTheory.setIntegral_tilted_mul_eq_cgf, MeasureTheory.pdf.IsUniform.integral_eq, intervalIntegral.integral_interval_add_Ioi', MeasureTheory.aecover_Ioc_of_Ico, rnDeriv_restrict_self, ProbabilityTheory.Kernel.setIntegral_piecewise, MeasureTheory.setIntegral_setAverage_sub, MeasureTheory.norm_Lp_toLp_restrict_le, restrict_sub_eq_restrict_sub_restrict, MeasureTheory.le_ae_restrict, MeasureTheory.integral_union_eq_left_of_forall₀, MeasureTheory.setLAverage_const, MeasureTheory.setAverage_const, MeasureTheory.tendsto_setIntegral_of_monotone, MeasureTheory.restrict_trim, MeasureTheory.IntegrableOn.integrable, MeasureTheory.nullMeasurableSet_restrict_of_subset, MeasureTheory.lintegral_abs_det_fderiv_eq_addHaar_image₀, MeasureTheory.setIntegral_mono, ProbabilityTheory.setIntegral_compProd_univ_left, ProbabilityTheory.Kernel.setIntegral_traj_partialTraj, MeasureTheory.aecover_Ioo_of_Ico, MeasureTheory.setLIntegral_trim_ae, Asymptotics.IsBigO.set_integral_isBigO, MeasureTheory.aecover_Iio_of_Iio, measurePreserving_quotientAddGroup_mk_of_AddQuotientMeasureEqMeasurePreimage, MeasureTheory.Martingale.condExp_stopping_time_ae_eq_restrict_eq_const, MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_eq_zero, Real.integral_rpow_mul_exp_neg_mul_Ioi, MeasureTheory.setLIntegral_smul_measure, MeasureTheory.setIntegral_congr_set, MeasureTheory.aecover_Icc_of_Ioo, MutuallySingular.restrict_compl_nullSet, intervalIntegral.norm_integral_eq_norm_integral_uIoc, integral_Ioi_cpow_of_lt, ProbabilityTheory.Kernel.setIntegral_density, MeasureTheory.setIntegral_eq_zero_of_forall_eq_zero, tendsto_sum_mul_atTop_nhds_one_sub_integral, MeasureTheory.integral_Iic_of_hasDerivAt_of_tendsto, MeasureTheory.IsFundamentalDomain.setIntegral_eq, MonotoneOn.memLp_isCompact, ProbabilityTheory.Kernel.integral_integral_indicator, aemeasurable_indicator_iff, MeasurableEmbedding.setIntegral_map, MeasureTheory.restrict_compl_sigmaFiniteSetWRT, MeasureTheory.aecover_Ico_of_Ioc, Complex.lintegral_comp_pi_polarCoord_symm, NumberField.mixedEmbedding.fundamentalCone.setLIntegral_expMapBasis_image, volume_regionBetween_eq_integral, mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem, ProbabilityTheory.setLIntegral_condCDF, restrictₗ_apply, MeasureTheory.measure_setAverage_le_pos, MeasureTheory.withDensity_apply', MeasureTheory.integral_singleton, MeasureTheory.integral_iUnion, MeasureTheory.integral_comp_smul_deriv_Ioi, setIntegral_toReal_rnDeriv_le, MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le_of_hasFiniteIntegral, MeasureTheory.setLIntegral_tilted', MeasureTheory.integral_Iic_of_hasDerivAt_of_tendsto', MeasureTheory.IsAddFundamentalDomain.setIntegral_eq, integral_exp_mul_complex_Iic, ProbabilityTheory.Kernel.setLIntegral_piecewise, MeasurableEmbedding.map_comap, MeasureTheory.measureReal_restrict_apply_univ, integrable_mulExpNegMulSq_comp_restrict_of_isCompact, MonotoneOn.memLp_top, MeasureTheory.ae_restrict_iff'₀, MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux2, MeasureTheory.integral_piecewise, MeasureTheory.MeasurePreserving.setLIntegral_comp_preimage_emb, sum_mul_eq_sub_sub_integral_mul', integral_Ioi_inv_one_add_sq, restrict_union_add_inter', MeasureTheory.sigmaFinite_restrict_sigmaFiniteSetWRT', MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum', MeasureTheory.integral_comp_mul_left_Ioi, setLIntegral_condKernel_univ_right, ProbabilityTheory.setLIntegral_condDistrib_of_measurableSet, MeasureTheory.instSigmaFiniteRestrictSigmaFiniteSet, MeasureTheory.IsFundamentalDomain.projection_respects_measure, aestronglyMeasurable_union_iff, integral_exp_neg_Ioi_zero, MeasureTheory.measure_smul_setAverage, MeasureTheory.setLIntegral_setLAverage, IntervalIntegrable.aestronglyMeasurable_restrict_uIoc, MeasureTheory.setLIntegral_eq_zero, MeasureTheory.laverage_union_mem_openSegment, sum_mul_eq_sub_integral_mul, exists_eq_const_mul_setIntegral_of_nonneg, MeasurableEquiv.gaussianReal_map_symm_apply, MeasureTheory.setIntegral_condExpL1CLM, setIntegral_toReal_rnDeriv_eq_withDensity, setIntegral_comp_smul_of_pos, map_comap_subtype_coe, ProbabilityTheory.Kernel.withDensity_apply', integral_gaussian_Ioi, setIntegral_re_add_im, intervalIntegral.integral_Iic_add_Ioi, MeasureTheory.exists_eq_setAverage, MeasureTheory.instSigmaFiniteRestrictInterSet_1, MeasureTheory.integral_finset, ProbabilityTheory.setLIntegral_preimage_condDistrib, ProbabilityTheory.Kernel.tendsto_eLpNorm_one_restrict_densityProcess_limitProcess, ContinuousAt.integral_sub_linear_isLittleO_ae, MeasureTheory.integral_Ici_eq_integral_Ioi', intervalIntegral.integral_interval_add_Ioi, toSignedMeasure_restrict_eq_restrict_toSignedMeasure, MeasureTheory.measure_setLAverage_le_pos, MeasureTheory.setIntegral_nonneg_of_ae, MeasureTheory.setLAverage_congr_fun, ae_eq_restrict_iff_indicator_ae_eq, measurePreserving_quotientGroup_mk_of_QuotientMeasureEqMeasurePreimage, MutuallySingular.restrict, abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt, MeasureTheory.exists_measurable_le_setLIntegral_eq_of_integrable, MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_quotientMeasure, ProbabilityTheory.cdf_paretoMeasure_eq_lintegral, MeasureTheory.aecover_Ico_of_Icc, MeasureTheory.integral_Iic_mul_deriv_eq_deriv_mul, MeasureTheory.withDensity_indicator_one, integral_Iic_inv_one_add_sq, MeasureTheory.aecover_Ico_of_Ico, interval_average_eq, NumberField.mixedEmbedding.volume_eq_two_pi_pow_mul_integral, ProbabilityTheory.Kernel.setLIntegral_const, Real.integral_rpowIntegrand₀₁_eq_rpow_mul_const, MeasureTheory.setIntegral_le_nonneg, restrict_apply', ProbabilityTheory.gaussianReal_apply_eq_integral, MeasureTheory.setIntegral_mono_ae, VitaliFamily.ae_tendsto_average, ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral, Measurable.setLIntegral_kernel_prod_right, MeasureTheory.ae_restrict_iUnion_iff, indicator_ae_eq_restrict, MeasureTheory.lintegral_deriv_eq_volume_image_of_monotoneOn, ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat_rat, MeasureTheory.integral_norm_eq_pos_sub_neg, exists_eq_interval_average, MeasureTheory.IsAddFundamentalDomain.absolutelyContinuous_map, integral_exp_Iic_zero, PMF.restrict_toMeasure_support, MeasureTheory.tilted_apply_eq_ofReal_integral', MeasureTheory.instSFiniteRestrict, MeasureTheory.setIntegral_congr_fun₀, MeasureTheory.IsAddFundamentalDomain.setIntegral_eq_tsum', MeasureTheory.lintegral_biUnion₀, sum_mul_eq_sub_integral_mul₀, MeasureTheory.average_union_mem_openSegment, MeasureTheory.aecover_Icc_of_Ico, setLIntegral_rnDeriv_le, MeasureTheory.setLIntegral_condLExp, restrict_apply₀', MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure, MeasureTheory.continuous_setIntegral, NumberField.mixedEmbedding.integral_comp_polarCoord_symm, MeasureTheory.average_union, ContinuousOn.aemeasurable₀, sum_restrict_le, MeasureTheory.setLIntegral_le_meas, MeasureTheory.integral_iUnion_fintype, restrict_eq_self, tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn, MeasureTheory.MeasurePreserving.restrict_preimage_emb, MeasureTheory.setLAverage_lt_top, MeasureTheory.setIntegral_mono_on, Complex.integral_cpow_mul_exp_neg_mul_Ioi, MeasureTheory.lintegral_piecewise, MeasureTheory.aecover_Ioo_of_Icc, ProbabilityTheory.Kernel.setIntegral_comp, LipschitzOnWith.ae_differentiableWithinAt, lintegral_rnDeriv_lt_top_of_measure_ne_top, MeasureTheory.ae_restrict_uIoc_eq, intervalIntegral.norm_integral_le_integral_norm_uIoc, ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat, VitaliFamily.ae_tendsto_lintegral_enorm_sub_div_of_integrable, restrict_union_le, MeasureTheory.AECover.iSup_lintegral_eq_of_countably_generated, sum_mul_eq_sub_sub_integral_mul, MeasureTheory.eLpNorm_restrict_le, VitaliFamily.ae_tendsto_lintegral_enorm_sub_div, MeasureTheory.setIntegral_eq_zero_of_ae_eq_zero, setIntegral_toReal_rnDeriv, ProbabilityTheory.Kernel.compProd_apply_prod, MeasureTheory.IsFundamentalDomain.integral_eq_tsum', VitaliFamily.ae_tendsto_lintegral_enorm_sub_div'_of_integrable, restrict_iUnion_congr, UnitAddCircle.integral_preimage, MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg', aemeasurable_restrict_of_antitoneOn, MeasureTheory.setLIntegral_iUnion_of_directed, MeasureTheory.Integrable.integral_eq_integral_Ioc_meas_le, MeasureTheory.LocallyIntegrableOn.aestronglyMeasurable, MeasureTheory.restrict_withDensity', restrict_toMeasurable_of_sFinite, restrict_compl_add_restrict, MeasureTheory.tendsto_integral_meas_thickening_le, ProbabilityTheory.Kernel.setIntegral_traj_partialTraj', Real.exists_measure_rpow_eq_integral, le_restrict_apply, MeasureTheory.measure_mul_setLAverage, ProbabilityTheory.Kernel.setLIntegral_rnDerivAux, MeasureTheory.ae_eq_restrict_iUnion_iff, MeasureTheory.integral_Iic_deriv_mul_eq_sub, integral_pow_abs_sub_uIoc, MeasureTheory.setLIntegral_le_lintegral, NumberField.mixedEmbedding.integral_comp_polarCoordReal_symm, MeasureTheory.map_withDensity_abs_det_fderiv_eq_addHaar, AddCircle.integral_preimage, MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_le, integral_comp_pi_polarCoord_symm, MeasureTheory.measureReal_restrict_apply, restrict_prod_eq_prod_univ, MeasureTheory.integral_iUnion_ae, MeasureTheory.integral_Icc_eq_integral_Ioc, toSignedMeasure_restrict_sub, MeasureTheory.restrict_Ioc_eq_restrict_Icc, MeasureTheory.ae_restrict_union_eq, LSeries_eq_mul_integral', ProbabilityTheory.exponentialCDFReal_eq_lintegral, MeasureTheory.sum_restrict_disjointed_spanningSets, MeasureTheory.IsFundamentalDomain.measurePreserving_quotient_mk, setLIntegral_condKernel_eq_measure_prod, MeasureTheory.setIntegral_setAverage, ProbabilityTheory.Kernel.setLIntegral_rnDeriv_le, ProbabilityTheory.cdf_gammaMeasure_eq_integral, MonotoneOn.ae_differentiableWithinAt, MeasureTheory.setIntegral_univ, support_restrict_subset, aestronglyMeasurable_indicator_iff, ContinuousOn.aestronglyMeasurable_of_isSeparable, ProbabilityTheory.tilted_mul_apply_cgf', MeasureTheory.setLIntegral_indicator, MeasureTheory.self_mem_ae_restrict, ProbabilityTheory.Kernel.lintegral_restrict, MeasureTheory.IsHahnDecomposition.le_on, MeasureTheory.measureReal_restrict_apply₀', MeasureTheory.integral_comp_mul_deriv_Ioi, MeasureTheory.AEFinStronglyMeasurable.exists_set_sigmaFinite, MeasureTheory.iInf_mul_le_setLIntegral, MeasureTheory.measure_sigmaFiniteSetGE_ge, MeasureTheory.Lp_toLp_restrict_smul, MeasureTheory.setIntegral_prod, MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on, MeasureTheory.AECover.lintegral_tendsto_of_nat, MeasureTheory.tilted_apply', aemeasurable_indicator_iff₀, MeasureTheory.setLIntegral_congr, MeasureTheory.IsFundamentalDomain.integral_eq_tsum, MeasureTheory.setLIntegral_lt_top_of_isCompact, MeasureTheory.withDensity_apply, integral_gaussian_complex_Ioi, MeasureTheory.setLIntegral_mono', restrict_inter_add_diff, restrict_univ, lintegral_Iic_eq_lintegral_Iio_add_Icc, ProbabilityTheory.setLIntegral_toKernel_Iic, MeasureTheory.tendsto_setLIntegral_zero, restrict_iUnion_le, MeasureTheory.setLIntegral_condLExp_trim, iSup_restrict_spanningSets_of_measurableSet, ext_iff_of_biUnion_eq_univ, MeasureTheory.IntegrableOn.restrict, MeasureTheory.integral_image_eq_integral_deriv_smul_of_monotoneOn, MeasureTheory.measureReal_restrict_apply_self, MeasureTheory.instIsFiniteMeasureOnCompactsRestrict, MeasureTheory.setLIntegral_univ, restrict_union_congr, NumberField.mixedEmbedding.lintegral_comp_polarSpaceCoord_symm, MeasureTheory.AEStronglyMeasurable.aestronglyMeasurable_uIoc_iff, MeasureTheory.setIntegral_const, MeasureTheory.integral_finset_biUnion, MeasureTheory.setLIntegral_measure_zero bridge: MeasureTheory.SimpleFunc.hasBoxIntegral, MeasureTheory.IntegrableOn.hasBoxIntegral, MeasureTheory.SimpleFunc.box_integral_eq_integral
restrictₗ 📖	CompOp	1 math math: restrictₗ_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absolutelyContinuous_restrict 📖	mathematical	—	AbsolutelyContinuous restrict	—	absolutelyContinuous_of_le restrict_le_self
exists_mem_of_measure_ne_zero_of_ae 📖	mathematical	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass restrict	Set Set.instMembership	—	instOuterMeasureClass Filter.Frequently.exists Filter.Frequently.and_eventually MeasureTheory.frequently_ae_mem_iff restrict_apply_self
ext_iff_of_biUnion_eq_univ 📖	mathematical	Set.iUnion Set Set.instMembership Set.univ	restrict	—	restrict_biUnion_congr restrict_univ
ext_iff_of_iUnion_eq_univ 📖	mathematical	Set.iUnion Set.univ	restrict	—	restrict_iUnion_congr restrict_univ
ext_iff_of_sUnion_eq_univ 📖	mathematical	Set.sUnion Set.univ	restrict	—	ext_iff_of_biUnion_eq_univ Set.sUnion_eq_biUnion
ext_of_biUnion_eq_univ 📖	—	Set.iUnion Set Set.instMembership Set.univ restrict	—	—	ext_iff_of_biUnion_eq_univ
ext_of_generateFrom_of_cover 📖	—	MeasurableSpace.generateFrom IsPiSystem Set.sUnion Set.univ DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Set.instInter	—	—	ext_of_sUnion_eq_univ ext restrict_apply MeasurableSpace.induction_on_inter Set.empty_inter MeasureTheory.measure_empty instOuterMeasureClass Set.inter_comm ne_top_of_le_ne_top MeasureTheory.measure_mono Set.inter_subset_left MeasureTheory.measure_inter_add_diff MeasurableSet.iUnion instCountableNat MeasureTheory.measure_iUnion
ext_of_generateFrom_of_cover_subset 📖	—	MeasurableSpace.generateFrom IsPiSystem Set Set.instHasSubset Set.sUnion Set.univ DFunLike.coe MeasureTheory.Measure ENNReal instFunLike	—	—	ext_of_generateFrom_of_cover Set.eq_empty_or_nonempty MeasureTheory.measure_empty instOuterMeasureClass
ext_of_generateFrom_of_iUnion 📖	—	MeasurableSpace.generateFrom IsPiSystem Set.iUnion Set.univ Set Set.instMembership DFunLike.coe MeasureTheory.Measure ENNReal instFunLike	—	—	ext_of_generateFrom_of_cover_subset Set.countable_range instCountableNat
ext_of_iUnion_eq_univ 📖	—	Set.iUnion Set.univ restrict	—	—	ext_iff_of_iUnion_eq_univ
ext_of_sUnion_eq_univ 📖	—	Set.sUnion Set.univ restrict	—	—	ext_iff_of_sUnion_eq_univ
le_restrict_apply 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set instFunLike Set.instInter restrict	—	restrict_eq_self Set.inter_subset_right MeasureTheory.measure_mono instOuterMeasureClass Set.inter_subset_left
map_eq_comap 📖	mathematical	Measurable MeasurableEmbedding Filter.Eventually Set Set.instMembership Set.range MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass	map comap	—	instOuterMeasureClass ext map_apply MeasurableEmbedding.comap_apply MeasureTheory.measure_diff_null sdiff_compl
measure_inter_eq_zero_of_restrict 📖	mathematical	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike restrict instZeroENNReal	Set.instInter	—	nonpos_iff_eq_zero ENNReal.instCanonicallyOrderedAdd le_restrict_apply
measure_subtype_coe_eq_zero_of_comap_eq_zero 📖	mathematical	MeasureTheory.NullMeasurableSet DFunLike.coe MeasureTheory.Measure Set Set.instMembership Subtype.instMeasurableSpace ENNReal instFunLike comap instZeroENNReal	Set.image	—	eq_bot_iff LE.le.trans measure_subtype_coe_le_comap Eq.le
measure_subtype_coe_le_comap 📖	mathematical	MeasureTheory.NullMeasurableSet	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set instFunLike Set.image Set.instMembership Subtype.instMeasurableSpace comap	—	le_comap_apply Subtype.coe_injective MeasurableSet.nullMeasurableSet_subtype_coe
restrict_add 📖	mathematical	—	restrict MeasureTheory.Measure instAdd	—	LinearMap.map_add IsScalarTower.right
restrict_add_restrict_compl 📖	mathematical	MeasurableSet	MeasureTheory.Measure instAdd restrict Compl.compl Set Set.instCompl	—	restrict_union disjoint_compl_right MeasurableSet.compl Set.union_compl_self restrict_univ
restrict_apply 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike restrict Set.instInter	—	restrict_apply₀ MeasurableSet.nullMeasurableSet
restrict_apply' 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike restrict Set.instInter	—	toOuterMeasure_apply IsScalarTower.right restrict_toOuterMeasure_eq_toOuterMeasure_restrict MeasureTheory.OuterMeasure.restrict_apply
restrict_apply_eq_zero 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike restrict instZeroENNReal Set.instInter	—	restrict_apply
restrict_apply_eq_zero' 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike restrict instZeroENNReal Set.instInter	—	restrict_apply'
restrict_apply_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set instFunLike restrict	—	le_iff' restrict_le_self
restrict_apply_self 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike restrict	—	restrict_eq_self Set.Subset.rfl
restrict_apply_superset 📖	mathematical	Set Set.instHasSubset	DFunLike.coe MeasureTheory.Measure ENNReal instFunLike restrict	—	LE.le.antisymm LE.le.trans_eq MeasureTheory.measure_mono instOuterMeasureClass Set.subset_univ restrict_apply_univ Eq.trans_le restrict_apply_self
restrict_apply_univ 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike restrict Set.univ	—	restrict_apply MeasurableSet.univ Set.univ_inter
restrict_apply₀ 📖	mathematical	MeasureTheory.NullMeasurableSet restrict	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Set.instInter	—	IsScalarTower.right restrictₗ_apply restrictₗ.eq_1 liftLinear_apply₀ restrict.eq_1 MeasureTheory.OuterMeasure.restrict_apply coe_toOuterMeasure
restrict_apply₀' 📖	mathematical	MeasureTheory.NullMeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike restrict Set.instInter	—	restrict_congr_set MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq restrict_apply' MeasureTheory.measurableSet_toMeasurable MeasureTheory.measure_congr instOuterMeasureClass Filter.EventuallyEq.inter MeasureTheory.ae_eq_refl
restrict_biUnion 📖	mathematical	Set.Pairwise Function.onFun Set Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice MeasurableSet	restrict Set.iUnion Set.instMembership sum Set.Elem	—	Set.biUnion_eq_iUnion restrict_iUnion Subtype.coe_prop Subtype.coe_ne_coe
restrict_biUnion_congr 📖	mathematical	—	restrict Set.iUnion Set Set.instMembership	—	Set.biUnion_eq_iUnion Encodable.countable
restrict_biUnion_finset 📖	mathematical	Set.Pairwise SetLike.coe Finset Finset.instSetLike Function.onFun Set Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice MeasurableSet	restrict Set.iUnion Finset.instMembership sum SetLike.instMembership	—	restrict_biUnion Finite.to_countable Finite.of_fintype
restrict_biUnion_finset_congr 📖	mathematical	—	restrict Set.iUnion Finset Finset.instMembership	—	Finset.induction_on Set.iUnion_congr_Prop Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty restrict_empty Set.iUnion_iUnion_eq_or_left restrict_union_congr
restrict_biUnion_le 📖	mathematical	—	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict Set.iUnion Set Set.instMembership sum Set.Elem	—	le_iff restrict_apply Set.inter_iUnion sum_apply MeasureTheory.measure_biUnion_le instOuterMeasureClass
restrict_comm 📖	mathematical	MeasurableSet	restrict	—	restrict_restrict restrict_restrict' Set.inter_comm
restrict_compl_add_restrict 📖	mathematical	MeasurableSet	MeasureTheory.Measure instAdd restrict Compl.compl Set Set.instCompl	—	add_comm restrict_add_restrict_compl
restrict_congr_meas 📖	mathematical	MeasurableSet	restrict DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike	—	Set.inter_eq_self_of_subset_left restrict_apply ext Set.inter_subset_right MeasurableSet.inter
restrict_congr_mono 📖	—	Set Set.instHasSubset restrict	—	—	restrict_restrict_of_subset
restrict_congr_set 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass	restrict	—	instOuterMeasureClass le_antisymm restrict_mono_ae Filter.EventuallyEq.le Filter.EventuallyEq.symm
restrict_empty 📖	mathematical	—	restrict Set Set.instEmptyCollection MeasureTheory.Measure instZero	—	restrict_zero_set MeasureTheory.measure_empty instOuterMeasureClass
restrict_eq_self 📖	mathematical	Set Set.instHasSubset	DFunLike.coe MeasureTheory.Measure ENNReal instFunLike restrict	—	LE.le.antisymm le_iff' restrict_le_self MeasureTheory.measure_mono instOuterMeasureClass Set.subset_inter MeasureTheory.subset_toMeasurable restrict_apply MeasureTheory.measurableSet_toMeasurable MeasureTheory.measure_toMeasurable
restrict_eq_self_of_ae_mem 📖	mathematical	Filter.Eventually Set Set.instMembership MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass	restrict	—	instOuterMeasureClass restrict_congr_set Filter.eventuallyEq_univ restrict_univ
restrict_eq_zero 📖	mathematical	—	restrict MeasureTheory.Measure instZero DFunLike.coe Set ENNReal instFunLike instZeroENNReal	—	measure_univ_eq_zero restrict_apply_univ
restrict_finset_biUnion_congr 📖	mathematical	—	restrict Set.iUnion Finset Finset.instMembership	—	restrict_biUnion_finset_congr
restrict_iUnion 📖	mathematical	Pairwise Function.onFun Set Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice MeasurableSet	restrict Set.iUnion sum	—	restrict_iUnion_ae Pairwise.aedisjoint MeasurableSet.nullMeasurableSet
restrict_iUnion_ae 📖	mathematical	Pairwise Function.onFun Set MeasureTheory.AEDisjoint MeasureTheory.NullMeasurableSet	restrict Set.iUnion sum	—	ext restrict_iUnion_apply_ae sum_apply
restrict_iUnion_apply 📖	mathematical	Pairwise Function.onFun Set Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice MeasurableSet	DFunLike.coe MeasureTheory.Measure ENNReal instFunLike restrict Set.iUnion tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	restrict_iUnion_apply_ae Pairwise.aedisjoint MeasurableSet.nullMeasurableSet
restrict_iUnion_apply_ae 📖	mathematical	Pairwise Function.onFun Set MeasureTheory.AEDisjoint MeasureTheory.NullMeasurableSet MeasurableSet	DFunLike.coe MeasureTheory.Measure ENNReal instFunLike restrict Set.iUnion tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	restrict_apply Set.inter_iUnion MeasureTheory.measure_iUnion₀ Pairwise.mono MeasureTheory.AEDisjoint.mono Set.inter_subset_right MeasureTheory.NullMeasurableSet.inter MeasurableSet.nullMeasurableSet
restrict_iUnion_apply_eq_iSup 📖	mathematical	Directed Set Set.instHasSubset MeasurableSet	DFunLike.coe MeasureTheory.Measure ENNReal instFunLike restrict Set.iUnion iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	restrict_apply Set.inter_iUnion Directed.measure_iUnion Directed.mono_comp Set.inter_subset_inter_right
restrict_iUnion_congr 📖	mathematical	—	restrict Set.iUnion	—	restrict_congr_mono Set.subset_iUnion ext Monotone.directed_le Finset.isDirected_le Set.biUnion_subset_biUnion_left Set.iUnion_eq_iUnion_finset restrict_iUnion_apply_eq_iSup Finset.countable restrict_biUnion_finset_congr
restrict_iUnion_le 📖	mathematical	—	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict Set.iUnion sum	—	le_iff restrict_apply Set.inter_iUnion sum_apply MeasureTheory.measure_iUnion_le instOuterMeasureClass
restrict_inter_add_diff 📖	mathematical	MeasurableSet	MeasureTheory.Measure instAdd restrict Set Set.instInter Set.instSDiff	—	restrict_inter_add_diff₀ MeasurableSet.nullMeasurableSet
restrict_inter_add_diff₀ 📖	mathematical	MeasureTheory.NullMeasurableSet	MeasureTheory.Measure instAdd restrict Set Set.instInter Set.instSDiff	—	ext restrict_apply MeasureTheory.measure_inter_add_diff₀
restrict_inter_toMeasurable 📖	mathematical	MeasurableSet Set Set.instHasSubset	restrict Set.instInter MeasureTheory.toMeasurable	—	ext restrict_apply Set.inter_comm Set.inter_assoc measure_toMeasurable_inter MeasurableSet.inter
restrict_le_self 📖	mathematical	—	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict	—	le_iff restrict_apply MeasureTheory.measure_mono instOuterMeasureClass Set.inter_subset_left
restrict_map 📖	mathematical	Measurable MeasurableSet	restrict map Set.preimage	—	ext restrict_apply map_apply
restrict_mono 📖	mathematical	Set Set.instHasSubset MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder	restrict	—	restrict_mono' MeasureTheory.ae_of_all instOuterMeasureClass
restrict_mono' 📖	mathematical	Filter.EventuallyLE Prop.le MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass Preorder.toLE PartialOrder.toPreorder instPartialOrder	restrict	—	instOuterMeasureClass le_iff restrict_apply MeasureTheory.measure_mono_ae Filter.Eventually.mono le_iff'
restrict_mono_ae 📖	mathematical	Filter.EventuallyLE Prop.le MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass	Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict	—	instOuterMeasureClass restrict_mono' le_refl
restrict_mono_measure 📖	mathematical	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder	restrict	—	restrict_mono subset_rfl Set.instReflSubset
restrict_mono_set 📖	mathematical	Set Set.instHasSubset	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict	—	restrict_mono le_rfl
restrict_restrict 📖	mathematical	MeasurableSet	restrict Set Set.instInter	—	restrict_restrict₀ MeasurableSet.nullMeasurableSet
restrict_restrict' 📖	mathematical	MeasurableSet	restrict Set Set.instInter	—	restrict_restrict₀' MeasurableSet.nullMeasurableSet
restrict_restrict_of_subset 📖	mathematical	Set Set.instHasSubset	restrict	—	ext restrict_apply restrict_eq_self HasSubset.Subset.trans Set.instIsTransSubset Set.inter_subset_right
restrict_restrict₀ 📖	mathematical	MeasureTheory.NullMeasurableSet restrict	Set Set.instInter	—	ext restrict_apply restrict_apply₀ MeasureTheory.NullMeasurableSet.inter MeasurableSet.nullMeasurableSet Set.inter_assoc
restrict_restrict₀' 📖	mathematical	MeasureTheory.NullMeasurableSet	restrict Set Set.instInter	—	ext restrict_apply restrict_apply₀' Set.inter_assoc
restrict_sInf_eq_sInf_restrict 📖	mathematical	Set.Nonempty MeasureTheory.Measure MeasurableSet	restrict InfSet.sInf instInfSet Set.image	—	ext sInf_apply restrict_apply MeasurableSet.inter Set.image_image IsScalarTower.right Set.image_congr restrict_toOuterMeasure_eq_toOuterMeasure_restrict MeasureTheory.OuterMeasure.restrict_sInf_eq_sInf_restrict Set.Nonempty.image MeasureTheory.OuterMeasure.restrict_apply
restrict_sUnion_congr 📖	mathematical	—	restrict Set.sUnion	—	Set.sUnion_eq_biUnion restrict_biUnion_congr
restrict_smul 📖	mathematical	—	restrict MeasureTheory.Measure instSMul	—	IsScalarTower.right smul_one_smul instIsScalarTower LinearMap.map_smul
restrict_sum 📖	mathematical	MeasurableSet	restrict sum	—	ext restrict_apply sum_apply MeasurableSet.inter
restrict_sum_of_countable 📖	mathematical	—	restrict sum	—	ext sum_apply restrict_apply sum_apply_of_countable
restrict_toMeasurable 📖	mathematical	—	restrict MeasureTheory.toMeasurable	—	Set.univ_inter restrict_inter_toMeasurable MeasurableSet.univ Set.subset_univ
restrict_toOuterMeasure_eq_toOuterMeasure_restrict 📖	mathematical	MeasurableSet	toOuterMeasure restrict DFunLike.coe LinearMap ENNReal CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.addCommMonoid MeasureTheory.OuterMeasure.instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike MeasureTheory.OuterMeasure.restrict	—	IsScalarTower.right restrictₗ.eq_1 MeasureTheory.OuterMeasure.restrict_trim trimmed
restrict_union 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice MeasurableSet	restrict Set.instUnion MeasureTheory.Measure instAdd	—	restrict_union₀ Disjoint.aedisjoint MeasurableSet.nullMeasurableSet
restrict_union' 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice MeasurableSet	restrict Set.instUnion MeasureTheory.Measure instAdd	—	Set.union_comm restrict_union Disjoint.symm add_comm
restrict_union_add_inter 📖	mathematical	MeasurableSet	MeasureTheory.Measure instAdd restrict Set Set.instUnion Set.instInter	—	restrict_union_add_inter₀ MeasurableSet.nullMeasurableSet
restrict_union_add_inter' 📖	mathematical	MeasurableSet	MeasureTheory.Measure instAdd restrict Set Set.instUnion Set.instInter	—	add_comm Set.union_comm Set.inter_comm restrict_union_add_inter
restrict_union_add_inter₀ 📖	mathematical	MeasureTheory.NullMeasurableSet	MeasureTheory.Measure instAdd restrict Set Set.instUnion Set.instInter	—	restrict_inter_add_diff₀ Set.union_inter_cancel_right Set.union_diff_right add_comm add_assoc add_right_comm
restrict_union_congr 📖	mathematical	—	restrict Set Set.instUnion	—	restrict_congr_mono Set.subset_union_left Set.subset_union_right ext restrict_apply Set.inter_union_distrib_left MeasureTheory.exists_measurable_superset₂ MeasureTheory.measure_union_congr_of_subset Eq.le Set.Subset.rfl le_rfl MeasureTheory.measure_add_diff MeasurableSet.nullMeasurableSet Set.inter_comm Set.inter_diff_assoc MeasurableSet.diff
restrict_union_le 📖	mathematical	—	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict Set Set.instUnion instAdd	—	le_iff restrict_apply Set.inter_union_distrib_left MeasureTheory.measure_union_le instOuterMeasureClass
restrict_union₀ 📖	mathematical	MeasureTheory.AEDisjoint MeasureTheory.NullMeasurableSet	restrict Set Set.instUnion MeasureTheory.Measure instAdd	—	restrict_union_add_inter₀ restrict_zero_set add_zero
restrict_univ 📖	mathematical	—	restrict Set.univ	—	ext restrict_apply Set.inter_univ
restrict_zero 📖	mathematical	—	restrict MeasureTheory.Measure instZero	—	LinearMap.map_zero IsScalarTower.right
restrict_zero_set 📖	mathematical	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike instZeroENNReal	restrict instZero	—	restrict_eq_zero
restrictₗ_apply 📖	mathematical	—	DFunLike.coe LinearMap ENNReal CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.Measure instAddCommMonoid instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike restrictₗ restrict	—	IsScalarTower.right
sum_restrict_le 📖	mathematical	MeasurableSet ENat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Set.encard setOf Set Set.instMembership ENat.instNatCast	MeasureTheory.Measure instPartialOrder sum restrict AddMonoid.toNatSMul AddCommMonoid.toAddMonoid instAddCommMonoid Set.iUnion	—	le_iff sum_apply Summable.tsum_le_of_sum_le OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology SummationFilter.instNeBotUnconditional ENNReal.summable MeasurableSet.inter Finset.measurableSet_biInter MeasurableSet.compl Set.mem_biUnion Finset.mem_powerset Finset.filter_subset Finset.mem_filter Set.iUnion_congr_Prop Finset.nonempty_iff_ne_empty Finset.notMem_singleton Set.iInter_congr_Prop Set.iInter_true of_not_not Set.mem_iInter₂ Set.mem_inter_iff Finset.mem_sdiff Finset.sdiff_subset Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid LE.le.trans restrict_mono_set restrict_biUnion_le Set.Finite.countable Set.Finite.subset Finset.finite_toSet Set.sep_subset Finset.sum_congr Summable.tsum_finsetSum ENNReal.instT2Space ENNReal.instContinuousAdd tsum_subtype sum_eq_tsum_indicator SummationFilter.instLeAtTopUnconditional Finset.sum_const_zero Finset.coe_sdiff Finset.coe_singleton Finset.sum_ite_mem Finset.sum_const nsmul_eq_mul restrict_empty nsmul_zero Set.nonempty_iff_ne_empty Set.encard_mono nsmul_le_nsmul_left zero_le ENNReal.instCanonicallyOrderedAdd Finset.card_mono Set.ncard_coe_finset ENat.toNat_le_of_le_coe Finset.smul_sum Finset.tsum_subtype restrict_biUnion_finset Set.disjoint_iff subset_antisymm Finset.instAntisymmSubset Set.inter_comm smul_apply nsmul_le_nsmul_right covariant_swap_add_of_covariant_add
volume_subtype_coe_eq_zero_of_volume_eq_zero 📖	mathematical	MeasureTheory.NullMeasurableSet MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.volume DFunLike.coe MeasureTheory.Measure Set.Elem Subtype.measureSpace Set Set.instMembership ENNReal instFunLike instZeroENNReal	Set.image	—	measure_subtype_coe_eq_zero_of_comap_eq_zero
volume_subtype_coe_le_volume 📖	mathematical	MeasureTheory.NullMeasurableSet MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.volume	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set instFunLike Set.image Set.instMembership Set.Elem Subtype.measureSpace	—	measure_subtype_coe_le_comap

MeasureTheory.Measure.AbsolutelyContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrict 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous	MeasureTheory.Measure.restrict	—	MeasureTheory.Measure.restrict_apply

MeasureTheory.Measure.MeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nullMeasurableSet_subtype_coe 📖	mathematical	MeasureTheory.NullMeasurableSet MeasurableSet Set.Elem Subtype.instMeasurableSpace Set Set.instMembership	Set.image	—	MeasurableSpace.generateFrom_induction Subtype.image_preimage_coe MeasureTheory.NullMeasurableSet.inter MeasurableSet.nullMeasurableSet Set.image_empty Set.range_diff_image Subtype.coe_injective Subtype.range_coe_subtype MeasureTheory.NullMeasurableSet.diff Set.image_iUnion MeasureTheory.NullMeasurableSet.iUnion instCountableNat MeasurableSpace.comap_eq_generateFrom Subtype.instMeasurableSpace.eq_1

MeasureTheory.Measure.NullMeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
subtype_coe 📖	mathematical	MeasureTheory.NullMeasurableSet Set.Elem Subtype.instMeasurableSpace Set Set.instMembership MeasureTheory.Measure.comap	Set.image	—	image Subtype.coe_injective MeasureTheory.Measure.MeasurableSet.nullMeasurableSet_subtype_coe

MeasureTheory.Measure.QuasiMeasurePreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_eq_comp 📖	—	MeasureTheory.Measure.QuasiMeasurePreserving Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_eq_comp' aemeasurable absolutelyContinuous
restrict 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving Set.MapsTo	MeasureTheory.Measure.restrict	—	measurable MeasureTheory.measure_mono_null MeasureTheory.Measure.instOuterMeasureClass Set.preimage_inter Set.inter_subset_inter subset_refl Set.instReflSubset preimage_null MeasureTheory.Measure.restrict_apply MeasureTheory.Measure.map_apply

MeasureTheory.Measure.Subtype

Definitions

Name	Category	Theorems
measureSpace 📖	CompOp	9 math math: volume_set_coe_def, MeasurableSet.map_coe_volume, volume_def, MeasureTheory.Measure.volume_subtype_coe_le_volume, volume_univ, MeasureTheory.integral_subtype, Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc, volume_preimage_coe, volume_image_subtype_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
volume_def 📖	mathematical	—	MeasureTheory.MeasureSpace.volume Set.Elem measureSpace Set Set.instMembership MeasureTheory.Measure.comap MeasureTheory.MeasureSpace.toMeasurableSpace	—	—
volume_univ 📖	mathematical	MeasureTheory.NullMeasurableSet MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.volume	DFunLike.coe MeasureTheory.Measure Set.Elem measureSpace Set Set.instMembership ENNReal MeasureTheory.Measure.instFunLike Set.univ	—	volume_def MeasureTheory.Measure.comap_apply₀ Subtype.coe_injective MeasureTheory.Measure.MeasurableSet.nullMeasurableSet_subtype_coe MeasurableSet.nullMeasurableSet MeasurableSet.univ Set.image_univ Subtype.range_coe_subtype

MeasureTheory.Measure.restrict

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
neZero 📖	mathematical	—	MeasureTheory.Measure MeasureTheory.Measure.instZero MeasureTheory.Measure.restrict	—	MeasureTheory.Measure.restrict_eq_zero

MeasureTheory.NullMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measure_preimage_eq_measure_restrict_preimage_of_ae_compl_eq_const 📖	mathematical	MeasureTheory.NullMeasurable MeasureTheory.Measure.restrict Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Compl.compl Set Set.instCompl MeasurableSet Set.instMembership	DFunLike.coe ENNReal Set.preimage	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict_apply₀ le_antisymm LE.le.trans MeasureTheory.measure_mono Eq.le Set.inter_union_compl MeasureTheory.measure_union_le MeasureTheory.NullMeasurableSet.of_null MeasureTheory.ae_iff Filter.EventuallyEq.eq_1 Set.inter_subset_inter_left zero_le ENNReal.instCanonicallyOrderedAdd add_zero Set.inter_subset_left

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_eq_restrict_iff_indicator_ae_eq 📖	mathematical	MeasurableSet	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict Set.indicator	—	MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyEq.eq_1 MeasureTheory.ae_restrict_iff' Filter.mp_mem Filter.univ_mem' Set.indicator_of_mem Set.indicator_of_notMem
ae_restrict_iff_subtype 📖	mathematical	MeasurableSet	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict Set.Elem Set Set.instMembership Subtype.instMeasurableSpace MeasureTheory.Measure.comap	—	MeasureTheory.Measure.instOuterMeasureClass map_comap_subtype_coe MeasurableEmbedding.ae_map_iff MeasurableEmbedding.subtype_coe
comap_subtype_coe_apply 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set.Elem Subtype.instMeasurableSpace Set Set.instMembership ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.comap Set.image	—	MeasurableEmbedding.comap_apply MeasurableEmbedding.subtype_coe
indicator_ae_eq_of_ae_eq_set 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Set.indicator	—	MeasureTheory.Measure.instOuterMeasureClass piecewise_ae_eq_of_ae_eq_set
indicator_ae_eq_of_restrict_compl_ae_eq_zero 📖	mathematical	MeasurableSet Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict Compl.compl Set Set.instCompl Pi.instZero	Set.indicator	—	MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem MeasureTheory.ae_restrict_iff' MeasurableSet.compl Filter.EventuallyEq.eq_1 Filter.univ_mem' Set.indicator_of_mem
indicator_ae_eq_restrict 📖	mathematical	MeasurableSet	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict Set.indicator	—	piecewise_ae_eq_restrict
indicator_ae_eq_restrict_compl 📖	mathematical	MeasurableSet	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict Compl.compl Set Set.instCompl Set.indicator Pi.instZero	—	piecewise_ae_eq_restrict_compl
indicator_ae_eq_zero_of_restrict_ae_eq_zero 📖	mathematical	MeasurableSet Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict Pi.instZero	Set.indicator	—	MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem MeasureTheory.ae_restrict_iff' Filter.EventuallyEq.eq_1 Filter.univ_mem' Set.indicator_of_mem Set.indicator_of_notMem
indicator_meas_zero 📖	mathematical	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike instZeroENNReal	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure.instOuterMeasureClass Set.indicator Pi.instZero	—	MeasureTheory.Measure.instOuterMeasureClass indicator_ae_eq_of_ae_eq_set MeasureTheory.ae_eq_empty Set.indicator_empty'
map_comap_subtype_coe 📖	mathematical	MeasurableSet	MeasureTheory.Measure.map Set Set.instMembership Subtype.instMeasurableSpace MeasureTheory.Measure.comap MeasureTheory.Measure.restrict	—	MeasurableEmbedding.map_comap MeasurableEmbedding.subtype_coe Subtype.range_coe
map_restrict_ae_le_map_indicator_ae 📖	mathematical	MeasurableSet	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.map MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict Set.indicator	—	MeasureTheory.Measure.instOuterMeasureClass mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem mem_map_indicator_ae_iff_of_zero_notMem MeasureTheory.mem_map_restrict_ae_iff MeasureTheory.measure_mono_null HasSubset.Subset.trans Set.instIsTransSubset Set.inter_subset_left Set.subset_union_left
mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem 📖	mathematical	Set Set.instMembership MeasurableSet	Filter Filter.instMembership Filter.map Set.indicator MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict_apply' Set.indicator_preimage Set.ite.eq_1 Set.compl_union Set.compl_inter Set.preimage_const compl_compl Set.union_inter_distrib_right Set.compl_inter_self Set.union_empty
mem_map_indicator_ae_iff_of_zero_notMem 📖	mathematical	Set Set.instMembership	Filter Filter.instMembership Filter.map Set.indicator MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ENNReal Set.instUnion Compl.compl Set.instCompl Set.preimage instZeroENNReal	—	MeasureTheory.Measure.instOuterMeasureClass Filter.mem_map MeasureTheory.mem_ae_iff Set.indicator_preimage Set.ite.eq_1 Set.compl_union Set.compl_inter Set.preimage_const Set.empty_diff Set.compl_empty Set.inter_univ
piecewise_ae_eq_of_ae_eq_set 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Set.piecewise	—	MeasureTheory.Measure.instOuterMeasureClass Filter.Eventually.mono Filter.EventuallyEq.mem_iff
piecewise_ae_eq_restrict 📖	mathematical	MeasurableSet	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict Set.piecewise	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_restrict_eq Filter.EventuallyEq.filter_mono Set.EqOn.eventuallyEq Set.piecewise_eqOn inf_le_right
piecewise_ae_eq_restrict_compl 📖	mathematical	MeasurableSet	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict Compl.compl Set Set.instCompl Set.piecewise	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_restrict_eq MeasurableSet.compl Filter.EventuallyEq.filter_mono Set.EqOn.eventuallyEq Set.piecewise_eqOn_compl inf_le_right
volume_image_subtype_coe 📖	mathematical	MeasurableSet MeasureTheory.MeasureSpace.toMeasurableSpace	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume Set.image Set.Elem Set.instMembership MeasureTheory.Measure.Subtype.measureSpace	—	comap_subtype_coe_apply
volume_preimage_coe 📖	mathematical	MeasureTheory.NullMeasurableSet MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.volume MeasurableSet	DFunLike.coe MeasureTheory.Measure Set Set.instMembership MeasureTheory.Measure.Subtype.measureSpace ENNReal MeasureTheory.Measure.instFunLike Set.preimage Set.instInter	—	volume_set_coe_def MeasureTheory.Measure.comap_apply₀ Subtype.coe_injective MeasureTheory.Measure.MeasurableSet.nullMeasurableSet_subtype_coe MeasurableSet.nullMeasurableSet measurable_subtype_coe Set.image_preimage_eq_inter_range Subtype.range_coe
volume_set_coe_def 📖	mathematical	—	MeasureTheory.MeasureSpace.volume Set.Elem MeasureTheory.Measure.Subtype.measureSpace Set Set.instMembership MeasureTheory.Measure.comap Subtype.instMeasurableSpace MeasureTheory.MeasureSpace.toMeasurableSpace	—	—

---

← Back to Index