Zulip Chat Archive

Stream: general

Topic: What's good notation for convergence?


Jan-David Salchow (Jan 15 2019 at 11:24):

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 (Jan 15 2019 at 11:25):

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

Johannes Hölzl (Jan 15 2019 at 11:25):

never put a big term on the right of a notation

Johannes Hölzl (Jan 15 2019 at 11:26):

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 (Jan 15 2019 at 13:27):

I see, that's better :)

Jan-David Salchow (Jan 15 2019 at 13:28):

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

Mario Carneiro (Jan 15 2019 at 13:51):

usually it's stated as an iff

Johannes Hölzl (Jan 15 2019 at 14:42):

its an iff now ;-)


Last updated: Dec 20 2023 at 11:08 UTC