We introduce the necessary bits to be able to define manifolds modelled over ℝ^n, boundaryless or with boundary or with corners. As a concrete example, we construct explicitly the manifold with boundary structure on the real interval [x, y].
More specifically, we introduce
The manifold structure on the interval [x, y] = Icc x y requires the assumption x < y. We introduce a dummy class lt_class x y for this, to make such an assumption available to typeclass search. This should hopefully not be necessary any more in Lean 4.
The space ℝ^n. Note that the name is slightly misleading, as we only need a normed space structure on ℝ^n, but the one we use here is the sup norm and not the euclidean one -- this is not a problem for the manifold applications, but should probably be refactored at some point.
The half-space in ℝ^n, used to model manifolds with boundary. We only define it when 1 ≤ n, as the definition only makes sense in this case.
The quadrant in ℝ^n, used to model manifolds with corners, made of all vectors with nonnegative coordinates.
Definition of the model with corners (euclidean_space n, euclidean_half_space n), used as a model for manifolds with boundary.
Definition of the model with corners (euclidean_space n, euclidean_quadrant n), used as a model for manifolds with corners
Dummy class to make an assumption such as x < y available to typeclass search. Such an assumption is used to define a manifold structure on [x, y] when x < y. Should be fixed in Lean 4.
The left chart for the topological space [x, y], defined on [x,y) and sending x to 0 in euclidean_half_space 1.
The right chart for the topological space [x, y], defined on (x,y] and sending y to 0 in euclidean_half_space 1.
Manifold with boundary structure on [x, y], using only two charts.
The manifold structure on [x, y] is smooth.