proposition: Lemma le_limn_infD u v : bounded_fun u -> bounded_fun v -> limn_inf u + limn_inf v <= limn_inf (u \+ v).
proof: Proof. move=> ba bb; have ab k : infs u k + infs v k <= infs (u \+ v) k. apply: lb_le_inf; first by exists ((u \+ v) k); exists k => /=. by move=> M [n /= kn <-]; apply: lerD; apply: inf_lb; [ exact/has_lbound_sdrop/bounded_fun_has_lbound; exact | exists n | exact/has_lbound_sdrop/bounded_fun_has_lbound; exact | exists n ]. have cu : cvgn (infs u). apply: nondecreasing_is_cvgn; last exact: bounded_fun_has_ubound_infs. exact/nondecreasing_infs/bounded_fun_has_lbound. have cv : cvgn (infs v). apply: nondecreasing_is_cvgn; last exact: bounded_fun_has_ubound_infs. exact/nondecreasing_infs/bounded_fun_has_lbound. rewrite -(limD cu cv); apply: ler_lim. - exact: is_cvgD cu cv. - apply: nondecreasing_is_cvgn; last first. exact/bounded_fun_has_ubound_infs/bounded_funD. exact/nondecreasing_infs/bounded_fun_has_lbound/bounded_funD. - exact: nearW. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau