How to define a real n-dimensional manifold (where is 𝓡?)

Stream: new members

[Dominic Steinitz]

I have

import Mathlib

variable {M : Type*} [TopologicalSpace M] [ChartedSpace ℝ M] [SmoothManifoldWithCorners (𝓡 1) M]

but get

unknown identifier '𝓡'

I'd like to define a n-dimensional real manifold. My plan as an exercise is to prove the composition of two smooth maps (on manifolds) is smooth. But I am not even out of the starting blocks :-(

[Luigi Massacci]

Did you open Manifold?

[Luigi Massacci]

A lot of notation is scoped

[Dominic Steinitz]

Luigi Massacci said:

A lot of notation is scoped

That solved it thanks and now I have other problems

[Luigi Massacci]

C'est la vie