proposition: Lemma einfs_preimage T (a : \bar R) (f : (T -> \bar R)^nat) n : (fun x => einfs (f^~x) n) @^-1` `[a, +oo[%classic = \bigcap_(k in [set k | n <= k]%N) f k @^-1` `[a, +oo[%classic.
proof: Proof. rewrite predeqE => t; split => /= [|h]. rewrite in_itv andbT /= => h k nk /=. by rewrite /= in_itv/= (le_trans h)//; apply: ereal_inf_lb; exists k. rewrite /= in_itv /= andbT leNgt; apply/negP. move=> /ereal_inf_lt[_ /= [k nk <-]]; apply/negP. by have := h _ nk; rewrite /= in_itv /= andbT -leNgt. 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