proposition: Lemma cvg_limn_inf_sup u l : u @ \oo --> l -> (limn_inf u = l) * (limn_sup u = l).
proof: Proof. move=> ul. have /cvg_seq_bounded [M [Mr Mu]] : cvg (u @ \oo) by apply/cvg_ex; eexists; exact: ul. suff: limn_sup u <= l <= limn_inf u. move=> /andP[sul liu]. have /limn_inf_sup iusu : cvg (u @ \oo) by apply/cvg_ex; eexists; exact: ul. split; first by apply/eqP; rewrite eq_le liu andbT (le_trans iusu). by apply/eqP; rewrite eq_le sul /= (le_trans _ iusu). apply/andP; split. - apply/ler_addgt0Pr => e e0. apply: limr_le; first by apply: is_cvg_sups; apply/cvg_ex; exists l. move/cvgrPdist_lt : (ul) => /(_ _ e0) -[k _ klu]. near=> n; have kn : (k <= n)%N by near: n; exists k. apply: sup_le_ub; first by exists (u n) => /=; exists n => //=. move=> _ /= [m nm] <-; apply/ltW/ltr_distlDr; rewrite distrC. by apply: (klu m) => /=; rewrite (leq_trans kn). - apply/ler_addgt0Pr => e e0; rewrite -lerBlDr. apply: limr_ge; first by apply: is_cvg_infs; apply/cvg_ex; exists l. move/cvgrPdist_lt : (ul) => /(_ _ e0) -[k _ klu]. near=> n; have kn : (k <= n)%N by near: n; exists k. apply: lb_le_inf; first by exists (u n) => /=; exists n => //=. move=> _ /= [m nm] <-; apply/ltW/ltr_distlBl. by apply: (klu m) => /=; rewrite (leq_trans kn). Unshelve. all: by end_near. 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