0
$\begingroup$

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.

  • 0
    @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.2012-02-07

1 Answers 1

1

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.

added

Terminology (I think from Kelley):

$(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$.

(Stated this way, and not "all but finitely many" and "infintely many" so that it applies to nets other than sequences.)

  • 1
    I will need to present it to people from the formal verification community, and for [LTL](http://en.wikipedia.org/wiki/Linear_temporal_logic) `eventually` (as you've used) corresponds to `eventually always`, `frequently` corresponds to `always eventually`. I have to follow their terminology in that sense.2012-02-07