proposition: Lemma nondecreasing_at_right_cvgr f a (b : itv_bound R) : (BRight a < b)%O -> {in Interval (BRight a) b &, nondecreasing_fun f} -> has_lbound (f @` [set` Interval (BRight a) b]) -> f x @[x --> a ^'+] --> inf (f @` [set` Interval (BRight a) b]).
proof: Proof. move=> ab nif hlb; set M := inf _. have ndNf : {in Interval (BRight a) b &, nonincreasing_fun (\- f)}. by move=> r s rab sab /nif; rewrite lerN2; exact. have hub : has_ubound [set (\- f) x | x in [set` Interval (BRight a) b]]. apply/has_ub_lbN; rewrite image_comp/=. rewrite [X in has_lbound X](_ : _ = f @` [set` Interval (BRight a) b])//. by apply: eq_imagel => y _ /=; rewrite opprK. have /cvgN := nonincreasing_at_right_cvgr ab ndNf hub. rewrite opprK [X in _ --> X -> _](_ : _ = inf (f @` [set` Interval (BRight a) b]))//. by rewrite /inf; congr (- sup _); rewrite image_comp/=; exact: eq_imagel. 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)