Commit 2020-09-26 20:43 8600cb08

feat(measure_space): define sigma finite measures (#4265) They are defined as a Prop. The noncomputable "eliminator" is called spanning_sets, and satisfies monotonicity, even though that is not required to give a sigma_finite instance. I define a helper function accumulate s := ⋃ y ≤ x, s y. This is helpful, to separate out some monotonicity proofs. It is in its own file purely for import reasons (there is no good file to put it that imports both set.lattice and finset.basic, the latter is used in 1 lemma).