proposition: Lemma limn_einf_shift u l : l \is a fin_num -> limn_einf (fun x => l + u x) = l + limn_einf u.
proof: Proof. move=> lfin; rewrite !limn_einf_lim; apply/cvg_lim => //; apply: cvg_trans; last first. apply: (@cvgeD _ \oo _ _ (cst l) (einfs u) _ (limn (einfs u))). - by rewrite fin_num_adde_defr. - exact: cvg_cst. - exact: is_cvg_einfs. suff : einfs (fun n => l + u n) = (fun n => l + einfs u n) by move=> ->. rewrite funeqE => n. apply/eqP; rewrite eq_le; apply/andP; split. - rewrite addeC -lee_subl_addr//; apply: lb_ereal_inf => /= _ [m /= mn] <-. rewrite lee_subl_addr//; apply: ereal_inf_lb. by exists m => //; rewrite addeC. - apply: lb_ereal_inf => /= _ [m /= mn] <-. by rewrite leeD2l//; apply: ereal_inf_lb; exists m => /=. 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