# Commit 2020-10-20 03:17 cd884eb8

View on Github →feat(measure_theory): finite_spanning_sets_in (#4668)

- We define a new Type-valued structure
`finite_spanning_sets_in`

which consists of a countable sequence of sets that span the type, have finite measure, and live in a specified collection of sets, `sigma_finite`

is redefined in terms of`finite_spanning_sets_in`

- One of the ext lemmas is now conveniently formulated in terms of
`finite_spanning_sets_in`

`finite_spanning_sets_in`

is also used to remove a little bit of code duplication in`prod`

(which occurred because`sigma_finite`

was a`Prop`

, and forgot the actual construction)- Define a predicate
`is_countably_spanning`

which states that a collection of sets has a countable spanning subset. This is useful for one particular lemma in`prod`

. - Generalize some lemmas about products in the case that the σ-algebras are generated by a collection of sets. This can be used to reason about iterated products.
- Prove
`prod_assoc_prod`

. - Cleanup in
`measurable_space`

and somewhat in`measure_space`

. - Rename
`measurable.sum_rec -> measurable.sum_elim`

(and give a different but definitionally equal statement)