Commit 2021-03-15 22:29 bd386a8f

feat(measure_theory/outer_measure): golf, add lemmas (#6664)

• Union_of_tendsto_zero, Union_nat_of_monotone_of_tsum_ne_top, of_function_union_of_separated: supporting lemmas for the upcoming definition of the Hausdorff measure (and more generally metric outer measures).
• ext_nonempty, smul_supr, map_sup, map_supr, comap_supr, restrict_univ, restrict_empty, restrict_supr, map_comap, map_comap_le, map_comap_of_surjective, restrict_le_self, map_le_restrict_range, le_comap_map, comap_map, comap_top, top_apply', map_top, map_top_of_surjective: new API lemmas about map/comap/restrict and sup/supr/top;
• is_greatest_of_function, of_function_eq_Sup, comap_of_function, map_of_function_le, map_of_function, restrict_of_function, smul_of_function: new lemmas about of_function`;
• Inf_apply': a version of Inf_apply that assumes that another set is nonempty;
• infi_apply, infi_apply', binfi_apply, binfi_apply', map_infi_le, comap_infi, map_infi, map_infi_comap, map_binfi_comap, restrict_infi_restrict, restrict_infi, restrict_binfi: new lemmas about map/comap/restrict and Inf/infi;
• extend_congr: infi_congr_Prop specialized for extend; why this is not a congr lemma?
• le_induced_outer_measure: le_of_function for induced_outer_measure;
• trim_le_trim → trim_mono: rename, use monotone;
• exists_measurable_superset_forall_eq_trim: a version of exists_measurable_superset_eq_trim that works for countable families of measures;
• trim_binop, trim_op: new helper lemmas to golf trim_add etc;
• trim_sup, trim_supr: new lemmas about trim.
• map_mono, comap_mono, mono'', restrict_mono, trim_mono: @[mono] lemmas.