proposition: Lemma iota_filterlimi_locally {F} {FF : ProperFilter' F} (f : T -> V -> Prop) l : F (fun x => forall y1 y2, f x y1 -> f x y2 -> y1 = y2) -> filterlimi f F (locally l) -> iota (fun x => filterlimi f F (locally x)) = l.
proof: Proof. intros Hf Hl. apply: iota_unique (Hl) => l' Hl'. exact: filterlimi_locally_unique Hf Hl' Hl. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub