Theorems · Inductive type · global analysis

ModelWithCorners

(𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    (E : Type u_2) →
      [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (H : Type u_3) → [TopologicalSpace H] → Type (max u_2 u_3)

A structure containing information on the way a space H embeds in a model vector space E over the field 𝕜. This is all that is needed to define a C^n manifold with model space H, and model vector space E. We require that, when the field is ℝ or ℂ, the range is ℝ-convex, as this is what is needed to do calculus and covers the standard examples of manifolds with boundary. Over other fields, we require that the range is univ, as there is no relevant notion of manifold with boundary there.

Defined in

Mathlib.Geometry.Manifold.IsManifold.Basic

Cited by

2,462 results in Mathlib

Foundations

Depth 11 from the axioms, rests on 70 definitions · uses no axioms

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpace