What's good notation for convergence?

Stream: general

[Jan-David Salchow]

To avoid introducing constants, @Johannes Hölzl asked me to change

/-- The notion of convergence of sequences in topological spaces. -/
def converges_to (x : ℕ → X) (limit : X) : Prop :=
∀ U : set X, limit ∈ U → is_open U → ∃ n0 : ℕ, ∀ n ≥ n0, (x n) ∈ U

(and a similar definition for convergence in metric spaces) into notation.

I'm struggling to find good notation. My first try was

notation x `⟶t` limit := ∀ U : set X, limit ∈ U → is_open U → ∃ n0 : ℕ, ∀ n ≥ n0, (x n) ∈ U

but this only works for a fixed topological space X. Is there a way to determine the domain for (the sequence) x without using meta programming? Or is the price for using notation that you always have to specify sequence, limit, and domain?

[Johannes Hölzl]

Uh, no, more like: notation x ⟶t limit := tendsto x at_top (nhds limit)

[Johannes Hölzl]

never put a big term on the right of a notation

[Johannes Hölzl]

also the term we want to operate on should be using tendsto and then we have different views on tendsto telling us how to unfold tendsto into a concrete representation.

tendsto x at_top (nhds limit) <-> ∀ U : set X, limit ∈ U → is_open U → ∃ n0 : ℕ, ∀ n ≥ n0, (x n) ∈ U

[Jan-David Salchow]

I see, that's better :)

[Jan-David Salchow]

The difference between equality and iff is a propext, why is it better to state it as an equality?

[Mario Carneiro]

usually it's stated as an iff

[Johannes Hölzl]

its an iff now ;-)