Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-02 21:38 1b1ad15c

View on Github →

refactor(measure_theory/*): rename is_(null_)?measurable to (null_)?measurable_set (#6001) Search & replace:

is_null_measurable → null_measurable;
is_measurable → measurable_set';
measurable_set_set → measurable_set;
measurable_set_spanning_sets → measurable_spanning_sets;
measurable_set_superset → measurable_superset.

Estimated changes

Modified src/analysis/calculus/fderiv_measurable.lean

deleted theorem is_measurable_set_of_differentiable_at

deleted theorem is_measurable_set_of_differentiable_at_of_is_complete

added theorem measurable_set_of_differentiable_at

added theorem measurable_set_of_differentiable_at_of_is_complete

Modified src/analysis/special_functions/pow.lean

Modified src/measure_theory/ae_measurable_sequence.lean

deleted theorem ae_seq.ae_seq_set_is_measurable

added theorem ae_seq.ae_seq_set_measurable_set

Modified src/measure_theory/bochner_integration.lean

Modified src/measure_theory/borel_space.lean

deleted theorem is_Gδ.is_measurable

added theorem is_Gδ.measurable_set

deleted theorem is_closed.is_measurable

added theorem is_closed.measurable_set

deleted theorem is_compact.is_measurable

added theorem is_compact.measurable_set

deleted theorem is_measurable.nhds_within_is_measurably_generated

deleted theorem is_measurable_Icc

deleted theorem is_measurable_Ici

deleted theorem is_measurable_Ico

deleted theorem is_measurable_Iic

deleted theorem is_measurable_Iio

deleted theorem is_measurable_Ioc

deleted theorem is_measurable_Ioi

deleted theorem is_measurable_Ioo

deleted theorem is_measurable_ball

deleted theorem is_measurable_closed_ball

deleted theorem is_measurable_closure

deleted theorem is_measurable_eball

deleted theorem is_measurable_interior

deleted theorem is_measurable_interval

deleted theorem is_measurable_le'

deleted theorem is_measurable_le

deleted theorem is_measurable_lt'

deleted theorem is_measurable_lt

deleted theorem is_measurable_set_of_continuous_at

deleted theorem is_open.is_measurable

added theorem is_open.measurable_set

modified theorem measurable_of_Ici

modified theorem measurable_of_Iic

modified theorem measurable_of_Iio

modified theorem measurable_of_Ioi

modified theorem measurable_of_is_closed

modified theorem measurable_of_is_open

added theorem measurable_set.nhds_within_is_measurably_generated

added theorem measurable_set_Icc

added theorem measurable_set_Ici

added theorem measurable_set_Ico

added theorem measurable_set_Iic

added theorem measurable_set_Iio

added theorem measurable_set_Ioc

added theorem measurable_set_Ioi

added theorem measurable_set_Ioo

added theorem measurable_set_ball

added theorem measurable_set_closed_ball

added theorem measurable_set_closure

added theorem measurable_set_eball

added theorem measurable_set_interior

added theorem measurable_set_interval

added theorem measurable_set_le'

added theorem measurable_set_le

added theorem measurable_set_lt'

added theorem measurable_set_lt

added theorem measurable_set_of_continuous_at

Modified src/measure_theory/content.lean

Modified src/measure_theory/decomposition.lean

Modified src/measure_theory/giry_monad.lean

modified theorem measure_theory.measure.measurable_coe

Modified src/measure_theory/group.lean

modified theorem measure_theory.measure.inv_apply

Modified src/measure_theory/haar_measure.lean

modified theorem measure_theory.measure.haar_measure_apply

Modified src/measure_theory/integration.lean

modified theorem measure_theory.lintegral_Union

modified theorem measure_theory.lintegral_indicator

modified theorem measure_theory.simple_func.coe_piecewise

modified theorem measure_theory.simple_func.coe_restrict

deleted theorem measure_theory.simple_func.is_measurable_cut

deleted theorem measure_theory.simple_func.is_measurable_fiber

deleted theorem measure_theory.simple_func.is_measurable_preimage

added theorem measure_theory.simple_func.measurable_set_cut

added theorem measure_theory.simple_func.measurable_set_fiber

added theorem measure_theory.simple_func.measurable_set_preimage

modified theorem measure_theory.simple_func.mem_restrict_range

modified def measure_theory.simple_func.piecewise

modified theorem measure_theory.simple_func.piecewise_apply

modified theorem measure_theory.simple_func.piecewise_compl

modified theorem measure_theory.simple_func.piecewise_empty

modified theorem measure_theory.simple_func.piecewise_univ

modified theorem measure_theory.simple_func.restrict_apply

modified theorem measure_theory.simple_func.restrict_const_lintegral

modified theorem measure_theory.simple_func.restrict_lintegral

modified theorem measure_theory.simple_func.restrict_preimage

modified theorem measure_theory.simple_func.restrict_preimage_singleton

modified theorem measure_theory.with_density_apply

Modified src/measure_theory/interval_integral.lean

Modified src/measure_theory/lebesgue_measure.lean

Modified src/measure_theory/measurable_space.lean

deleted theorem finset.is_measurable_bInter

deleted theorem finset.is_measurable_bUnion

added theorem finset.measurable_set_bInter

added theorem finset.measurable_set_bUnion

deleted theorem is_countably_spanning_is_measurable

added theorem is_countably_spanning_measurable_set

deleted theorem is_measurable.Inter

deleted theorem is_measurable.Inter_Prop

deleted theorem is_measurable.Inter_fintype

deleted theorem is_measurable.Union

deleted theorem is_measurable.Union_Prop

deleted theorem is_measurable.Union_fintype

deleted theorem is_measurable.bInter

deleted theorem is_measurable.bUnion

deleted theorem is_measurable.bUnion_decode2

deleted theorem is_measurable.compl

deleted theorem is_measurable.compl_iff

deleted theorem is_measurable.congr

deleted theorem is_measurable.const

deleted theorem is_measurable.diff

deleted theorem is_measurable.disjointed

deleted theorem is_measurable.empty

deleted theorem is_measurable.inl_image

deleted theorem is_measurable.insert

deleted theorem is_measurable.inter

deleted theorem is_measurable.of_compl

deleted theorem is_measurable.pi

deleted theorem is_measurable.pi_fintype

deleted theorem is_measurable.pi_univ

deleted theorem is_measurable.prod

deleted theorem is_measurable.sInter

deleted theorem is_measurable.sUnion

deleted theorem is_measurable.subtype_image

deleted theorem is_measurable.tprod

deleted theorem is_measurable.union

deleted theorem is_measurable.univ

deleted def is_measurable

deleted theorem is_measurable_eq

deleted theorem is_measurable_inr_image

deleted theorem is_measurable_insert

deleted theorem is_measurable_pi

deleted theorem is_measurable_pi_of_nonempty

deleted theorem is_measurable_prod

deleted theorem is_measurable_prod_of_nonempty

deleted theorem is_measurable_range_inl

deleted theorem is_measurable_range_inr

deleted theorem is_measurable_swap_iff

modified theorem measurable_find_greatest

added theorem measurable_set.Inter

added theorem measurable_set.Inter_Prop

added theorem measurable_set.Inter_fintype

added theorem measurable_set.Union

added theorem measurable_set.Union_Prop

added theorem measurable_set.Union_fintype

added theorem measurable_set.bInter

added theorem measurable_set.bUnion

added theorem measurable_set.bUnion_decode2

added theorem measurable_set.compl

added theorem measurable_set.compl_iff

added theorem measurable_set.congr

added theorem measurable_set.const

added theorem measurable_set.diff

added theorem measurable_set.disjointed

added theorem measurable_set.empty

added theorem measurable_set.inl_image

added theorem measurable_set.insert

added theorem measurable_set.inter

added theorem measurable_set.of_compl

added theorem measurable_set.pi

added theorem measurable_set.pi_fintype

added theorem measurable_set.pi_univ

added theorem measurable_set.prod

added theorem measurable_set.sInter

added theorem measurable_set.sUnion

added theorem measurable_set.subtype_image

added theorem measurable_set.tprod

added theorem measurable_set.union

added theorem measurable_set.univ

added def measurable_set

added theorem measurable_set_eq

added theorem measurable_set_inr_image

added theorem measurable_set_insert

added theorem measurable_set_pi

added theorem measurable_set_pi_of_nonempty

added theorem measurable_set_prod

added theorem measurable_set_prod_of_nonempty

added theorem measurable_set_range_inl

added theorem measurable_set_range_inr

added theorem measurable_set_swap_iff

deleted theorem measurable_space.generate_from_is_measurable

added theorem measurable_space.generate_from_measurable_set

modified def measurable_space.gi_generate_from

deleted theorem measurable_space.is_measurable_Inf

deleted theorem measurable_space.is_measurable_Sup

deleted theorem measurable_space.is_measurable_bot_iff

deleted theorem measurable_space.is_measurable_generate_from

deleted theorem measurable_space.is_measurable_inf

deleted theorem measurable_space.is_measurable_infi

deleted theorem measurable_space.is_measurable_sup

deleted theorem measurable_space.is_measurable_supr

deleted theorem measurable_space.is_measurable_top

deleted theorem measurable_space.is_pi_system_is_measurable

added theorem measurable_space.is_pi_system_measurable_set

added theorem measurable_space.measurable_set_Inf

added theorem measurable_space.measurable_set_Sup

added theorem measurable_space.measurable_set_bot_iff

added theorem measurable_space.measurable_set_generate_from

added theorem measurable_space.measurable_set_inf

added theorem measurable_space.measurable_set_infi

added theorem measurable_space.measurable_set_sup

added theorem measurable_space.measurable_set_supr

added theorem measurable_space.measurable_set_top

modified theorem measurable_to_encodable

modified theorem measurable_to_nat

modified theorem nonempty_measurable_superset

deleted theorem set.finite.is_measurable

deleted theorem set.finite.is_measurable_bInter

deleted theorem set.finite.is_measurable_bUnion

deleted theorem set.finite.is_measurable_sInter

deleted theorem set.finite.is_measurable_sUnion

added theorem set.finite.measurable_set

added theorem set.finite.measurable_set_bInter

added theorem set.finite.measurable_set_bUnion

added theorem set.finite.measurable_set_sInter

added theorem set.finite.measurable_set_sUnion

deleted theorem subsingleton.is_measurable

added theorem subsingleton.measurable_set

Modified src/measure_theory/measure_space.lean

deleted theorem ae_measurable.is_null_measurable

added theorem ae_measurable.null_measurable_set

deleted theorem is_measurable.diff_null

deleted theorem is_measurable.is_null_measurable

deleted theorem is_null_measurable.Union_nat

deleted theorem is_null_measurable.compl

deleted theorem is_null_measurable.diff_null

deleted theorem is_null_measurable.union_null

deleted def is_null_measurable

deleted theorem is_null_measurable_iff

deleted theorem is_null_measurable_iff_ae

deleted theorem is_null_measurable_iff_sandwich

deleted theorem is_null_measurable_measure_eq

deleted theorem is_null_measurable_of_complete

added theorem measurable_set.diff_null

added theorem measurable_set.null_measurable_set

modified theorem measure_theory.ae_dirac_iff

modified theorem measure_theory.ae_eventually_not_mem

modified theorem measure_theory.ae_map_iff

modified theorem measure_theory.ae_restrict_eq

modified theorem measure_theory.ae_restrict_iff'

modified theorem measure_theory.ae_restrict_iff

deleted theorem measure_theory.exists_is_measurable_superset

deleted theorem measure_theory.exists_is_measurable_superset_iff_measure_eq_zero

deleted theorem measure_theory.exists_is_measurable_superset_of_null

added theorem measure_theory.exists_measurable_superset

added theorem measure_theory.exists_measurable_superset_iff_measure_eq_zero

added theorem measure_theory.exists_measurable_superset_of_null

deleted theorem measure_theory.is_measurable_spanning_sets

deleted theorem measure_theory.is_measurable_to_measurable

added theorem measure_theory.measurable_set_to_measurable

added theorem measure_theory.measurable_spanning_sets

modified theorem measure_theory.measure.Inf_apply

modified theorem measure_theory.measure.Inf_caratheodory

modified theorem measure_theory.measure.absolutely_continuous.mk

modified theorem measure_theory.measure.count_apply

modified theorem measure_theory.measure.dirac_apply'

modified theorem measure_theory.measure.ext

modified theorem measure_theory.measure.ext_iff

modified theorem measure_theory.measure.le_iff

modified theorem measure_theory.measure.lt_iff

modified theorem measure_theory.measure.map_apply

modified theorem measure_theory.measure.map_comap_subtype_coe

modified def measure_theory.measure.of_measurable

modified theorem measure_theory.measure.of_measurable_apply

modified theorem measure_theory.measure.restrict_Inf_eq_Inf_restrict

modified theorem measure_theory.measure.restrict_Union_congr

modified theorem measure_theory.measure.restrict_add_restrict_compl

modified theorem measure_theory.measure.restrict_apply

modified theorem measure_theory.measure.restrict_apply_eq_zero'

modified theorem measure_theory.measure.restrict_apply_eq_zero

modified theorem measure_theory.measure.restrict_compl_add_restrict

modified theorem measure_theory.measure.restrict_congr_meas

modified theorem measure_theory.measure.restrict_congr_mono

modified theorem measure_theory.measure.restrict_map

modified theorem measure_theory.measure.restrict_restrict

modified theorem measure_theory.measure.restrict_sUnion_congr

modified theorem measure_theory.measure.restrict_sum

modified theorem measure_theory.measure.restrict_to_outer_measure_eq_to_outer_measure_restrict

modified theorem measure_theory.measure.restrict_union

modified theorem measure_theory.measure.restrict_union_add_inter

modified theorem measure_theory.measure.restrict_union_apply

modified theorem measure_theory.measure.restrict_union_congr

modified theorem measure_theory.measure.sub_apply

modified theorem measure_theory.measure.sum_apply

modified theorem measure_theory.measure.supr_restrict_spanning_sets

modified theorem measure_theory.measure_Union_eq_supr

modified theorem measure_theory.measure_compl

modified theorem measure_theory.measure_diff

modified theorem measure_theory.measure_eq_extend

modified theorem measure_theory.measure_eq_infi

modified theorem measure_theory.measure_eq_inter_diff

modified theorem measure_theory.measure_limsup_eq_zero

modified theorem measure_theory.measure_union

modified theorem measure_theory.measure_union_add_inter

modified theorem measure_theory.mem_ae_dirac_iff

modified theorem measure_theory.mem_ae_map_iff

modified theorem measure_theory.self_mem_ae_restrict

modified theorem measure_theory.sum_measure_le_measure_univ

modified theorem measure_theory.tendsto_measure_Union

modified theorem measure_theory.tsum_measure_le_measure_univ

deleted theorem null_is_null_measurable

added theorem null_measurable_set.Union_nat

added theorem null_measurable_set.compl

added theorem null_measurable_set.diff_null

added theorem null_measurable_set.union_null

added def null_measurable_set

added theorem null_measurable_set_iff

added theorem null_measurable_set_iff_ae

added theorem null_measurable_set_iff_sandwich

added theorem null_measurable_set_measure_eq

added theorem null_measurable_set_of_complete

added theorem null_null_measurable_set

deleted theorem restrict_apply_of_is_null_measurable

added theorem restrict_apply_of_null_measurable_set

Modified src/measure_theory/outer_measure.lean

modified theorem measure_theory.extend_mono

modified theorem measure_theory.induced_outer_measure_eq

modified theorem measure_theory.induced_outer_measure_eq_extend

deleted theorem measure_theory.outer_measure.exists_is_measurable_superset_eq_trim

deleted theorem measure_theory.outer_measure.exists_is_measurable_superset_of_trim_eq_zero

added theorem measure_theory.outer_measure.exists_measurable_superset_eq_trim

added theorem measure_theory.outer_measure.exists_measurable_superset_of_trim_eq_zero

modified theorem measure_theory.outer_measure.le_trim_iff

modified theorem measure_theory.outer_measure.restrict_trim

modified theorem measure_theory.outer_measure.trim_eq

modified theorem measure_theory.outer_measure.trim_eq_infi'

modified theorem measure_theory.outer_measure.trim_eq_infi

Modified src/measure_theory/pi.lean

modified theorem measure_theory.measure.pi_pi

Modified src/measure_theory/prod.lean

deleted theorem is_measurable_integrable

added theorem measurable_set_integrable

modified theorem measure_theory.measure.ae_measure_lt_top

modified theorem measure_theory.measure.prod_apply

modified theorem measure_theory.measure.prod_apply_symm

modified theorem measure_theory.measure.prod_restrict

Modified src/measure_theory/prod_group.lean

modified theorem measure_theory.measurable_measure_mul_right

modified theorem measure_theory.measure_inv_null

modified theorem measure_theory.measure_mul_right_ne_zero

modified theorem measure_theory.measure_mul_right_null

Modified src/measure_theory/set_integral.lean

modified theorem indicator_ae_eq_restrict

modified theorem indicator_ae_eq_restrict_compl

modified theorem measure_theory.ae_measurable_indicator_iff

modified theorem measure_theory.integrable_indicator_iff

modified theorem measure_theory.integrable_on.indicator

modified theorem measure_theory.integral_add_compl

modified theorem measure_theory.integral_indicator

modified theorem measure_theory.integral_indicator_const

modified theorem measure_theory.integral_union

modified theorem measure_theory.norm_set_integral_le_of_norm_le_const'

modified theorem measure_theory.norm_set_integral_le_of_norm_le_const_ae''

modified theorem measure_theory.set_integral_congr

modified theorem measure_theory.set_integral_congr_ae

modified theorem piecewise_ae_eq_restrict

modified theorem piecewise_ae_eq_restrict_compl

Modified src/measure_theory/simple_func_dense.lean

Modified src/probability_theory/independence.lean