proposition: Lemma filterlim_ge_p_infty : forall {T F} {FF : Filter F} (f g : T -> R), F (fun x => f x <= g x) -> filterlim f F (Rbar_locally p_infty) -> filterlim g F (Rbar_locally p_infty).
proof: Proof. intros T F FF f g H Hf. intros P [M HM]. assert (H' : Rbar_locally p_infty (fun y => M < y)). now exists M. unfold filtermap. generalize (filter_and (fun x : T => f x <= g x) _ H (Hf (fun y : R => M < y) H')). apply filter_imp. intros x [H1 H2]. apply HM. now apply Rlt_le_trans with (f x). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy