proposition: Lemma __deprecated__squeeze T (f g h : T -> R) (a : filter_on T) : (\forall x \near a, f x <= g x <= h x) -> forall (l : R), f @ a --> l -> h @ a --> l -> g @ a --> l.
proof: Proof. exact: squeeze_cvgr. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau