Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-30 13:54 d003c550

View on Github →

chore(analysis, measure_theory): Fix lint (#16216) Satisfy the fintype_finite and to_additive_doc linters. Further, perform the similar weakening from encodable to countable, even though that's not yet linted for. The advantage of this is that finite α → countable α in known to TC inference, while fintype α → encodable α is not (because it's noncanonical data). As a result, some lemmas that were proved for both fintype and encodable are now deduplicated.

Estimated changes

modified theorem unique_diff_on.pi
modified theorem unique_diff_on.univ_pi
modified theorem unique_diff_within_at.pi
modified theorem basis.exists_op_nnnorm_le
modified theorem basis.exists_op_norm_le
modified theorem set.countable_coe_iff
added theorem set.Inter_plift_down
added theorem set.Inter_plift_up
added theorem set.Union_plift_down
added theorem set.Union_plift_up
modified theorem submodule.supr_map_single
added theorem nonempty_encodable
deleted theorem finset.nonempty_encodable
modified theorem ae_measurable.ennreal_tsum
modified theorem ae_measurable.is_glb
modified theorem ae_measurable.is_lub
modified theorem ae_measurable_infi
modified theorem ae_measurable_supr
deleted theorem borel_eq_top_of_encodable
modified theorem measurable.ennreal_tsum'
modified theorem measurable.ennreal_tsum
modified theorem measurable.is_glb
modified theorem measurable.is_lub
modified theorem measurable.nnreal_tsum
modified theorem measurable_infi
modified theorem measurable_supr
modified theorem ae_seq.ae_seq_eq_fun_ae
modified theorem ae_seq.ae_seq_eq_mk_ae
modified theorem ae_seq.ae_seq_n_eq_fun_n_ae
modified theorem ae_seq.supr
modified theorem ennreal.ess_sup_liminf_le
added theorem measurable_of_finite
deleted theorem measurable_of_fintype
deleted theorem measurable_set.pi_fintype
modified theorem measurable_set.univ_pi
deleted theorem measurable_to_encodable
modified theorem measurable_set.Inter
deleted theorem measurable_set.Inter_Prop
modified theorem measurable_set.Union
deleted theorem measurable_set.Union_Prop
modified theorem ae_measurable.sum_measure
modified theorem ae_measurable_Union_iff
modified theorem measure_theory.ae_all_iff
deleted theorem measure_theory.ae_imp_iff
modified theorem measure_theory.extend_Union
added theorem infi_plift_down
added theorem infi_plift_up
added theorem supr_plift_down
added theorem supr_plift_up
modified theorem countable_Inter_mem
modified theorem countable_bInter_mem
modified theorem eventually_countable_ball
modified theorem eventually_countable_forall
modified theorem submodule.fg_pi
modified theorem submodule.fg_supr