Commit 2022-02-24 14:38 d011bf20

View on Github →

chore(measure_theory/function/uniform_integrable): replace ℕ by a type verifying enough assumptions (#12242) This PR does not generalize the results of the uniform_integrable file much, but using a generic type instead of ℕ makes clear where we need assumptions like encodable.

Estimated changes

Modified src/measure_theory/function/uniform_integrable.lean

modified theorem measure_theory.egorov.measure_inter_not_convergent_seq_eq_zero

modified theorem measure_theory.egorov.measure_not_convergent_seq_tendsto_zero

modified theorem measure_theory.egorov.mem_not_convergent_seq_iff

modified def measure_theory.egorov.not_convergent_seq

modified theorem measure_theory.egorov.not_convergent_seq_antitone

modified theorem measure_theory.egorov.not_convergent_seq_measurable_set