Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-07 15:31 6f75c57e

View on Github →

refactor(measure_theory/borel): borel is not an instance (#2326) Redo Borel spaces in a way similar to closed_order_topology/order_topology.

  • borel is no longer an instance;
  • define typeclass opens_measurable_space for a space with measurable_space and topological_space structures such that all open sets are measurable;
  • define typeclass borel_space for a space with measurable_space and topological_space structures such that measurable_space structure is equal to borel;
  • use dot syntax in more cases;
  • review some proofs that started to fail because of this change.

Estimated changes

modified def borel
deleted theorem borel_eq_subtype
deleted theorem borel_induced
deleted theorem borel_prod
deleted theorem borel_prod_le
added theorem continuous.measurable2
added theorem continuous.measurable
deleted theorem ennreal.measurable.add
deleted theorem ennreal.measurable.mul
deleted theorem ennreal.measurable.sub
added theorem finset.measurable_prod
modified theorem is_measurable_Icc
modified theorem is_measurable_Ici
modified theorem is_measurable_Iic
modified theorem is_measurable_Iio
modified theorem is_measurable_Ioi
modified theorem is_measurable_Ioo
modified theorem is_measurable_ball
added theorem is_measurable_eball
added theorem is_measurable_eq
modified theorem is_measurable_interior
modified theorem is_measurable_interval
added theorem is_measurable_le'
modified theorem is_measurable_le
deleted theorem is_measurable_of_is_open
added theorem is_open.is_measurable
deleted theorem measurable.add
deleted theorem measurable.coe_nnnorm
added theorem measurable.const_smul
modified theorem measurable.dist
modified theorem measurable.edist
added theorem measurable.ennnorm
added theorem measurable.ennreal_add
added theorem measurable.ennreal_coe
added theorem measurable.ennreal_mul
added theorem measurable.ennreal_sub
deleted theorem measurable.infi
modified theorem measurable.infi_Prop
added theorem measurable.inv'
added theorem measurable.inv
modified theorem measurable.is_glb
modified theorem measurable.is_lub
modified theorem measurable.max
modified theorem measurable.min
modified theorem measurable.mul
deleted theorem measurable.neg
modified theorem measurable.nndist
modified theorem measurable.nnnorm
added theorem measurable.nnreal_coe
modified theorem measurable.norm
added theorem measurable.of_inv
deleted theorem measurable.smul'
modified theorem measurable.smul
modified theorem measurable.sub
added theorem measurable.sub_nnreal
deleted theorem measurable.supr
modified theorem measurable.supr_Prop
added theorem measurable_binfi
added theorem measurable_bsupr
deleted theorem measurable_coe_int_real
modified theorem measurable_dist
modified theorem measurable_edist
deleted theorem measurable_finset_sum
added theorem measurable_infi
added theorem measurable_inv'
added theorem measurable_inv
added theorem measurable_inv_iff
added theorem measurable_mul
deleted theorem measurable_neg_iff
modified theorem measurable_nndist
modified theorem measurable_nnnorm
modified theorem measurable_norm
deleted theorem measurable_of_continuous2
deleted theorem measurable_of_continuous
deleted theorem measurable_smul_iff
added theorem measurable_supr
deleted theorem nnreal.measurable.add
deleted theorem nnreal.measurable.mul
deleted theorem nnreal.measurable.sub
deleted theorem nnreal.measurable_of_real
added theorem prod_le_borel_prod
modified def measure_theory.l1
added theorem is_measurable.congr
added theorem is_measurable.of_compl
added theorem is_measurable.prod
deleted theorem is_measurable_set_prod
added theorem measurable.mono
added theorem measurable.subtype_coe
deleted theorem measurable.subtype_val
added theorem measurable_from_top
modified theorem integrable_on.add
modified theorem integrable_on.sub
modified theorem integrable_on.union
modified theorem measurable_on_singleton
added theorem monotone.map_infi2_le
added theorem monotone.map_infi_le
added theorem monotone.map_supr2_ge
added theorem monotone.map_supr_ge