proposition: Lemma iota_filterlim_locally {F} {FF : ProperFilter' F} (f : T -> V) l : filterlim f F (locally l) -> iota (fun x => filterlim f F (locally x)) = l.
proof: Proof. apply iota_is_filter_lim. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub