Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-21 13:22 5bb145ef

View on Github →

feat(topology/lebesgue_measure): add Lebesgue outer measure; show that the lower half open interval is measurable

Estimated changes

added theorem finset.prod_sdiff
added theorem inv_pos
added theorem inv_inv'
added theorem inv_one
modified theorem pow_ge_one_of_ge_one
added theorem pow_inv
added theorem pow_le_pow
added theorem pow_ne_zero
added theorem pow_nonneg
modified theorem pow_pos
modified theorem pow_succ'
added theorem finset.not_mem_upto
modified theorem finset.subset.refl
modified theorem finset.upto_succ
modified theorem finset.upto_zero
added theorem lt_max_iff
added theorem set.sdiff_subset_sdiff
added theorem set.subset_Union
added theorem lattice.sub_le_sub
added theorem Inf_lt_iff
added theorem ennreal.lt_add_right
added theorem ennreal.sum_of_real
added theorem ennreal.supr_add
added theorem infi_lt_iff
deleted theorem inv_inv'
deleted theorem inv_pos
added theorem add_div
added theorem filter.mem_at_top
added def Ico
added theorem Ico_eq_Ico_iff
added theorem Ico_eq_empty
added theorem Ico_eq_empty_iff
added theorem Ico_inter_Iio_eq
added theorem Ico_sdiff_Iio_eq
added theorem Ico_subset_Ico_iff
added def Iio
added theorem div_eq_mul_inv
added theorem exists_lt_of_nat
added theorem int_of_nat_eq_of_nat
added theorem is_sum_geometric
added theorem map_succ_at_top_eq
added theorem mul_add_one_le_pow
added theorem neg_inv
added def of_nat
added theorem of_nat_add
added theorem of_nat_bit0
added theorem of_nat_bit1
added theorem of_nat_le_of_nat
added theorem of_nat_le_of_nat_iff
added theorem of_nat_mul
added theorem of_nat_one
added theorem of_nat_sub
added theorem one_lt_inv
added theorem rat_coe_eq_of_nat
added theorem rat_of_nat_eq_of_nat
added theorem sum_geometric'
added theorem sum_geometric
added theorem zero_le_of_nat
added theorem mem_uniformity_dist
added theorem Inter_neg
added theorem Inter_pos
added theorem Inter_univ
added theorem Union_empty
added theorem Union_neg
added theorem Union_pos
added theorem classical.or_not
added theorem ennreal.add_infi
added theorem ennreal.infi_add
added theorem ennreal.infi_add_infi
added theorem ennreal.infi_sum
added theorem inv_lt_one
added theorem sdiff_empty
added theorem sdiff_eq:
added theorem union_sdiff_left
added theorem union_sdiff_right
modified theorem one_lt_two