proposition: Lemma filterlimi_locally_unique : forall {F} {FF : ProperFilter' F} (f : T -> V -> Prop) (x y : V), F (fun x => forall y1 y2, f x y1 -> f x y2 -> y1 = y2) -> filterlimi f F (locally x) -> filterlimi f F (locally y) -> x = y.
proof: Proof. intros F FF f x y Hf Hx Hy. apply ball_norm_eq => eps. specialize (Hx (ball_norm x (pos_div_2 eps)) (locally_ball_norm _ _)). specialize (Hy (ball_norm y (pos_div_2 eps)) (locally_ball_norm _ _)). unfold filtermapi in Hx, Hy. apply Rnot_le_lt. intros H. apply (@filter_not_empty _ F FF). apply: filter_imp (filter_and _ _ (filter_and _ _ Hx Hy) Hf). clear -H. intros z [[[x' [Hx Bx]] [y' [Hy By]]] Hf]. apply: Rlt_not_le H. rewrite (double_var eps). change (eps / 2) with (pos (pos_div_2 eps)). apply ball_norm_triangle with (1 := Bx). apply ball_norm_sym. now rewrite (Hf _ _ Hx Hy). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub