'open' vs 'namespace'

Stream: new members

[kaminsod]

What is the fundamental difference between 'open' and 'namespace' ? They seem somewhat interchangeable?

[Bryan Gin-ge Chen]

namespace foo adds foo. to the beginning of the names of all new declarations until end foo.

open foo simply lets you refer to theorems like foo.bar as bar.

See this section of TPiL for more details.

[Johan Commelin]

In addition, namespace foo also acts as open foo.

[kaminsod]

Makes sense, thanks!