# Eventually always notation

Let $X$ be a set and $A\subset X$. For a sequence $F = (f_n)_{n\geq 0}$ of elements of $X$ we say that $F$ is eventually always in $A$ if for some $N\geq0$ it holds that $f_n\in A$ for all $n\geq N$. I wonder if there is a notation for this property. I do not know one, so I am going to use $$F\xrightarrow{e.a.}A$$ since eventually always property is certainly stronger than any kind of convergence $F\to A$. On the other hand, it may be not the best choice.

-
I see people write, "$f_n \in A$ for $n \gg 0$". I'm pretty sure that these mean the same thing. [I also think the first sentence is missing some words. I think you want to say that $f_n \in A$ for $n \geq N$.] –  Dylan Moreland Feb 7 '12 at 15:02
@Dylan thank you, I've fixed it. I maybe should use the same notation, but we'll see if there are other alternatives. –  Ilya Feb 7 '12 at 15:07
If you specify the notation at the beginning, then whatever you decide upon is probably fine. If I just saw $F\xrightarrow{e.a.}A$ I would probably not know what was going on. –  Dylan Moreland Feb 7 '12 at 15:12
@Dylan certainly, I will specify it explicitly. The question is rather, wouldn't it be a bit incorrect to use such a notation? It makes quite a sense to me, but maybe not to the other people even after the specification. –  Ilya Feb 7 '12 at 15:17

If you really want a notation, I would not write $F\xrightarrow{e.a.}A$, but maybe put some e.a. index on an $\in$ sign. I am used to terminology "eventually" rather than "eventually always", but of course you can use whatever terminology you choose and make clear to the reader.

$(f_n)$ is eventually in $A$: there is $N$ so that for all $n \ge N$ we have $f_n \in A$.
$(f_n)$ is frequently in $A$: for every $N$ there is $n \ge N$ so that $f_n \in A$.
Thanks for the answer. "Eventually" alone I saw used to denote $f_n\in A$ for at least $n$. I'll try to play around with $\stackrel{e.a.}{\in}$ and see is it good. –  Ilya Feb 7 '12 at 15:41
I will need to present it to people from the formal verification community, and for LTL eventually (as you've used) corresponds to eventually always, frequently corresponds to always eventually. I have to follow their terminology in that sense. –  Ilya Feb 7 '12 at 16:03