AEMeasurable

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

Statistics

Metric	Count
Definitions AEMeasurable	1
Theorems add_measure, ae_inf_principal_eq_mk, ae_mem_imp_eq_mk, comp_aemeasurable, comp_aemeasurable', comp_measurable, comp_quasiMeasurePreserving, exists_ae_eq_range_subset, exists_measurable_nonneg, fst, iUnion, indicator, indicator₀, map_add₀, map_map_of_aemeasurable, mono', mono_ac, mono_measure, mono_set, prodMk, restrict, smul_measure, snd, subtype_mk, sum_measure, aemeasurable_comp_iff, aemeasurable_map_iff, instSFiniteMap, map_mono_of_aemeasurable, map_sum, restrict_map_of_aemeasurable, aemeasurable, aemeasurable_of_aerange, aemeasurable, aemeasurable_Ioi_of_forall_Ioc, aemeasurable_add_measure_iff, aemeasurable_const', aemeasurable_iUnion_iff, aemeasurable_id'', aemeasurable_iff_measurable, aemeasurable_indicator_const_iff, aemeasurable_indicator_iff, aemeasurable_indicator_iff₀, aemeasurable_map_equiv_iff, aemeasurable_of_aemeasurable_trim, aemeasurable_of_map_neZero, aemeasurable_of_subsingleton_codomain, aemeasurable_one, aemeasurable_restrict_iff_comap_subtype, aemeasurable_restrict_of_measurable_subtype, aemeasurable_smul_measure_iff, aemeasurable_sum_measure_iff, aemeasurable_uIoc_iff, aemeasurable_union_iff, aemeasurable_zero, aemeasurable_zero_measure, nullMeasurableSet_eq_fun	57
Total	58

AEMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_measure 📖	mathematical	AEMeasurable	AEMeasurable MeasureTheory.Measure MeasureTheory.Measure.instAdd	—	aemeasurable_add_measure_iff
ae_inf_principal_eq_mk 📖	mathematical	AEMeasurable MeasureTheory.Measure.restrict	Filter.EventuallyEq Filter Filter.instInf MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Filter.principal MeasureTheory.Measure.restrict	—	MeasureTheory.le_ae_restrict
ae_mem_imp_eq_mk 📖	mathematical	AEMeasurable MeasureTheory.Measure.restrict	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.ae_imp_of_ae_restrict
comp_aemeasurable 📖	mathematical	AEMeasurable MeasureTheory.Measure.map	AEMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass Measurable.comp Filter.EventuallyEq.trans MeasureTheory.ae_eq_comp Filter.EventuallyEq.fun_comp
comp_aemeasurable' 📖	mathematical	AEMeasurable MeasureTheory.Measure.map	AEMeasurable	—	comp_aemeasurable
comp_measurable 📖	mathematical	AEMeasurable MeasureTheory.Measure.map Measurable	AEMeasurable	—	comp_aemeasurable Measurable.aemeasurable
comp_quasiMeasurePreserving 📖	mathematical	AEMeasurable MeasureTheory.Measure.QuasiMeasurePreserving	AEMeasurable	—	comp_measurable mono' MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous MeasureTheory.Measure.QuasiMeasurePreserving.measurable
exists_ae_eq_range_subset 📖	mathematical	AEMeasurable Filter.Eventually Set Set.instMembership MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.Nonempty	Measurable Set Set.instHasSubset Set.range Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass Measurable.piecewise MeasureTheory.measurableSet_toMeasurable measurable_const Set.piecewise_eq_of_mem Set.Nonempty.some_mem Set.piecewise_eq_of_notMem Mathlib.Tactic.Contrapose.contrapose₂ MeasureTheory.subset_toMeasurable MeasureTheory.measure_toMeasurable MeasureTheory.compl_mem_ae_iff compl_compl Filter.Eventually.and Filter.mp_mem Filter.univ_mem' Set.mem_compl_iff
exists_measurable_nonneg 📖	mathematical	AEMeasurable Filter.Eventually Preorder.toLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Measurable Pi.hasLe Preorder.toLE Pi.instZero Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass exists_ae_eq_range_subset le_rfl Set.mem_range_self
fst 📖	mathematical	AEMeasurable Prod.instMeasurableSpace	AEMeasurable	—	Measurable.comp_aemeasurable measurable_fst
iUnion 📖	mathematical	AEMeasurable MeasureTheory.Measure.restrict	AEMeasurable MeasureTheory.Measure.restrict Set.iUnion	—	mono_measure sum_measure MeasureTheory.Measure.restrict_iUnion_le
indicator 📖	mathematical	AEMeasurable MeasurableSet	AEMeasurable Set.indicator	—	aemeasurable_indicator_iff restrict
indicator₀ 📖	mathematical	AEMeasurable MeasureTheory.NullMeasurableSet	AEMeasurable Set.indicator	—	aemeasurable_indicator_iff₀ restrict
map_add₀ 📖	mathematical	AEMeasurable	MeasureTheory.Measure.map MeasureTheory.Measure MeasureTheory.Measure.instAdd	—	MeasureTheory.Measure.ext MeasureTheory.Measure.map_apply_of_aemeasurable
map_map_of_aemeasurable 📖	mathematical	AEMeasurable MeasureTheory.Measure.map	MeasureTheory.Measure.map	—	MeasureTheory.Measure.ext MeasureTheory.Measure.map_apply_of_aemeasurable MeasureTheory.Measure.map_apply₀ nullMeasurable comp_aemeasurable Set.preimage_comp
mono' 📖	mathematical	AEMeasurable MeasureTheory.Measure.AbsolutelyContinuous	AEMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass
mono_ac 📖	mathematical	AEMeasurable MeasureTheory.Measure.AbsolutelyContinuous	AEMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.AbsolutelyContinuous.ae_le
mono_measure 📖	mathematical	AEMeasurable MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder MeasureTheory.Measure.instPartialOrder	AEMeasurable	—	mono_ac LE.le.absolutelyContinuous
mono_set 📖	mathematical	Set Set.instHasSubset AEMeasurable MeasureTheory.Measure.restrict	AEMeasurable MeasureTheory.Measure.restrict	—	mono_measure MeasureTheory.Measure.restrict_mono le_rfl
prodMk 📖	mathematical	AEMeasurable	AEMeasurable Prod.instMeasurableSpace	—	MeasureTheory.Measure.instOuterMeasureClass Measurable.prodMk Filter.EventuallyEq.prodMk
restrict 📖	mathematical	AEMeasurable	AEMeasurable MeasureTheory.Measure.restrict	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_restrict_of_ae
smul_measure 📖	mathematical	AEMeasurable	AEMeasurable MeasureTheory.Measure MeasureTheory.Measure.instSMul	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.ae_smul_measure
snd 📖	mathematical	AEMeasurable Prod.instMeasurableSpace	AEMeasurable	—	Measurable.comp_aemeasurable measurable_snd
subtype_mk 📖	mathematical	AEMeasurable Set Set.instMembership	AEMeasurable Set.Elem Subtype.instMeasurableSpace Set Set.instMembership Set.codRestrict	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim MeasureTheory.Measure.instOuterMeasureClass exists_ae_eq_range_subset Filter.Eventually.of_forall Nontrivial.to_nonempty Set.mem_range_self Filter.mp_mem Filter.univ_mem'
sum_measure 📖	mathematical	AEMeasurable	AEMeasurable MeasureTheory.Measure.sum	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim MeasureTheory.measure_toMeasurable MeasurableSet.iInter MeasureTheory.measurableSet_toMeasurable Mathlib.Tactic.Contrapose.contrapose₂ MeasureTheory.subset_toMeasurable Nontrivial.to_nonempty MeasureTheory.Measure.instOuterMeasureClass measurable_of_restrict_of_restrict_compl Set.restrict_piecewise measurable_const Set.restrict_piecewise_compl Set.compl_iInter MeasurableSet.iUnion MeasurableSet.inter MeasurableSet.compl Set.ext MeasureTheory.Measure.ae_sum_iff MeasureTheory.measure_mono_null Set.piecewise_eq_of_notMem Set.mem_iInter

MeasurableEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable_comp_iff 📖	mathematical	MeasurableEmbedding	AEMeasurable	—	Measurable.comp_aemeasurable measurable_rangeSplitting Set.mem_range_self Function.RightInverse.comp_eq_id Set.rightInverse_rangeSplitting injective measurable
aemeasurable_map_iff 📖	mathematical	MeasurableEmbedding	AEMeasurable MeasureTheory.Measure.map	—	AEMeasurable.comp_measurable measurable MeasureTheory.Measure.instOuterMeasureClass exists_measurable_extend ae_map_iff

MeasureTheory.Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSFiniteMap 📖	mathematical	—	MeasureTheory.SFinite map	—	MeasureTheory.sum_sfiniteSeq map_sum MeasureTheory.instSFiniteSumOfCountable instCountableNat MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite isFiniteMeasure_map MeasureTheory.isFiniteMeasure_sfiniteSeq map_of_not_aemeasurable MeasureTheory.instSFiniteOfNatMeasure
map_mono_of_aemeasurable 📖	mathematical	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder AEMeasurable	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder map	—	le_iff map_apply_of_aemeasurable AEMeasurable.mono_measure
map_sum 📖	mathematical	AEMeasurable sum	map sum	—	ext map_apply_of_aemeasurable sum_apply₀ AEMeasurable.nullMeasurable sum_apply AEMeasurable.mono_measure le_sum
restrict_map_of_aemeasurable 📖	mathematical	AEMeasurable MeasurableSet	restrict map Set.preimage	—	map_congr restrict_map MeasureTheory.ae_restrict_of_ae Filter.EventuallyEq.symm instOuterMeasureClass ext restrict_apply MeasureTheory.measure_congr Filter.EventuallyEq.inter Filter.EventuallyEq.refl Filter.EventuallyEq.preimage

MeasureTheory.NullMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable 📖	mathematical	MeasureTheory.NullMeasurable	AEMeasurable	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim MeasurableSpace.CountablyGenerated.isCountablyGenerated MeasureTheory.Measure.instOuterMeasureClass MeasurableSet.biUnion MeasurableSet.diff MeasureTheory.measure_biUnion_null_iff MeasureTheory.ae_le_set Filter.EventuallyEq.le Filter.EventuallyEq.trans Filter.EventuallyEq.symm Nontrivial.to_nonempty measurable_of_restrict_of_restrict_compl Set.restrict_piecewise measurable_const Set.restrict_piecewise_compl Set.restrict_eq measurable_generateFrom MeasurableSet.of_subtype_image Set.preimage_comp Subtype.image_preimage_coe Set.inter_comm Set.ext by_contra Set.mem_biUnion MeasureTheory.measure_mono_null not_imp_comm Set.piecewise_eq_of_notMem MeasureTheory.NullMeasurableSet.exists_measurable_superset_ae_eq Function.sometimes_spec MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq
aemeasurable_of_aerange 📖	mathematical	MeasureTheory.NullMeasurable Filter.Eventually Set Set.instMembership MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	AEMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass Set.eq_empty_or_nonempty aemeasurable_zero_measure AEMeasurable.exists_ae_eq_range_subset Measurable.aemeasurable measurable' MeasureTheory.Measure.ae_completion CanLift.prf Pi.canLift Subtype.canLift Set.range_subset_iff AEMeasurable.congr Measurable.comp_aemeasurable measurable_subtype_coe aemeasurable Filter.EventuallyEq.symm

Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable 📖	mathematical	—	AEMeasurable	—	Measurable.aemeasurable measurable

(root)

Definitions

Name	Category	Theorems
AEMeasurable 📖	MathDef	256 math math: AEMeasurable.csin, aemeasurable_of_re_im, Subsingleton.aemeasurable, AEMeasurable.congr, MeasureTheory.aemeasurable_withDensity_ennreal_iff', MeasureTheory.aefinStronglyMeasurable_iff_aemeasurable, aemeasurable_pi_lambda, AEMeasurable.const_smul, AEMeasurable.sup_const, AEMeasurable.pow_const, AEMeasurable.add_const, AEMeasurable.singularPart, AEMeasurable.isLUB, MeasureTheory.AEStronglyMeasurable.aemeasurable, AEMeasurable.ennreal_toNNReal, ProbabilityTheory.aemeasurable_of_mem_interior_integrableExpSet, aemeasurable_smul_const, AEMeasurable.add', AEMeasurable.of_map_ne_zero, Multiset.aemeasurable_sum, AEMeasurable.sinc, AEMeasurable.csinh, Measurable.comp_aemeasurable', AEMeasurable.pow, IsAddUnit.aemeasurable_const_vadd_iff, AEMeasurable.const_vadd, AEMeasurable.max, MeasureTheory.HasPDF.aemeasurable', Measurable.aemeasurable, MeasureTheory.aemeasurable_of_pdf_ne_zero, AEMeasurable.mabs, AEMeasurable.norm, MeasurableEmbedding.aemeasurable_comp_iff, AEMeasurable.iInf, AEMeasurable.add_iff_right, AEMeasurable.isGLB, AEMeasurable.im, AEMeasurable.enorm, aemeasurable_coe_nnreal_real_iff, MeasureTheory.Measure.aemeasurable_lintegral, aemeasurable_iff_measurable, AEMeasurable.add, MeasureTheory.hasPDF_iff, AEMeasurable.iUnion, aemeasurable_lineDeriv_uncurry, aemeasurable_zero, aemeasurable_pi_iff, AEMeasurable.comp_aemeasurable', IsUnit.aemeasurable_const_smul_iff, AEMeasurable.exp, AEMeasurable.comp_measurable, AEMeasurable.add_measure, aemeasurable_neg_iff, AEMeasurable.const_add, AEMeasurable.smul_const, List.aemeasurable_prod, AEMeasurable.const_sub, AEMeasurable.ae_of_bind, AEMeasurable.ccosh, AEMeasurable.comp_quasiMeasurePreserving, aemeasurable_restrict_iff_comap_subtype, Multiset.aemeasurable_prod, AEMeasurable.indicator, AEMeasurable.comp_snd, aestronglyMeasurable_iff_aemeasurable_separable, aemeasurable_deriv_with_param, AEMeasurable.smul, AEMeasurable.prod_swap, MeasureTheory.MeasurePreserving.aemeasurable_comp_iff, AEMeasurable.biInf, AEMeasurable.real_toNNReal, AEMeasurable.div_const, MeasureTheory.MeasurePreserving.aemeasurable, MeasureTheory.Measure.map_def, aemeasurable_of_tendsto_metrizable_ae', MeasureTheory.aemeasurable_ofReal_abs_det_fderivWithin, Finset.aemeasurable_fun_sum, AEMeasurable.const_inner, Multiset.aemeasurable_fun_prod, aemeasurable_inv_iff, MeasureTheory.TendstoInDistribution.forall_aemeasurable, MeasureTheory.aemeasurable_lconvolution, AEMeasurable.div', AEMeasurable.edist, ProbabilityTheory.Kernel.aemeasurable, AEMeasurable.lintegral_prod_left', ProbabilityTheory.IdentDistrib.aemeasurable_fst, AEMeasurable.const_inf, AEMeasurable.ae_of_join, AEMeasurable.mul_iff_right, MeasureTheory.TendstoInMeasure.aemeasurable, ProbabilityTheory.IsAEKolmogorovProcess.aemeasurable, AEMeasurable.sub', MeasureTheory.Integrable.aemeasurable, MeasureTheory.aemeasurable_fderivWithin, AEMeasurable.coe_nnreal_ennreal, Finset.aemeasurable_fun_prod, AEMeasurable.div, AEMeasurable.min, Finset.aemeasurable_prod, AEMeasurable.vadd_const, AEMeasurable.const_mul, MeasureTheory.NullMeasurable.aemeasurable_of_aerange, AEMeasurable.sum_measure, List.aemeasurable_fun_prod, AEMeasurable.lintegral_prod_left, AEMeasurable.sin, AEMeasurable.lintegral_prod_right', AEMeasurable.restrict, AEMeasurable.add_iff_left, AEMeasurable.inner, ProbabilityTheory.HasLaw.aemeasurable, AEMeasurable.mul_const, ProbabilityTheory.aemeasurable_of_integrable_exp_mul, AEMeasurable.mul, MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersets, AEMeasurable.neg, ProbabilityTheory.HasSubgaussianMGF.aemeasurable, AEMeasurable.log, aemeasurable_restrict_of_measurable_subtype, AEMeasurable.inner_const, Real.aemeasurable_of_aemeasurable_exp_mul, AEMeasurable.mul_iff_left, Real.hasPDF_iff, ENNReal.aemeasurable_of_exist_almost_disjoint_supersets, aemeasurable_uIoc_iff, MeasureTheory.AEFinStronglyMeasurable.aemeasurable, AEMeasurable.const_div, MeasureTheory.MemLp.aemeasurable, AEMeasurable.lintegral_prod_right, aemeasurable_id', Continuous.aemeasurable, AEMeasurable.snd, aemeasurable_const_vadd_iff, MeasureTheory.AECover.aemeasurable, AEMeasurable.cexp, aemeasurable_iUnion_iff, AEMeasurable.carg, AEMeasurable.apply_continuousLinearMap, List.aemeasurable_sum, aemeasurable_restrict_of_monotoneOn, AEMeasurable.mono_ac, AEMeasurable.sup', MeasureTheory.L1.aemeasurable_coeFn, AEMeasurable.indicator₀, aemeasurable_smul_measure_iff, AEMeasurable.const_pow, AEMeasurable.ereal_toENNReal, aemeasurable_lineDeriv, MeasureTheory.Measure.QuasiMeasurePreserving.aemeasurable, aemeasurable_withDensity_iff, AEMeasurable.prodMk, aemeasurable_union_iff, aemeasurable_deriv, AEMeasurable.mono_measure, AEMeasurable.fst, AEMeasurable.complex_ofReal, Multiset.aemeasurable_fun_sum, AEMeasurable.fun_const_smul, aemeasurable_sum_measure_iff, MeasureTheory.aemeasurable_withDensity_ennreal_iff, aemeasurable_of_unif_approx, AEMeasurable.ereal_toReal, AEMeasurable.mono_set, ENNReal.aemeasurable_of_tendsto', AEMeasurable.coe_ereal_ennreal, aemeasurable_congr, AEMeasurable.withDensity_rnDeriv, AEMeasurable.iSup, aemeasurable_map_equiv_iff, AEMeasurable.inf_const, MeasureTheory.TendstoInDistribution.aemeasurable_limit, ContinuousOn.aemeasurable, AEMeasurable.sinh, aemeasurable_zero_measure, AEMeasurable.nnnorm, AEMeasurable.biSup, MeasureTheory.aemeasurable_toNNReal_abs_det_fderivWithin, MeasureTheory.NullMeasurable.aemeasurable, MeasureTheory.AEStronglyMeasurable.enorm, MeasureTheory.SimpleFunc.aemeasurable, ProbabilityTheory.IdentDistrib.aemeasurable_snd, aemeasurable_const_smul_iff, aemeasurable_indicator_const_iff, ENNReal.aemeasurable_of_tendsto, AEMeasurable.ennreal_tsum, Measurable.comp_aemeasurable, AEMeasurable.ccos, AEMeasurable.ennreal_ofReal, AEMeasurable.sup, AEMeasurable.of_discrete, AEMeasurable.mul', aestronglyMeasurable_iff_aemeasurable, MeasureTheory.pdf.IsUniform.aemeasurable, aemeasurable_indicator_iff, MeasureTheory.AEEqFun.aemeasurable, MeasureTheory.HasPDF.aemeasurable, Continuous.aemeasurable2, ProbabilityTheory.IsGaussianProcess.aemeasurable, AEMeasurable.abs, AEMeasurable.re, aemeasurable_id, aemeasurable_one, aemeasurable_id'', aemeasurable_Ioi_of_forall_Ioc, aemeasurable_derivWithin_Ici, AEMeasurable.smul_measure, AEMeasurable.nnreal_tsum, AEMeasurable.fun_const_vadd, MeasureTheory.StronglyMeasurable.aemeasurable, ProbabilityTheory.IsAEKolmogorovProcess.aemeasurable_edist, AEMeasurable.sqrt, AEMeasurable.inv, AEMeasurable.eval, aemeasurable_of_subsingleton_codomain, Real.aemeasurable_of_aemeasurable_exp, aemeasurable_of_aemeasurable_trim, AEMeasurable.coe_nnreal_real, AEMeasurable.sub_const, AEMeasurable.cos, AEMeasurable.vadd, ProbabilityTheory.HasGaussianLaw.aemeasurable, aemeasurable_of_tendsto_metrizable_ae, aemeasurable_add_measure_iff, AEMeasurable.subtype_mk, AEMeasurable.sub, AEMeasurable.ennreal_toReal, ContinuousOn.aemeasurable₀, aemeasurable_of_map_neZero, aemeasurable_const', AEMeasurable.clog, aemeasurable_coe_nnreal_ennreal_iff, MeasureTheory.aemeasurable_dirac, AEMeasurable.inf', aemeasurable_restrict_of_antitoneOn, MeasureTheory.AEStronglyMeasurable.edist, AEMeasurable.inf, MeasureTheory.Measure.aemeasurable_bind, List.aemeasurable_fun_sum, Finset.aemeasurable_sum, MeasureTheory.Lp.simpleFunc.aemeasurable, AEMeasurable.dist, MeasureTheory.aemeasurable_mlconvolution, VitaliFamily.aemeasurable_limRatio, AEMeasurable.coe_real_ereal, AEMeasurable.cosh, aemeasurable_indicator_iff₀, IndexedPartition.aemeasurable_piecewise, aemeasurable_const_smul_iff₀, AEMeasurable.comp_fst, MeasurableEmbedding.aemeasurable_map_iff, AEMeasurable.comp_aemeasurable, AEMeasurable.const_sup, AEMeasurable.mono', aemeasurable_derivWithin_Ioi, aemeasurable_const

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable_Ioi_of_forall_Ioc 📖	mathematical	AEMeasurable MeasureTheory.Measure.restrict Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	AEMeasurable MeasureTheory.Measure.restrict Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Filter.exists_seq_tendsto Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Set.iUnion_Ioc_eq_Ioi_self_iff Filter.Eventually.exists instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.eventually Filter.eventually_ge_atTop aemeasurable_iUnion_iff instCountableNat lt_or_ge Set.Ioc_eq_empty not_lt MeasureTheory.Measure.restrict_empty aemeasurable_zero_measure
aemeasurable_add_measure_iff 📖	mathematical	—	AEMeasurable MeasureTheory.Measure MeasureTheory.Measure.instAdd	—	MeasureTheory.Measure.sum_cond aemeasurable_sum_measure_iff Bool.countable
aemeasurable_const' 📖	mathematical	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	AEMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass eq_or_ne aemeasurable_zero_measure Filter.Eventually.exists MeasureTheory.ae_neBot measurable_const Filter.EventuallyEq.symm
aemeasurable_iUnion_iff 📖	mathematical	—	AEMeasurable MeasureTheory.Measure.restrict Set.iUnion	—	AEMeasurable.mono_measure MeasureTheory.Measure.restrict_mono Set.subset_iUnion le_rfl AEMeasurable.iUnion
aemeasurable_id'' 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	AEMeasurable	—	Measurable.aemeasurable measurable_id''
aemeasurable_iff_measurable 📖	mathematical	—	AEMeasurable Measurable	—	MeasureTheory.NullMeasurable.measurable_of_complete AEMeasurable.nullMeasurable Measurable.aemeasurable
aemeasurable_indicator_const_iff 📖	mathematical	—	AEMeasurable Set.indicator MeasureTheory.NullMeasurableSet	—	Set.indicator_const_preimage_eq_union Set.union_empty AEMeasurable.nullMeasurable MeasurableSet.compl MeasurableSet.singleton aemeasurable_indicator_iff₀ aemeasurable_const
aemeasurable_indicator_iff 📖	mathematical	MeasurableSet	AEMeasurable Set.indicator MeasureTheory.Measure.restrict	—	AEMeasurable.congr AEMeasurable.mono_measure MeasureTheory.Measure.restrict_le_self indicator_ae_eq_restrict MeasureTheory.Measure.instOuterMeasureClass Measurable.indicator Filter.EventuallyEq.trans Filter.EventuallyEq.symm indicator_ae_eq_restrict_compl MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl
aemeasurable_indicator_iff₀ 📖	mathematical	MeasureTheory.NullMeasurableSet	AEMeasurable Set.indicator MeasureTheory.Measure.restrict	—	MeasureTheory.Measure.instOuterMeasureClass aemeasurable_congr indicator_ae_eq_of_ae_eq_set Filter.EventuallyEq.symm aemeasurable_indicator_iff MeasureTheory.Measure.restrict_congr_set
aemeasurable_map_equiv_iff 📖	mathematical	—	AEMeasurable MeasureTheory.Measure.map DFunLike.coe MeasurableEquiv EquivLike.toFunLike MeasurableEquiv.instEquivLike	—	MeasurableEmbedding.aemeasurable_map_iff MeasurableEquiv.measurableEmbedding
aemeasurable_of_aemeasurable_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE AEMeasurable MeasureTheory.Measure.trim	AEMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass Measurable.mono le_rfl MeasureTheory.ae_eq_of_ae_eq_trim
aemeasurable_of_map_neZero 📖	mathematical	—	AEMeasurable	—	MeasureTheory.Measure.map_of_not_aemeasurable
aemeasurable_of_subsingleton_codomain 📖	mathematical	—	AEMeasurable	—	Measurable.aemeasurable measurable_of_subsingleton_codomain
aemeasurable_one 📖	mathematical	—	AEMeasurable	—	Measurable.aemeasurable measurable_one
aemeasurable_restrict_iff_comap_subtype 📖	mathematical	MeasurableSet	AEMeasurable MeasureTheory.Measure.restrict Set.Elem Subtype.instMeasurableSpace Set Set.instMembership MeasureTheory.Measure.comap	—	map_comap_subtype_coe MeasurableEmbedding.aemeasurable_map_iff MeasurableEmbedding.subtype_coe
aemeasurable_restrict_of_measurable_subtype 📖	mathematical	MeasurableSet Measurable Set.Elem Subtype.instMeasurableSpace Set Set.instMembership	AEMeasurable MeasureTheory.Measure.restrict	—	aemeasurable_restrict_iff_comap_subtype Measurable.aemeasurable
aemeasurable_smul_measure_iff 📖	mathematical	—	AEMeasurable ENNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	IsScalarTower.right MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.ae_ennreal_smul_measure_iff
aemeasurable_sum_measure_iff 📖	mathematical	—	AEMeasurable MeasureTheory.Measure.sum	—	AEMeasurable.mono_measure MeasureTheory.Measure.le_sum AEMeasurable.sum_measure
aemeasurable_uIoc_iff 📖	mathematical	—	AEMeasurable MeasureTheory.Measure.restrict Set.uIoc Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Set.uIoc_eq_union aemeasurable_union_iff
aemeasurable_union_iff 📖	mathematical	—	AEMeasurable MeasureTheory.Measure.restrict Set Set.instUnion	—	Set.union_eq_iUnion Bool.countable
aemeasurable_zero 📖	mathematical	—	AEMeasurable	—	Measurable.aemeasurable measurable_zero
aemeasurable_zero_measure 📖	mathematical	—	AEMeasurable MeasureTheory.Measure MeasureTheory.Measure.instZero	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim MeasureTheory.Measure.instOuterMeasureClass Nontrivial.to_nonempty measurable_const
nullMeasurableSet_eq_fun 📖	mathematical	AEMeasurable	MeasureTheory.NullMeasurableSet setOf	—	AEMeasurable.nullMeasurableSet_preimage AEMeasurable.prodMk MeasurableEq.measurableSet_diagonal

---

← Back to Index