proposition: Lemma filterlim_locally_ball_norm : forall {K : AbsRing} {T} {U : NormedModule K} {F : (T -> Prop) -> Prop} {FF : Filter F} (f : T -> U) (y : U), filterlim f F (locally y) <-> forall eps : posreal, F (fun x => ball_norm y eps (f x)).
proof: Proof. intros K T U F FF f y. split. - intros Cf eps. apply (Cf (fun x => ball_norm y eps x)). apply locally_le_locally_norm. apply locally_norm_ball_norm. - intros Cf. apply (filterlim_filter_le_2 _ (locally_norm_le_locally y)). intros P [eps He]. apply: filter_imp (Cf eps). intros t. apply He. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub