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 .
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 .
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 .
|Date of creation||2013-03-22 16:34:45|
|Last modified on||2013-03-22 16:34:45|
|Last modified by||CWoo (3771)|