AEStronglyMeasurable

📁 Source: Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean

Statistics

Metric	Count
Definitions AEFinStronglyMeasurable, mk, sigmaFiniteSet, AEStronglyMeasurable, mk, «termAEStronglyMeasurable[_]»	6
Theorems aestronglyMeasurable, aestronglyMeasurable, comp_aestronglyMeasurable, comp_aestronglyMeasurable₂, aestronglyMeasurable_fun_prod, aestronglyMeasurable_fun_sum, aestronglyMeasurable_prod, aestronglyMeasurable_sum, aestronglyMeasurable_const_smul_iff, aestronglyMeasurable_fun_prod, aestronglyMeasurable_fun_sum, aestronglyMeasurable_prod, aestronglyMeasurable_sum, aestronglyMeasurable, aestronglyMeasurable_map_iff, add, ae_eq_mk, ae_eq_zero_compl, aemeasurable, const_smul, exists_set_sigmaFinite, finStronglyMeasurable_mk, inf, measurableSet, mul, neg, sigmaFinite_restrict, sub, sup, add, add_const, add_iff_left, add_iff_right, add_measure, ae_eq_mk, ae_mem_imp_eq_mk, aemeasurable, aestronglyMeasurable_uIoc_iff, comp_aemeasurable, comp_measurable, comp_quasiMeasurePreserving, const_add, const_mul, const_nsmul, const_smul, const_smul', const_vadd, const_vadd', dist, div, div₀, edist, enorm, exists_stronglyMeasurable_range_subset, fst, iUnion, indicator, indicator₀, inf, inv, isSeparable_ae_range, measurable_mk, mono, mono_ac, mono_measure, mono_set, mul, mul_const, mul_iff_left, mul_iff_right, neg, nnnorm, norm, nullMeasurableSet_eq_fun, nullMeasurableSet_le, nullMeasurableSet_lt, nullMeasurableSet_mulSupport, nullMeasurableSet_support, of_discrete, of_measurableSpace_le_on, of_subsingleton_cod, of_subsingleton_dom, of_trim, piecewise, pow, prodMk, real_toNNReal, restrict, smul, smul_const, smul_measure, snd, stronglyMeasurable_mk, sub, sum_measure, sup, vadd, vadd_const, aefinStronglyMeasurable, aestronglyMeasurable, aestronglyMeasurable, aefinStronglyMeasurable_iff_aemeasurable, aefinStronglyMeasurable_of_aemeasurable, aefinStronglyMeasurable_zero, aestronglyMeasurable_const, aestronglyMeasurable_one, aestronglyMeasurable_zero, aestronglyMeasurable_zero_measure, aestronglyMeasurable_fun_prod, aestronglyMeasurable_fun_sum, aestronglyMeasurable_prod, aestronglyMeasurable_sum, aestronglyMeasurable_comp_iff, aestronglyMeasurable_add_measure_iff, aestronglyMeasurable_congr, aestronglyMeasurable_const_smul_iff, aestronglyMeasurable_const_smul_iff₀, aestronglyMeasurable_iUnion_iff, aestronglyMeasurable_id, aestronglyMeasurable_iff_aemeasurable, aestronglyMeasurable_iff_aemeasurable_separable, aestronglyMeasurable_iff_nullMeasurable_separable, aestronglyMeasurable_indicator_iff, aestronglyMeasurable_indicator_iff₀, aestronglyMeasurable_of_aestronglyMeasurable_trim, aestronglyMeasurable_of_tendsto_ae, aestronglyMeasurable_sum_measure_iff, aestronglyMeasurable_union_iff, exists_stronglyMeasurable_limit_of_tendsto_ae	129
Total	135

AEMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aestronglyMeasurable 📖	mathematical	AEMeasurable	MeasureTheory.AEStronglyMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass Measurable.stronglyMeasurable

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aestronglyMeasurable 📖	mathematical	Continuous	MeasureTheory.AEStronglyMeasurable	—	MeasureTheory.StronglyMeasurable.aestronglyMeasurable stronglyMeasurable
comp_aestronglyMeasurable 📖	mathematical	Continuous MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass comp_stronglyMeasurable Filter.EventuallyEq.fun_comp
comp_aestronglyMeasurable₂ 📖	mathematical	Continuous instTopologicalSpaceProd MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable	—	comp_aestronglyMeasurable MeasureTheory.AEStronglyMeasurable.prodMk

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aestronglyMeasurable_fun_prod 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable prod	—	aestronglyMeasurable_prod
aestronglyMeasurable_fun_sum 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable sum	—	sum_apply aestronglyMeasurable_sum
aestronglyMeasurable_prod 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable prod Pi.commMonoid	—	Multiset.aestronglyMeasurable_prod Multiset.mem_map
aestronglyMeasurable_sum 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable sum Pi.addCommMonoid	—	Multiset.aestronglyMeasurable_sum Multiset.mem_map

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aestronglyMeasurable_const_smul_iff 📖	mathematical	IsUnit	MeasureTheory.AEStronglyMeasurable SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	aestronglyMeasurable_const_smul_iff Units.continuousConstSMul

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aestronglyMeasurable_fun_prod 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toOne	—	aestronglyMeasurable_prod
aestronglyMeasurable_fun_sum 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddZero.toZero	—	Pi.list_sum_apply aestronglyMeasurable_sum
aestronglyMeasurable_prod 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable Pi.instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Pi.instOne MulOne.toOne	—	MeasureTheory.aestronglyMeasurable_one MeasureTheory.AEStronglyMeasurable.mul
aestronglyMeasurable_sum 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable Pi.instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass Pi.instZero AddZero.toZero	—	MeasureTheory.aestronglyMeasurable_zero MeasureTheory.AEStronglyMeasurable.add

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aestronglyMeasurable 📖	mathematical	Measurable	MeasureTheory.AEStronglyMeasurable	—	MeasureTheory.StronglyMeasurable.aestronglyMeasurable stronglyMeasurable

MeasurableEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aestronglyMeasurable_map_iff 📖	mathematical	MeasurableEmbedding	MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure.map	—	MeasureTheory.AEStronglyMeasurable.comp_measurable measurable MeasureTheory.Measure.instOuterMeasureClass exists_stronglyMeasurable_extend ae_map_iff

MeasureTheory

Definitions

Name	Category	Theorems
AEFinStronglyMeasurable 📖	MathDef	14 math math: aefinStronglyMeasurable_iff_aemeasurable, ENNReal.aefinStronglyMeasurable_of_aemeasurable, AEFinStronglyMeasurable.sub, AEFinStronglyMeasurable.neg, AEFinStronglyMeasurable.const_smul, AEFinStronglyMeasurable.sup, AEFinStronglyMeasurable.add, Integrable.aefinStronglyMeasurable, AEFinStronglyMeasurable.inf, MemLp.aefinStronglyMeasurable, aefinStronglyMeasurable_zero, FinStronglyMeasurable.aefinStronglyMeasurable, AEFinStronglyMeasurable.mul, aefinStronglyMeasurable_of_aemeasurable
AEStronglyMeasurable 📖	MathDef	213 math math: aestronglyMeasurable_const_smul_iff, AEMeasurable.aestronglyMeasurable, AEStronglyMeasurable.congr, aestronglyMeasurable_condExpInd, AEStronglyMeasurable.inv, mem_lpMeasSubgroup_iff_aestronglyMeasurable, Integrable.aestronglyMeasurable, AEStronglyMeasurable.div₀, Multiset.aestronglyMeasurable_fun_prod, AEStronglyMeasurable.integral_condDistrib_map, AEStronglyMeasurable.indicator₀, ProbabilityTheory.aemeasurable_exp_mul, IndexedPartition.aestronglyMeasurable_piecewise, IsFundamentalDomain.aestronglyMeasurable_on_iff, AEStronglyMeasurable.const_smul, AEStronglyMeasurable.comp_measurable, AEStronglyMeasurable.smul_const, MemLp.toLp_val, Continuous.comp_aestronglyMeasurable, ContinuousOn.aestronglyMeasurable_of_isCompact, aestronglyMeasurable_sum_measure_iff, IsAddFundamentalDomain.aestronglyMeasurable_on_iff, AEStronglyMeasurable.comp_measurePreserving, ContinuousMapZero.aeStronglyMeasurable_mkD_of_uncurry, aestronglyMeasurable_const, Lp.aestronglyMeasurable, aestronglyMeasurable_congr, AEStronglyMeasurable.sum_measure, AEStronglyMeasurable.sinc, AEStronglyMeasurable.add_measure, ProbabilityTheory.IdentDistrib.aestronglyMeasurable_fst, List.aestronglyMeasurable_fun_sum, AEStronglyMeasurable.add_const, MeasurableEmbedding.aestronglyMeasurable_map_iff, Real.aestronglyMeasurable_rpowIntegrand₀₁, AEStronglyMeasurable.integral_condExpKernel, withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part, AEStronglyMeasurable.inner_const, AEStronglyMeasurable.smul_measure, AEStronglyMeasurable.const_add, AEStronglyMeasurable.of_comp_fst, aestronglyMeasurable_condExpL2, AEStronglyMeasurable.comp_quasiMeasurePreserving, AEStronglyMeasurable.sub, aestronglyMeasurable_lineDeriv, uniformIntegrable_iff, AEStronglyMeasurable.nnnorm, StronglyMeasurable.aestronglyMeasurable, AEStronglyMeasurable.const_mul, AEStronglyMeasurable.prodMk_right, AEStronglyMeasurable.vadd, Measurable.aestronglyMeasurable, AEStronglyMeasurable.vadd_const, ContinuousOn.aestronglyMeasurable_of_subset_isCompact, AEStronglyMeasurable.piecewise, aestronglyMeasurable_zero_measure, AEStronglyMeasurable.star, AEStronglyMeasurable.dist, AEStronglyMeasurable.comp, List.aestronglyMeasurable_prod, aestronglyMeasurable_iff_aemeasurable_separable, aestronglyMeasurable_deriv, mem_lpMeas_iff_aestronglyMeasurable, aestronglyMeasurable_condExpL1, aestronglyMeasurable_indicator_iff₀, ProbabilityTheory.Kernel.aestronglyMeasurable_traj, ProbabilityTheory.aestronglyMeasurable_integral_condDistrib, AEStronglyMeasurable.of_discrete, IntervalIntegrable.aestronglyMeasurable', AEStronglyMeasurable.convolution_integrand_swap_snd', AEStronglyMeasurable.div, aestronglyMeasurable_derivWithin_Ioi, Continuous.aestronglyMeasurable_of_compactSpace, ContinuousMap.aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry, AEStronglyMeasurable.of_measurableSpace_le_on, Finset.aestronglyMeasurable_fun_sum, ContinuousLinearMap.aestronglyMeasurable_comp₂, AEStronglyMeasurable.mono_set, AEStronglyMeasurable.comp_snd_map_prod_id, ContinuousOn.aestronglyMeasurable, AEStronglyMeasurable.add, AEStronglyMeasurable.restrict, ProbabilityTheory.IdentDistrib.aestronglyMeasurable_snd, aestronglyMeasurable_smul_const_iff, isClosed_aestronglyMeasurable, AEStronglyMeasurable.integral_kernel_condKernel, AEStronglyMeasurable.inner, AEStronglyMeasurable.mono_ac, ProbabilityTheory.aestronglyMeasurable_comp_snd_map_prodMk_iff, aestronglyMeasurable_id, aestronglyMeasurable_of_tendsto_ae, AEStronglyMeasurable.convolution_integrand_snd', aestronglyMeasurable_derivWithin_Ici, aestronglyMeasurable_iUnion_iff, AEStronglyMeasurable.compProd_mk_left, MeasurePreserving.aestronglyMeasurable_comp_iff, aestronglyMeasurable_lineDeriv_uncurry, AEStronglyMeasurable.norm, AEStronglyMeasurable.neg, AEStronglyMeasurable.const_vadd, Multiset.aestronglyMeasurable_sum, Finset.aestronglyMeasurable_prod, IntervalIntegrable.aestronglyMeasurable, ProbabilityTheory.aestronglyMeasurable_exp_mul_sum, AEStronglyMeasurable.const_inner, AEStronglyMeasurable.truncation, IsUnit.aestronglyMeasurable_const_smul_iff, AEStronglyMeasurable.prodMk, AEStronglyMeasurable.integral_prod_right', StronglyMeasurableAtFilter.eventually, AEStronglyMeasurable.mul_iff_left, AEStronglyMeasurable.re, ContinuousMap.aeStronglyMeasurable_mkD_restrict_of_uncurry, AEStronglyMeasurable.fourierPowSMulRight, AEStronglyMeasurable.ae_of_compProd, List.aestronglyMeasurable_sum, AEStronglyMeasurable.pow, AEStronglyMeasurable.real_toNNReal, UniformIntegrable.aestronglyMeasurable, AEStronglyMeasurable.comp_aemeasurable, AEStronglyMeasurable.fourierSMulRight, aestronglyMeasurable_add_measure_iff, AEStronglyMeasurable.add_iff_left, AEStronglyMeasurable.prod_swap, ContinuousMap.aeStronglyMeasurable_restrict_mkD_of_uncurry, AEStronglyMeasurable.mono_measure, ProbabilityTheory.IdentDistrib.aestronglyMeasurable_iff, AEStronglyMeasurable.integral_condKernel, aestronglyMeasurable_condExpL1CLM, AEStronglyMeasurable.of_subsingleton_dom, AEStronglyMeasurable.im, ContinuousMapZero.aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry, AEStronglyMeasurable.fst, AEStronglyMeasurable.mul_iff_right, AEStronglyMeasurable.of_subsingleton_cod, AEStronglyMeasurable.mul_const, AEStronglyMeasurable.indicator, List.aestronglyMeasurable_fun_prod, AEStronglyMeasurable.comp_ae_measurable', isComplete_aestronglyMeasurable, aestronglyMeasurable_dirac, AEStronglyMeasurable.of_trim, MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_le, Topology.IsEmbedding.aestronglyMeasurable_comp_iff, aestronglyMeasurable_condExpIndSMul, L1.aestronglyMeasurable_coeFn, AEStronglyMeasurable.comp_snd_iff, AEStronglyMeasurable.const_vadd', Finset.aestronglyMeasurable_sum, AEStronglyMeasurable.comp_fst, ProbabilityTheory.HasSubgaussianMGF.aestronglyMeasurable, Lp.simpleFunc.aestronglyMeasurable, aestronglyMeasurable_iff_nullMeasurable_separable, ContinuousMapZero.aeStronglyMeasurable_mkD_restrict_of_uncurry, MemLp.aestronglyMeasurable, SimpleFunc.aestronglyMeasurable, aestronglyMeasurable_iff_aemeasurable, AEStronglyMeasurable.integral_condDistrib, ContinuousMap.aeStronglyMeasurable_mkD_of_uncurry, AEStronglyMeasurable.integral_kernel_compProd, AEEqFun.aestronglyMeasurable, AEStronglyMeasurable.integral_kernel_comp, ProbabilityTheory.aestronglyMeasurable_exp_mul_add, aestronglyMeasurable_const_smul_iff₀, aestronglyMeasurable_union_iff, AEStronglyMeasurable.comp_fst_iff, IntervalIntegrable.aestronglyMeasurable_restrict_uIoc, ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_aestronglyMeasurable, AEStronglyMeasurable.prodMk_left, aestronglyMeasurable_of_aestronglyMeasurable_trim, ContinuousMapZero.aeStronglyMeasurable_restrict_mkD_of_uncurry, AEStronglyMeasurable.const_nsmul, AEStronglyMeasurable.sup, AEStronglyMeasurable.const_smul', Multiset.aestronglyMeasurable_prod, AEStronglyMeasurable.comp_snd_map_prodMk, memLp_zero_iff_aestronglyMeasurable, AEStronglyMeasurable.mono, Continuous.aestronglyMeasurable, AEStronglyMeasurable.snd, AEStronglyMeasurable.convolution_integrand', ProbabilityTheory.IsAEKolmogorovProcess.aestronglyMeasurable_edist, AEStronglyMeasurable.inf, AECover.aestronglyMeasurable, AEStronglyMeasurable.convolution_integrand, AEStronglyMeasurable.smul, ProbabilityTheory.Kernel.HasSubgaussianMGF.aestronglyMeasurable, AEStronglyMeasurable.mul, aestronglyMeasurable_deriv_with_param, aestronglyMeasurable_zero, LocallyIntegrableOn.aestronglyMeasurable, memLp_trim_of_mem_lpMeasSubgroup, AEStronglyMeasurable.iUnion, AEStronglyMeasurable.comp_snd, AEStronglyMeasurable.convolution_integrand_swap_snd, AEEqFun.quot_mk_eq_mk, aestronglyMeasurable_one, ProbabilityTheory.aestronglyMeasurable_integral_condExpKernel, aestronglyMeasurable_indicator_iff, ContinuousOn.aestronglyMeasurable_of_isSeparable, aestronglyMeasurable_withDensity_iff, AEStronglyMeasurable.convolution_integrand_snd, MemLp.eLpNorm_mk_lt_top, AEStronglyMeasurable.of_comp_snd, AEStronglyMeasurable.add_iff_right, Multiset.aestronglyMeasurable_fun_sum, LocallyIntegrable.aestronglyMeasurable, AEStronglyMeasurable.apply_continuousLinearMap, lpMeas.aestronglyMeasurable, Finset.aestronglyMeasurable_fun_prod, Continuous.comp_aestronglyMeasurable₂, TendstoInMeasure.aestronglyMeasurable, AEStronglyMeasurable.aestronglyMeasurable_uIoc_iff
«termAEStronglyMeasurable[_]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aefinStronglyMeasurable_iff_aemeasurable 📖	mathematical	—	AEFinStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup AEMeasurable	—	Measure.instOuterMeasureClass
aefinStronglyMeasurable_of_aemeasurable 📖	mathematical	AEMeasurable	AEFinStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	aefinStronglyMeasurable_iff_aemeasurable
aefinStronglyMeasurable_zero 📖	mathematical	—	AEFinStronglyMeasurable Pi.instZero	—	Measure.instOuterMeasureClass finStronglyMeasurable_zero Filter.EventuallyEq.rfl
aestronglyMeasurable_const 📖	mathematical	—	AEStronglyMeasurable	—	StronglyMeasurable.aestronglyMeasurable stronglyMeasurable_const
aestronglyMeasurable_one 📖	mathematical	—	AEStronglyMeasurable Pi.instOne	—	StronglyMeasurable.aestronglyMeasurable stronglyMeasurable_one
aestronglyMeasurable_zero 📖	mathematical	—	AEStronglyMeasurable Pi.instZero	—	StronglyMeasurable.aestronglyMeasurable stronglyMeasurable_zero
aestronglyMeasurable_zero_measure 📖	mathematical	—	AEStronglyMeasurable Measure Measure.instZero	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Measure.instOuterMeasureClass Nontrivial.to_nonempty stronglyMeasurable_const

MeasureTheory.AEFinStronglyMeasurable

Definitions

Name	Category	Theorems
mk 📖	CompOp	—
sigmaFiniteSet 📖	CompOp	3 math math: measurableSet, ae_eq_zero_compl, sigmaFinite_restrict

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	MeasureTheory.AEFinStronglyMeasurable AddZero.toZero AddZeroClass.toAddZero	MeasureTheory.AEFinStronglyMeasurable AddZero.toZero AddZeroClass.toAddZero Pi.instAdd AddZero.toAdd	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.FinStronglyMeasurable.add Filter.EventuallyEq.add
ae_eq_mk 📖	mathematical	MeasureTheory.AEFinStronglyMeasurable	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass
ae_eq_zero_compl 📖	mathematical	MeasureTheory.AEFinStronglyMeasurable	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict Compl.compl Set Set.instCompl sigmaFiniteSet Pi.instZero	—	MeasureTheory.Measure.instOuterMeasureClass exists_set_sigmaFinite
aemeasurable 📖	mathematical	MeasureTheory.AEFinStronglyMeasurable	AEMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.FinStronglyMeasurable.measurable
const_smul 📖	mathematical	MeasureTheory.AEFinStronglyMeasurable	MeasureTheory.AEFinStronglyMeasurable Function.hasSMul SMulZeroClass.toSMul	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.FinStronglyMeasurable.const_smul Filter.EventuallyEq.const_smul
exists_set_sigmaFinite 📖	mathematical	MeasureTheory.AEFinStronglyMeasurable	Set MeasurableSet Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict Compl.compl Set.instCompl Pi.instZero MeasureTheory.SigmaFinite	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.FinStronglyMeasurable.exists_set_sigmaFinite Filter.EventuallyEq.trans MeasureTheory.ae_restrict_of_ae Filter.EventuallyEq.eq_1 MeasureTheory.ae_restrict_iff' MeasurableSet.compl Filter.Eventually.of_forall
finStronglyMeasurable_mk 📖	mathematical	MeasureTheory.AEFinStronglyMeasurable	MeasureTheory.FinStronglyMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass
inf 📖	mathematical	MeasureTheory.AEFinStronglyMeasurable	MeasureTheory.AEFinStronglyMeasurable Pi.instMinForall_mathlib SemilatticeInf.toMin	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.FinStronglyMeasurable.inf Filter.EventuallyEq.inf
measurableSet 📖	mathematical	MeasureTheory.AEFinStronglyMeasurable	MeasurableSet sigmaFiniteSet	—	MeasureTheory.Measure.instOuterMeasureClass exists_set_sigmaFinite
mul 📖	mathematical	MeasureTheory.AEFinStronglyMeasurable MulZeroClass.toZero	MeasureTheory.AEFinStronglyMeasurable MulZeroClass.toZero Pi.instMul MulZeroClass.toMul	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.FinStronglyMeasurable.mul Filter.EventuallyEq.mul
neg 📖	mathematical	MeasureTheory.AEFinStronglyMeasurable NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid	MeasureTheory.AEFinStronglyMeasurable NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid Pi.instNeg NegZeroClass.toNeg	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.FinStronglyMeasurable.neg Filter.EventuallyEq.neg
sigmaFinite_restrict 📖	mathematical	MeasureTheory.AEFinStronglyMeasurable	MeasureTheory.SigmaFinite MeasureTheory.Measure.restrict sigmaFiniteSet	—	MeasureTheory.Measure.instOuterMeasureClass exists_set_sigmaFinite
sub 📖	mathematical	MeasureTheory.AEFinStronglyMeasurable NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid	MeasureTheory.AEFinStronglyMeasurable NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid Pi.instSub SubNegMonoid.toSub SubtractionMonoid.toSubNegMonoid	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.FinStronglyMeasurable.sub Filter.EventuallyEq.sub
sup 📖	mathematical	MeasureTheory.AEFinStronglyMeasurable	MeasureTheory.AEFinStronglyMeasurable Pi.instMaxForall_mathlib SemilatticeSup.toMax	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.FinStronglyMeasurable.sup Filter.EventuallyEq.sup

MeasureTheory.AEStronglyMeasurable

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable Pi.instAdd	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.add Filter.EventuallyEq.add
add_const 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable	—	add MeasureTheory.aestronglyMeasurable_const
add_iff_left 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable Pi.instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	add_iff_right add_comm
add_iff_right 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable Pi.instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	add IsTopologicalAddGroup.toContinuousAdd neg IsTopologicalAddGroup.toContinuousNeg add_neg_cancel_comm
add_measure 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure MeasureTheory.Measure.instAdd	—	aestronglyMeasurable_add_measure_iff
ae_eq_mk 📖	mathematical	MeasureTheory.AEStronglyMeasurable	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass
ae_mem_imp_eq_mk 📖	mathematical	MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure.restrict	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.ae_imp_of_ae_restrict
aemeasurable 📖	mathematical	MeasureTheory.AEStronglyMeasurable	AEMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.measurable
aestronglyMeasurable_uIoc_iff 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure.restrict Set.uIoc Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Set.uIoc_eq_union aestronglyMeasurable_union_iff
comp_aemeasurable 📖	mathematical	MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure.map AEMeasurable	MeasureTheory.AEStronglyMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.comp_measurable Filter.EventuallyEq.trans MeasureTheory.ae_eq_comp Filter.EventuallyEq.fun_comp
comp_measurable 📖	mathematical	MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure.map Measurable	MeasureTheory.AEStronglyMeasurable	—	comp_aemeasurable Measurable.aemeasurable
comp_quasiMeasurePreserving 📖	mathematical	MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure.QuasiMeasurePreserving	MeasureTheory.AEStronglyMeasurable	—	comp_measurable mono_ac MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous MeasureTheory.Measure.QuasiMeasurePreserving.measurable
const_add 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable	—	add MeasureTheory.aestronglyMeasurable_const
const_mul 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable	—	mul MeasureTheory.aestronglyMeasurable_const
const_nsmul 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable Pi.instSMul AddMonoid.toNSMul	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.const_nsmul Filter.EventuallyEq.const_smul
const_smul 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable Function.hasSMul	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.const_smul Filter.EventuallyEq.const_smul
const_smul' 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable	—	const_smul
const_vadd 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable HVAdd.hVAdd instHVAdd Function.hasVAdd	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.const_vadd Filter.EventuallyEq.const_vadd
const_vadd' 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable HVAdd.hVAdd instHVAdd	—	const_vadd
dist 📖	mathematical	MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	MeasureTheory.AEStronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Dist.dist PseudoMetricSpace.toDist	—	Continuous.comp_aestronglyMeasurable continuous_dist prodMk
div 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable Pi.instDiv DivInvMonoid.toDiv Group.toDivInvMonoid	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.div' IsTopologicalGroup.to_continuousDiv Filter.EventuallyEq.div
div₀ 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable Pi.instDiv DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.div Filter.EventuallyEq.div
edist 📖	mathematical	MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	AEMeasurable ENNReal ENNReal.measurableSpace EDist.edist PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace	—	aemeasurable TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace ENNReal.instMetrizableSpace ENNReal.borelSpace Continuous.comp_aestronglyMeasurable continuous_edist prodMk
enorm 📖	mathematical	MeasureTheory.AEStronglyMeasurable	AEMeasurable ENNReal ENNReal.measurableSpace ENorm.enorm ContinuousENorm.toENorm	—	aemeasurable TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace ENNReal.instMetrizableSpace ENNReal.borelSpace Continuous.comp_aestronglyMeasurable continuous_enorm
exists_stronglyMeasurable_range_subset 📖	mathematical	MeasureTheory.AEStronglyMeasurable MeasurableSet Set.Nonempty Filter.Eventually Set Set.instMembership MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.StronglyMeasurable Set Set.instMembership Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.piecewise MeasureTheory.StronglyMeasurable.measurable MeasureTheory.stronglyMeasurable_const Set.range_subset_iff Set.range_piecewise Set.instReflSubset Set.Nonempty.some_mem Filter.EventuallyEq.trans Filter.mp_mem Filter.univ_mem' Set.piecewise_eq_of_mem
fst 📖	mathematical	MeasureTheory.AEStronglyMeasurable instTopologicalSpaceProd	MeasureTheory.AEStronglyMeasurable	—	Continuous.comp_aestronglyMeasurable continuous_fst
iUnion 📖	mathematical	MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure.restrict	MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure.restrict Set.iUnion	—	mono_measure sum_measure MeasureTheory.Measure.restrict_iUnion_le
indicator 📖	mathematical	MeasureTheory.AEStronglyMeasurable MeasurableSet	MeasureTheory.AEStronglyMeasurable Set.indicator	—	aestronglyMeasurable_indicator_iff restrict
indicator₀ 📖	mathematical	MeasureTheory.AEStronglyMeasurable MeasureTheory.NullMeasurableSet	MeasureTheory.AEStronglyMeasurable Set.indicator	—	aestronglyMeasurable_indicator_iff₀ restrict
inf 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable Pi.instMinForall_mathlib SemilatticeInf.toMin	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.inf Filter.EventuallyEq.inf
inv 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable Pi.instInv	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.inv Filter.EventuallyEq.inv
isSeparable_ae_range 📖	mathematical	MeasureTheory.AEStronglyMeasurable	Set TopologicalSpace.IsSeparable Filter.Eventually Set.instMembership MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.isSeparable_range Filter.mp_mem Filter.univ_mem'
measurable_mk 📖	mathematical	MeasureTheory.AEStronglyMeasurable	Measurable	—	MeasureTheory.StronglyMeasurable.measurable
mono 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.mono
mono_ac 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.AbsolutelyContinuous.ae_eq
mono_measure 📖	mathematical	MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder MeasureTheory.Measure.instPartialOrder	MeasureTheory.AEStronglyMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass Filter.Eventually.filter_mono MeasureTheory.ae_mono
mono_set 📖	mathematical	Set Set.instHasSubset MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure.restrict	MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure.restrict	—	mono_measure MeasureTheory.Measure.restrict_mono le_rfl
mul 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable Pi.instMul	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.mul Filter.EventuallyEq.mul
mul_const 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable	—	mul MeasureTheory.aestronglyMeasurable_const
mul_iff_left 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable Pi.instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	—	mul_iff_right mul_comm
mul_iff_right 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable Pi.instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	—	mul IsTopologicalGroup.toContinuousMul inv IsTopologicalGroup.toContinuousInv mul_inv_cancel_comm
neg 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable Pi.instNeg	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.neg Filter.EventuallyEq.neg
nnnorm 📖	mathematical	MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	MeasureTheory.AEStronglyMeasurable NNReal NNReal.instTopologicalSpace NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup	—	Continuous.comp_aestronglyMeasurable continuous_nnnorm
norm 📖	mathematical	MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	MeasureTheory.AEStronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm SeminormedAddCommGroup.toNorm	—	Continuous.comp_aestronglyMeasurable continuous_norm
nullMeasurableSet_eq_fun 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.NullMeasurableSet setOf	—	MeasureTheory.NullMeasurableSet.congr MeasurableSet.nullMeasurableSet MeasureTheory.StronglyMeasurable.measurableSet_eq_fun Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass Filter.univ_mem'
nullMeasurableSet_le 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.NullMeasurableSet setOf Preorder.toLE	—	MeasureTheory.NullMeasurableSet.congr MeasurableSet.nullMeasurableSet MeasureTheory.StronglyMeasurable.measurableSet_le Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass Filter.univ_mem'
nullMeasurableSet_lt 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.NullMeasurableSet setOf Preorder.toLT	—	MeasureTheory.NullMeasurableSet.congr MeasurableSet.nullMeasurableSet MeasureTheory.StronglyMeasurable.measurableSet_lt Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass Filter.univ_mem'
nullMeasurableSet_mulSupport 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.NullMeasurableSet Function.mulSupport	—	MeasureTheory.NullMeasurableSet.compl nullMeasurableSet_eq_fun MeasureTheory.StronglyMeasurable.aestronglyMeasurable MeasureTheory.stronglyMeasurable_const
nullMeasurableSet_support 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.NullMeasurableSet Function.support	—	MeasureTheory.NullMeasurableSet.compl nullMeasurableSet_eq_fun MeasureTheory.StronglyMeasurable.aestronglyMeasurable MeasureTheory.stronglyMeasurable_const
of_discrete 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable	—	MeasureTheory.StronglyMeasurable.aestronglyMeasurable MeasureTheory.StronglyMeasurable.of_discrete
of_measurableSpace_le_on 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet Set Set.instInter MeasureTheory.AEStronglyMeasurable Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict Compl.compl Set.instCompl Pi.instZero	MeasureTheory.AEStronglyMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyEq.trans Filter.mp_mem Filter.univ_mem' Set.indicator_of_mem Set.indicator_of_notMem indicator_ae_eq_of_restrict_compl_ae_eq_zero MeasureTheory.StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on MeasureTheory.StronglyMeasurable.indicator congr MeasureTheory.StronglyMeasurable.aestronglyMeasurable
of_subsingleton_cod 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable	—	MeasureTheory.StronglyMeasurable.aestronglyMeasurable MeasureTheory.StronglyMeasurable.of_subsingleton_cod
of_subsingleton_dom 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable	—	MeasureTheory.StronglyMeasurable.aestronglyMeasurable MeasureTheory.StronglyMeasurable.of_subsingleton_dom
of_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure.trim	MeasureTheory.AEStronglyMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_eq_of_ae_eq_trim
piecewise 📖	mathematical	MeasurableSet MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure.restrict Compl.compl Set Set.instCompl	MeasureTheory.AEStronglyMeasurable Set.piecewise	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.piecewise MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl MeasureTheory.ae_restrict_iff' Filter.mp_mem Filter.EventuallyEq.eq_1 Filter.univ_mem' Set.piecewise_eq_of_mem MeasurableSet.compl Set.piecewise_eq_of_notMem Set.mem_compl_iff
pow 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable Pi.instPow Monoid.toPow	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.pow Filter.EventuallyEq.pow_const
prodMk 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable instTopologicalSpaceProd	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.prodMk Filter.EventuallyEq.prodMk
real_toNNReal 📖	mathematical	MeasureTheory.AEStronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	MeasureTheory.AEStronglyMeasurable NNReal NNReal.instTopologicalSpace Real.toNNReal	—	Continuous.comp_aestronglyMeasurable continuous_real_toNNReal
restrict 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure.restrict	—	mono_measure MeasureTheory.Measure.restrict_le_self
smul 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable	—	Continuous.comp_aestronglyMeasurable ContinuousSMul.continuous_smul prodMk
smul_const 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable	—	Continuous.comp_aestronglyMeasurable ContinuousSMul.continuous_smul prodMk MeasureTheory.aestronglyMeasurable_const
smul_measure 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure MeasureTheory.Measure.instSMul	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.ae_smul_measure
snd 📖	mathematical	MeasureTheory.AEStronglyMeasurable instTopologicalSpaceProd	MeasureTheory.AEStronglyMeasurable	—	Continuous.comp_aestronglyMeasurable continuous_snd
stronglyMeasurable_mk 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.StronglyMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass
sub 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.sub IsTopologicalAddGroup.to_continuousSub Filter.EventuallyEq.sub
sum_measure 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure.sum	—	MeasureTheory.Measure.instOuterMeasureClass aestronglyMeasurable_iff_aemeasurable_separable AEMeasurable.sum_measure aemeasurable TopologicalSpace.IsSeparable.iUnion MeasureTheory.Measure.ae_sum_eq Filter.mp_mem Filter.univ_mem'
sup 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable Pi.instMaxForall_mathlib SemilatticeSup.toMax	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.sup Filter.EventuallyEq.sup
vadd 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable HVAdd.hVAdd instHVAdd	—	Continuous.comp_aestronglyMeasurable ContinuousVAdd.continuous_vadd prodMk
vadd_const 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable HVAdd.hVAdd instHVAdd	—	Continuous.comp_aestronglyMeasurable ContinuousVAdd.continuous_vadd prodMk MeasureTheory.aestronglyMeasurable_const

MeasureTheory.FinStronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aefinStronglyMeasurable 📖	mathematical	MeasureTheory.FinStronglyMeasurable	MeasureTheory.AEFinStronglyMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_eq_refl

MeasureTheory.SimpleFunc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aestronglyMeasurable 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable DFunLike.coe MeasureTheory.SimpleFunc instFunLike	—	MeasureTheory.StronglyMeasurable.aestronglyMeasurable stronglyMeasurable

MeasureTheory.StronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aestronglyMeasurable 📖	mathematical	MeasureTheory.StronglyMeasurable	MeasureTheory.AEStronglyMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyEq.refl

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aestronglyMeasurable_fun_prod 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable prod map	—	aestronglyMeasurable_prod
aestronglyMeasurable_fun_sum 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable sum map	—	Pi.multiset_sum_apply aestronglyMeasurable_sum
aestronglyMeasurable_prod 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable prod Pi.commMonoid	—	List.aestronglyMeasurable_prod
aestronglyMeasurable_sum 📖	mathematical	MeasureTheory.AEStronglyMeasurable	MeasureTheory.AEStronglyMeasurable sum Pi.addCommMonoid	—	List.aestronglyMeasurable_sum mem_coe

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aestronglyMeasurable_comp_iff 📖	mathematical	Topology.IsEmbedding	MeasureTheory.AEStronglyMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass aestronglyMeasurable_iff_aemeasurable_separable Set.mem_range_self codRestrict Function.Surjective.range_eq Set.rangeFactorization_surjective isClosed_univ MeasureTheory.AEStronglyMeasurable.aemeasurable MeasurableEmbedding.aemeasurable_comp_iff Topology.IsClosedEmbedding.measurableEmbedding Subtype.borelSpace isSeparable_preimage Continuous.comp_aestronglyMeasurable continuous

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aestronglyMeasurable_add_measure_iff 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure MeasureTheory.Measure.instAdd	—	MeasureTheory.Measure.sum_cond aestronglyMeasurable_sum_measure_iff Bool.countable
aestronglyMeasurable_congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.AEStronglyMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEStronglyMeasurable.congr Filter.EventuallyEq.symm
aestronglyMeasurable_const_smul_iff 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	inv_smul_smul MeasureTheory.AEStronglyMeasurable.const_smul' MeasureTheory.AEStronglyMeasurable.const_smul
aestronglyMeasurable_const_smul_iff₀ 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction	—	IsUnit.aestronglyMeasurable_const_smul_iff
aestronglyMeasurable_iUnion_iff 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure.restrict Set.iUnion	—	MeasureTheory.AEStronglyMeasurable.mono_measure MeasureTheory.Measure.restrict_mono Set.subset_iUnion le_rfl MeasureTheory.AEStronglyMeasurable.iUnion
aestronglyMeasurable_id 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable	—	AEMeasurable.aestronglyMeasurable aemeasurable_id
aestronglyMeasurable_iff_aemeasurable 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable AEMeasurable	—	MeasureTheory.AEStronglyMeasurable.aemeasurable AEMeasurable.aestronglyMeasurable BorelSpace.opensMeasurable
aestronglyMeasurable_iff_aemeasurable_separable 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable AEMeasurable Set TopologicalSpace.IsSeparable Filter.Eventually Set.instMembership MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEStronglyMeasurable.aemeasurable MeasureTheory.AEStronglyMeasurable.isSeparable_ae_range Set.eq_empty_or_nonempty MeasureTheory.aestronglyMeasurable_zero_measure AEMeasurable.exists_ae_eq_range_subset stronglyMeasurable_iff_measurable_separable TopologicalSpace.IsSeparable.mono
aestronglyMeasurable_iff_nullMeasurable_separable 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable MeasureTheory.NullMeasurable Set TopologicalSpace.IsSeparable Filter.Eventually Set.instMembership MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass aestronglyMeasurable_iff_aemeasurable_separable TopologicalSpace.IsSeparable.secondCountableTopology AEMeasurable.nullMeasurable MeasureTheory.NullMeasurable.aemeasurable_of_aerange BorelSpace.countablyGenerated Subtype.borelSpace
aestronglyMeasurable_indicator_iff 📖	mathematical	MeasurableSet	MeasureTheory.AEStronglyMeasurable Set.indicator MeasureTheory.Measure.restrict	—	MeasureTheory.AEStronglyMeasurable.congr MeasureTheory.AEStronglyMeasurable.mono_measure MeasureTheory.Measure.restrict_le_self indicator_ae_eq_restrict MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.indicator Filter.EventuallyEq.trans Filter.EventuallyEq.symm indicator_ae_eq_restrict_compl MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl
aestronglyMeasurable_indicator_iff₀ 📖	mathematical	MeasureTheory.NullMeasurableSet	MeasureTheory.AEStronglyMeasurable Set.indicator MeasureTheory.Measure.restrict	—	aestronglyMeasurable_congr indicator_ae_eq_of_ae_eq_set MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq aestronglyMeasurable_indicator_iff MeasureTheory.measurableSet_toMeasurable MeasureTheory.Measure.restrict_congr_set
aestronglyMeasurable_of_aestronglyMeasurable_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure.trim	MeasureTheory.AEStronglyMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.mono MeasureTheory.ae_eq_of_ae_eq_trim
aestronglyMeasurable_of_tendsto_ae 📖	mathematical	MeasureTheory.AEStronglyMeasurable Filter.Eventually Filter.Tendsto nhds MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.AEStronglyMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass aestronglyMeasurable_iff_aemeasurable_separable aemeasurable_of_tendsto_metrizable_ae MeasureTheory.AEStronglyMeasurable.aemeasurable Filter.exists_seq_tendsto TopologicalSpace.IsSeparable.closure TopologicalSpace.IsSeparable.iUnion instCountableNat Filter.mp_mem MeasureTheory.ae_all_iff Filter.univ_mem' mem_closure_of_tendsto Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.comp Set.mem_iUnion_of_mem
aestronglyMeasurable_sum_measure_iff 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure.sum	—	MeasureTheory.AEStronglyMeasurable.mono_measure MeasureTheory.Measure.le_sum MeasureTheory.AEStronglyMeasurable.sum_measure
aestronglyMeasurable_union_iff 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure.restrict Set Set.instUnion	—	Set.union_eq_iUnion Bool.countable
exists_stronglyMeasurable_limit_of_tendsto_ae 📖	mathematical	MeasureTheory.AEStronglyMeasurable Filter.Eventually Filter.Tendsto Filter.atTop Nat.instPreorder nhds MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.StronglyMeasurable Filter.Eventually Filter.Tendsto Filter.atTop Nat.instPreorder nhds MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass measurable_limit_of_tendsto_metrizable_ae instCountableNat instIsCountablyGenerated_atTop OrderTopology.of_linearLocallyFinite instDiscreteTopologyNat TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace PseudoEMetricSpace.pseudoMetrizableSpace MeasureTheory.AEStronglyMeasurable.aemeasurable aestronglyMeasurable_of_tendsto_ae Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.mp_mem Filter.univ_mem'

---

← Back to Index