proposition: Lemma infs_preimage T (D : set T) r (f : (T -> R)^nat) n : (forall t, D t -> has_lbound (range (f ^~ t))) -> D `&` (fun x => infs (f ^~ x) n) @^-1` `]-oo, r[ = D `&` \bigcup_(k in [set k | n <= k]%N) f k @^-1` `]-oo, r[.
proof: Proof. move=> lb_f; rewrite predeqE => t; split. - have [|/set0P h] := eqVneq (sdrop (f ^~ t) n) set0. by rewrite predeqE => /(_ (f n t))[+ _] => /forall2NP/(_ n)/= []. rewrite /= in_itv /= => -[Dt]. by move=> /(inf_lt h)[_ [m /= nm <-]] fmtr; split => //; exists m. - move=> [Dt [k /= nk]]; rewrite /= in_itv /= => fktr. rewrite in_itv /=; split => //; apply: le_lt_trans fktr. by apply/inf_lb => //; [exact/has_lbound_sdrop/lb_f|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