filter convergence and tendsto

Stream: maths

[Bernd Losert]

How is filter convergence done in mathlib. For example, how do I say that the neighborhood filter at x converges to x? Do I write this as tendsto id (𝓝 x) (𝓟 {x}) ?

[Johan Commelin]

I think that "converging to x" typically means tendsto f _ (𝓝 x).

[Johan Commelin]

So in that case, "the neighbourhoud filter at x convergest to x" would be a tautology.

[Bernd Losert]

Ah, I think you're right. I had the filter arguments backwards. Do you know if there is special notation for this?

[Bernd Losert]

I was thinking of something like (𝓝 x) converges_to x.

[Patrick Massot]

No, there is no special notation.

[Reid Barton]

The notation is 𝓝 x ≤ 𝓝 x :upside_down:

[Bernd Losert]

I think you mean 𝓟 {x} ≤ 𝓝 x.

[Patrick Massot]

These are different statements.

[Patrick Massot]

The statement (𝓝 x) converges_to x is what Reid wrote.

[Bernd Losert]

OK. I guess I'm confused because I don't know what is playing the role of "x" here.

[Bernd Losert]

I was told that to think of filters as sets and ultrafilters as points, so 𝓟 {x} would be "x".

[Bernd Losert]

𝓟 {x} ≤ 𝓝 x <-- So this means that 𝓟 {x} converges to x.

[Reid Barton]

That's also true but it says that the principal filter at x converges to x--which probably is what you meant in the first place

[Reid Barton]

(As a sanity check, the notion "converges to x" depends on the topology, so it must involve 𝓝 x.)

[Bernd Losert]

Yeah. Thanks.