how to define nets?

Stream: general

[Aron]

I don't think mathlib has an entry for nets, as defined here:
A function from an upward directed set to a set.
How would I go about defining updirsets and then nets?

[Heather Macbeth]

I'm not sure whether directed sets exist in mathlib. But preorders do, so you probably want to start with that notion (docs#preorder), and add extra hypotheses from there.

[Heather Macbeth]

Note that mathlib's topology is built around filters (docs#filter), which are a little more general than nets.

[Yury G. Kudryashov]

We have docs#directed_order

[Yury G. Kudryashov]

But most theorems assume [semilattice_sup α] instead

[Yury G. Kudryashov]

If you want to migrate theorems to directed_order, you should

• add a typeclass for the dual notion;
• add instance from semilattice_sup to directed_order;
• replace [semilattice_sup α] with [directed_order α] in many theorems, e.g., those about docs#filter.at_top

[Patrick Massot]

We should have a FAQ entry about why we use filters instead of nets. Filters are much more versatile than nets, and have much better formal properties. There are really much better than nets from every point of view except for the initial learning curve. It doesn't mean people shouldn't have fun formalizing nets using Lean, but we clearly won't switch in mathlib. We could have the definition in mathlib, but duplicating too many things would be very counter-productive and confusing.

[Yury G. Kudryashov]

We can switch theorems from [semilattice_sup α] to [directed_order α], and say "if you want to talk about nets, then use {α : Type*} [directed_order α] [nonempty α] {f : α → β} {l : filter β} (h : tendsto f at_top l)

[Aron]

Filters might be better than nets, but my professor has a hardon for nets.
I tried doing this on my own, and I'm probably far off the mark:

import topology.metric_space.basic topology.uniform_space.basic order.rel_classes algebra.order order

class my_updirorder (α: Type) extends preorder α :=
(le_updir : ∀ a b : α, ∃ c : α , a ≤ c ∧ b ≤ c)
structure my_updirset (α : Type):=
(set : set α )
(order : my_updirorder α )
def my_eventually {X Y Z: Type*} [my_updirset Z] [set X] (c : Z → X) (Y: set X):=∃ (n:Z),∀ (m:Z), m ≥ n → c m ∈ Y

The error happens in my_eventually:

failed to synthesize type class instance for
X : Type ?,
Y : Type ?,
Z : Type,
_inst_1 : my_updirset Z,
_inst_2 : set X,
c : Z → X,
Y : set X,
n m : Z
⊢ has_le Z

I think it doesn't want to extend has_le from preorder?

[Aron]

figured it out, just abandon my_updirset.