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