proposition: Lemma is_filter_lim_unique : forall {F} {FF : ProperFilter' F} (x y : V), is_filter_lim F x -> is_filter_lim F y -> x = y.
proof: Proof. intros F FF x y Hx Hy. apply ball_norm_eq => eps. assert (Hx': F (ball_norm x (pos_div_2 eps))). apply Hx. apply locally_ball_norm. assert (Hy': F (ball_norm y (pos_div_2 eps))). apply Hy. apply locally_ball_norm. apply Rnot_le_lt. intros H. apply (@filter_not_empty V F FF). apply: filter_imp (filter_and _ _ Hx' Hy'). clear -H. intros z [Bx By]. revert H. apply Rlt_not_le. rewrite (double_var eps). change (eps / 2) with (pos (pos_div_2 eps)). apply ball_norm_triangle with (1 := Bx). now apply ball_norm_sym. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub