Structures · Geometry

IsManifold

Typeclass defining manifolds with respect to a model with corners, over a field 𝕜. This definition includes the model with corners I (which might allow boundary, corners, or not, so this class covers both manifolds with boundary and manifolds without boundary), and a smoothness parameter n : ℕ∞ω (where n = 0 means topological manifold, n = ∞ means smooth manifold and n = ω means analytic manifold).

Defined in

Mathlib.Geometry.Manifold.IsManifold.Basic

Shape

3 explicit arguments