Chaining/gluing theorems

Stream: new members

[Pietro Lavino]

I am going through the Baire Category theorem proof in the textbook Mathematic in Lean and I was wondering when can an hypothesis be glued at the start of a theorem instead of written after with some space separating like usual. In this proof we see:refine' isClosed_ball.mem_of_tendsto ylim _where isClosedBall is a proof the closed balls are indeed closed sets but that is satisfying one of the hypothesis of the theorem IsClosed.mem_of_tendsto. How did this hypothesis make into the name of the theorem as if we were working with a new theorem?

[Richard Osborn]

Are you referring to the dot notation? It is explained in fpil here: https://lean-lang.org/functional_programming_in_lean/getting-to-know/conveniences.html#namespaces