[STATEMENT]
lemma smallomega_1_conv_filterlim: "f \<in> \<omega>[F](\<lambda>_. 1) \<longleftrightarrow> filterlim f at_infinity F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<in> \<omega>[F](\<lambda>_. 1::'b)) = filterlim f at_infinity F
[PROOF STEP]
by (auto intro: smallomegaI_filterlim_at_infinity dest: smallomegaD_filterlim_at_infinity)