Convergent sequences

Stream: Is there code for X?

[Moritz Doll]

Given a sequence a : ℕ → E (E topological space) is there a shorter way to state that a converges to some point then ∃ x, filter.tendsto a filter.at_top (𝓝 x)? This makes statements of theorems hard to read if you have several converging sequences and then prove that they converge to some explicit point.

[Oliver Nash]

It's so bad if you open filter and drop the filter. prefixes but maybe we do want some notation (maybe localized) for this.

[Oliver Nash]

E.g.,

import topology.basic

localized "notation a `→∞` x := filter.tendsto a filter.at_top (nhds x)" in sequential_limits

open_locale sequential_limits

variables {E : Type*} [topological_space E] (a : ℕ → E)

#check ∃ x, a →∞ x

[Patrick Massot]

I introduced such a notation a very long time ago and I regret it. If Moritz really needs this predicate a lot then he can define a notation for the whole predicate.

[Oliver Nash]

I'm willing to trust you that it would be regrettable but if there's an easy illustration of why, I'd be interested to hear it.

[Moritz Doll]

I don't really need it, but I feel that it makes statements really hard to read. Of course if there are technical reasons to not use shorthand notation, then I agree we should not use it. I have quite often in mathlib come across places where I would have liked to have abbreviations that don't change anything on the technical level, so that the statements look really nice, but all reductions work as intended.

[Oliver Nash]

A less controversial option might be a local notation around the relevant statements.

[Moritz Doll]

Given that math is hard enough as it is, I always prefer to have notation so that it is really easy to see that the statements in mathlib correspond to the statements in the literature (but maybe I am very oldschool about that)

[Matt Diamond]

I would have liked to have abbreviations that don't change anything on the technical level

would writing a def not suffice?

[Matt Diamond]

like how def converges_to {E : Type*} [topological_space E] (a : ℕ → E) (x) : Prop := filter.tendsto a filter.at_top (nhds x) would allow you to just write converges_to a x instead of the whole thing

[Matt Diamond]

you can define abbreviations for any proposition very easily

[Moritz Doll]

The 'issue' with def is that it is not syntactically equal to what it defines. this is why you cannot use rw, except if you mark your def as [reducible], because rw works up to reducible definitional equality (according to Mario). I want syntactic equality, which is even stronger.

[Matt Diamond]

ahh, I see... thanks for explaining, that makes sense

[Matt Diamond]

it would be nice if Lean gave you another way to create a syntactically-equal alias besides notation

[Matt Diamond]

though maybe notation is flexible enough... I haven't played around with it much

[Patrick Massot]

The problem with such a notation is that is creates an extra layer of complexity that needs to be unfolded when you want to use those theorems. It's fine when you look at the statement but as soon as you want to use it you need to remember what they stand for.