Don't understand "pure x" as a filter

Stream: new members

[Ching-Tsun Chou]

In sec.10.3.1 of #mil, there is the following passage:

The first constraint is that 𝓝 x, seen as a generalized set, contains the set {x} seen as the generalized set pure x (explaining this weird name would be too much of a digression, so we simply accept it for now). Another way to say it is that if a predicate holds for points close to xthen it holds at x.

example (x : X) : pure x ≤ 𝓝 x :=
pure_le_nhds x

What is pure x in this context? More precisely, what exactly is pure x as a set of subsets of X? Where can I find the definition? F12 sends me to the definition of the typeclass Pure, which is not very helpful.

Also, check 𝓝 x tells me that 𝓝 x is of type Filter X. But even #check pure x : Filter X fails to infer the type: pure x : ?m.2222 X. Why?

[Mitchell Lee]

It is the set of all sets that contain x

[Mitchell Lee]

You need to put parentheses around pure x : Filter X in order to do the type ascription. Try #check (pure x : Filter X).

[Mitchell Lee]

See here: Filter.instPure

[Ching-Tsun Chou]

Thanks! I was able to prove it:

example (x : X) : pure x = 𝓟 {x} := by simp

[Kyle Miller]

I think it's good to use something like simp? learn why it is that these are equal — that points to docs#Filter.principal_singleton in Mathlib.Order.Filter.Basic, so at least that equality is meant to be part of the basic theory. If not for technical reasons, it could be proved with rfl (it could be by definition). Here's the definition of pure: docs#Filter.instPure

If you want to know a bit more details, Filter forms a monad via docs#Filter.monad, which is where this odd pure terminology is coming from.

[Ching-Tsun Chou]

Thanks! How does Filter form a monad? What are the monad operations?