proposition: Lemma sups_preimage T (D : set T) r (f : (T -> R)^nat) n : (forall t, D t -> has_ubound (range (f ^~ t))) -> D `&` (fun x => sups (f ^~x) n) @^-1` `]r, +oo[%classic = D `&` \bigcup_(k in [set k | n <= k]%N) f k @^-1` `]r, +oo[.
proof: Proof. move=> f_ub; rewrite predeqE => t; split. - have [|/set0P h] := eqVneq (sdrop (f ^~ t) n) set0. by rewrite predeqE => /(_ (f n t))[+ _] => /forall2NP/(_ n)/= []. rewrite /= in_itv /= andbT => -[Dt]. move=> /(sup_gt h)[_ [m /= nm <-]] rfmt. split => //; exists m => //. by rewrite /= in_itv /= rfmt. - move=> [Dt [k /= nk]]; rewrite in_itv /= andbT => rfkt. split=> //; rewrite /= in_itv /= andbT; apply: (lt_le_trans rfkt). by apply: sup_ub; [exact/has_ubound_sdrop/f_ub|by 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