proposition: Lemma lime_supE f a : lime_sup f a = ereal_inf [set sup_ball f a e | e in `]0, +oo[ ]%R.
proof: Proof. rewrite lime_sup_lim; apply/cvg_lim => //. apply: nondecreasing_at_right_cvge => //. by move=> x y; rewrite !in_itv/= !andbT => x0 y0; exact: sup_ball_le. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)