Filters on posets

[lowasser]

Not related to the real numbers work I'm doing -- not directly -- just something that caught my interest.

[fredrik-bakke]

Nice little addition :)

At some point we might consider starting a new namespace topology and put locales and filters in that namespace, but that's not really called for until someone is actively taking on a project on topology.