proposition: Lemma outer_measure_sigma_subadditive_tail (T : Type) (R : realType) (mu : {outer_measure set T -> \bar R}) N (F : (set T) ^nat) : (mu (\bigcup_(n in ~` `I_N) (F n)) <= \sum_(N <= i <oo) mu (F i))%E.
proof: Proof. rewrite bigcup_mkcond. have := outer_measure_sigma_subadditive mu (fun n => if n \in ~` `I_N then F n else set0). move/le_trans; apply. rewrite [in leRHS]eseries_cond [in leRHS]eseries_mkcondr; apply: lee_nneseries. - by move=> k _; exact: outer_measure_ge0. - move=> k _; rewrite fun_if; case: ifPn => Nk; first by rewrite mem_not_I Nk. by rewrite mem_not_I (negbTE Nk) outer_measure0. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)