Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-28 06:57 8159af67

View on Github →

feat(measure_theory/construction/borel_space): two measures are equal if they agree on closed-open intervals (#9396)

Estimated changes

deleted theorem borel_eq_generate_Iio
deleted theorem borel_eq_generate_Ioi
added theorem bsupr_measure_Iic
deleted theorem is_pi_system_Ioo
deleted theorem is_pi_system_Ioo_mem
added theorem is_pi_system_Icc
added theorem is_pi_system_Icc_mem
added theorem is_pi_system_Ico
added theorem is_pi_system_Ico_mem
added theorem is_pi_system_Iio
added theorem is_pi_system_Ioc
added theorem is_pi_system_Ioc_mem
added theorem is_pi_system_Ioi
added theorem is_pi_system_Ioo
added theorem is_pi_system_Ioo_mem
added theorem is_pi_system_Ixx
added theorem is_pi_system_Ixx_mem
added theorem is_pi_system_image_Iio
added theorem is_pi_system_image_Ioi
added theorem dense.exists_between
added theorem dense.exists_ge'
added theorem dense.exists_ge
added theorem dense.exists_gt
added theorem dense.exists_le'
added theorem dense.exists_le
added theorem dense.exists_lt
added theorem dense.order_dual