proposition: Lemma esups_preimage T (a : \bar R) (f : (T -> \bar R)^nat) n : (fun x => esups (f^~x) n) @^-1` `]a, +oo[ = \bigcup_(k in [set k | n <= k]%N) f k @^-1` `]a, +oo[.
proof: Proof. rewrite predeqE => t; split => /=. rewrite /= in_itv /= andbT=> /ereal_sup_gt[_ [/= k nk <-]] afnt. by exists k => //=; rewrite in_itv /= afnt. move=> -[k /= nk] /=; rewrite in_itv /= andbT => /lt_le_trans afkt. by rewrite in_itv andbT/=; apply/afkt/ereal_sup_ub; exists k. 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