eventual property
Let be a set and a property on the elements of . Let be a net ( a directed set![]()
) in (that is, ). As each , either has or does not have property . We say that the net has property above if has property for all . Furthermore, we say that eventually has property if it has property above some .
Examples.
-
1.
Let and be non-empty sets. For , let be the property that . So is nothing more than the property of elements being in the intersection

of and . A net eventually has means that for some , the set . If , then we have that and eventually coincide.
-
2.
Now, suppose is a topological space

, and is an open neighborhood of a point . For , let be the property that . Then a net has eventually for every neighborhood of is a characterization of convergence (to the point , and is the accumulation point
of ).
-
3.
If is a poset and . For , let again be the property that . Let be a net that eventually has property . In other words, is eventually constant. In particular, if for every chain , the net is eventually constant in , then we have a characterization of the ascending chain condition

in .
-
4.
directed net. Let be a preorder

and let be a net in . Let be the image of the net: . Given a fixed and some , let be the property (on ) that . Let
If , then we say that the net is directed, or that is a directed net. In other words, a directed net is a net such that for every , there is a , such that for all .
If is a directed net, then is a directed set: Pick , then there are such that for all and for all . Since is directed, there is a such that and . So and .
However, if is a net such that is directed, need not be a directed net. For example, let such that , and such that . Define a net by and . Then is not a directed net.
Remark. The eventual property is a property on the class of nets (on a given set and a given property ). We can write to denote its dependence on and .
| Title | eventual property |
|---|---|
| Canonical name | EventualProperty |
| Date of creation | 2013-03-22 16:34:45 |
| Last modified on | 2013-03-22 16:34:45 |
| Owner | CWoo (3771) |
| Last modified by | CWoo (3771) |
| Numerical id | 16 |
| Author | CWoo (3771) |
| Entry type | Definition |
| Classification | msc 06A06 |
| Synonym | residually constant |
| Defines | eventually |
| Defines | directed net |
| Defines | eventually constant |