Commit 2024-03-05 14:11 6b5dcd21

View on Github →

chore(MeasureTheory/Integral/SetIntegral): rename type variables (#11131) Rename measurable spaces \alpha and \beta to X and Y. Rename variables a : X and b : Y to x and y, respectively (and associated hypotheses as well).

Estimated changes

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

modified theorem ClosedEmbedding.set_integral_map

modified theorem ContinuousAt.integral_sub_linear_isLittleO_ae

modified theorem ContinuousLinearEquiv.integral_comp_comm

modified theorem ContinuousLinearMap.integral_apply

modified theorem ContinuousLinearMap.integral_comp_L1_comm

modified theorem ContinuousLinearMap.integral_comp_comm'

modified theorem ContinuousLinearMap.integral_comp_comm

modified theorem ContinuousLinearMap.set_integral_compLp

modified theorem ContinuousOn.integral_sub_linear_isLittleO_ae

modified theorem ContinuousWithinAt.integral_sub_linear_isLittleO_ae

modified theorem LinearIsometry.integral_comp_comm

modified theorem MeasurableEmbedding.set_integral_map

modified theorem MeasureTheory.Integrable.measure_le_integral

modified theorem MeasureTheory.Integrable.simpleFunc_mul'

modified theorem MeasureTheory.Integrable.simpleFunc_mul

modified def MeasureTheory.LpToLpRestrictCLM

modified theorem MeasureTheory.LpToLpRestrictCLM_coeFn

modified theorem MeasureTheory.Lp_toLp_restrict_add

modified theorem MeasureTheory.Lp_toLp_restrict_smul

modified theorem MeasureTheory.MeasurePreserving.set_integral_image_emb

modified theorem MeasureTheory.MeasurePreserving.set_integral_preimage_emb

modified theorem MeasureTheory.continuous_set_integral

modified theorem MeasureTheory.hasSum_integral_iUnion

modified theorem MeasureTheory.hasSum_integral_iUnion_ae

modified theorem MeasureTheory.integrableOn_iUnion_of_summable_integral_norm

modified theorem MeasureTheory.integrableOn_iUnion_of_summable_norm_restrict

modified theorem MeasureTheory.integrable_of_summable_norm_restrict

modified theorem MeasureTheory.integral_Icc_eq_integral_Ico'

modified theorem MeasureTheory.integral_Icc_eq_integral_Ico

modified theorem MeasureTheory.integral_Icc_eq_integral_Ioc'

modified theorem MeasureTheory.integral_Icc_eq_integral_Ioc

modified theorem MeasureTheory.integral_Icc_eq_integral_Ioo'

modified theorem MeasureTheory.integral_Icc_eq_integral_Ioo

modified theorem MeasureTheory.integral_Ici_eq_integral_Ioi'

modified theorem MeasureTheory.integral_Ici_eq_integral_Ioi

modified theorem MeasureTheory.integral_Ico_eq_integral_Ioo'

modified theorem MeasureTheory.integral_Ico_eq_integral_Ioo

modified theorem MeasureTheory.integral_Iic_eq_integral_Iio'

modified theorem MeasureTheory.integral_Iic_eq_integral_Iio

modified theorem MeasureTheory.integral_Ioc_eq_integral_Ioo'

modified theorem MeasureTheory.integral_Ioc_eq_integral_Ioo

modified theorem MeasureTheory.integral_finset_biUnion

modified theorem MeasureTheory.integral_fintype_iUnion

modified theorem MeasureTheory.integral_iUnion

modified theorem MeasureTheory.integral_iUnion_ae

modified theorem MeasureTheory.integral_indicator_const

modified theorem MeasureTheory.integral_indicator_one

modified theorem MeasureTheory.integral_le_measure

modified theorem MeasureTheory.integral_norm_eq_pos_sub_neg

modified theorem MeasureTheory.integral_union_eq_left_of_forall

modified theorem MeasureTheory.integral_union_eq_left_of_forall₀

modified theorem MeasureTheory.norm_Lp_toLp_restrict_le

modified theorem MeasureTheory.ofReal_set_integral_one

modified theorem MeasureTheory.ofReal_set_integral_one_of_measure_ne_top

modified theorem MeasureTheory.set_integral_eq_zero_iff_of_nonneg_ae

modified theorem MeasureTheory.set_integral_gt_gt

modified theorem MeasureTheory.set_integral_le_nonneg

modified theorem MeasureTheory.set_integral_map

modified theorem MeasureTheory.set_integral_map_equiv

modified theorem MeasureTheory.set_integral_mono

modified theorem MeasureTheory.set_integral_mono_ae

modified theorem MeasureTheory.set_integral_neg_eq_set_integral_nonpos

modified theorem MeasureTheory.set_integral_nonneg

modified theorem MeasureTheory.set_integral_nonneg_ae

modified theorem MeasureTheory.set_integral_nonneg_of_ae

modified theorem MeasureTheory.set_integral_nonneg_of_ae_restrict

modified theorem MeasureTheory.set_integral_nonpos

modified theorem MeasureTheory.set_integral_nonpos_ae

modified theorem MeasureTheory.set_integral_nonpos_le

modified theorem MeasureTheory.set_integral_nonpos_of_ae

modified theorem MeasureTheory.set_integral_nonpos_of_ae_restrict

modified theorem MeasureTheory.set_integral_pos_iff_support_of_nonneg_ae

modified theorem MeasureTheory.set_integral_trim

modified theorem fst_integral

modified theorem integral_coe_re_add_coe_im

modified theorem integral_conj

modified theorem integral_im

modified theorem integral_ofReal

modified theorem integral_pair

modified theorem integral_re

modified theorem integral_re_add_im

modified theorem integral_withDensity_eq_integral_smul

modified theorem integral_withDensity_eq_integral_smul₀

modified theorem measure_le_lintegral_thickenedIndicator

modified theorem measure_le_lintegral_thickenedIndicatorAux

modified theorem set_integral_re_add_im

modified theorem set_integral_withDensity_eq_set_integral_smul

modified theorem set_integral_withDensity_eq_set_integral_smul₀'

modified theorem set_integral_withDensity_eq_set_integral_smul₀

modified theorem snd_integral

modified theorem swap_integral

Modified Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean