Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-28 18:16 7e7c6f58

View on Github →

feat(topology): various additions (preparation for the nonnegative integral)

Estimated changes

Modified data/set/countable.lean

Modified data/set/finite.lean

added theorem set.finite_prod

Modified data/set/prod.lean

added theorem set.empty_prod

added theorem set.insert_prod

added theorem set.prod_empty

added theorem set.prod_insert

Modified topology/borel_space.lean

modified theorem measure_theory.borel_prod

modified theorem measure_theory.measurable_add

modified theorem measure_theory.measurable_mul

modified theorem measure_theory.measurable_neg

modified theorem measure_theory.measurable_of_continuous2

modified theorem measure_theory.measurable_of_continuous

modified theorem measure_theory.measurable_sub

Modified topology/ennreal.lean

Modified topology/infinite_sum.lean

added theorem tsum_eq_single