Meaning of open Example (...) syntax

Stream: new members

[Nilay Patel]

I saw the syntax open Filter (Tendsto) in Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean and wasn't sure what this means. Is it a restricted opening ofFilter which only allows Tendsto through?

I also noticed (I think) that open Filter.Tendsto is also valid syntax, and I'm not sure what the difference is in this case. Any clarification would be very helpful.

Thanks in advance!

[Aaron Liu]

From docs#Lean.Parser.Command.open:

• open Some.Namespace.Path (def1 def2) only makes Some.Namespace.Path.def1 and
  Some.Namespace.Path.def2 available without the full prefix, so Some.Namespace.Path.def3 would
  be unaffected.

  This works even if def1 and def2 are protected.

[Aaron Liu]

open Filter.TendsTo works because you can open any namespace, even ones that don't have anything in them. To check the definitions registered for a namespace, you can #print prefix Namespace (this seems to be very slow).

[Nilay Patel]

This is perfect, I didn't see the page from the docs. Much appreciated!