proposition: Lemma filterlim_le_le : forall {T F} {FF : Filter F} (f g h : T -> R) (l : Rbar), F (fun x => f x <= g x <= h x) -> filterlim f F (Rbar_locally l) -> filterlim h F (Rbar_locally l) -> filterlim g F (Rbar_locally l).
proof: Proof. intros T F FF f g h l H Hf Hh. destruct l as [l| |]. - intros P [eps He]. assert (H' : Rbar_locally l (fun y => Rabs (y - l) < eps)). now exists eps. unfold filterlim, filter_le, filtermap in Hf, Hh |- *. generalize (filter_and _ _ H (filter_and _ _ (Hf _ H') (Hh _ H'))). apply filter_imp. intros x [H1 [H2 H3]]. apply He. apply Rabs_lt_between'. split. apply Rlt_le_trans with (2 := proj1 H1). now apply Rabs_lt_between'. apply Rle_lt_trans with (1 := proj2 H1). now apply Rabs_lt_between'. - apply filterlim_ge_p_infty with (2 := Hf). apply: filter_imp H. now intros x [H _]. - apply filterlim_le_m_infty with (2 := Hh). apply: filter_imp H. now intros x [_ H]. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy