Commit 2021-09-15 06:12 7492aa60

refactor(measure_theory/integral/lebesgue): golf a proof (#9206)

• add exists_pos_tsum_mul_lt_of_encodable;
• add measure.spanning_sets_index and lemmas about this definition;
• replace the proof of exists_integrable_pos_of_sigma_finite with a simpler one.