Theorems · Inductive type · global analysis

ModelWithCorners.Boundaryless

{𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] → {H : Type u_3} → [inst_3 : TopologicalSpace H] → ModelWithCorners 𝕜 E H → Prop

Property ensuring that the model with corners I defines manifolds without boundary. This differs from the more general BoundarylessManifold, which requires every point on the manifold to be an interior point.

Defined in

Mathlib.Geometry.Manifold.IsManifold.Basic

Cited by

20 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpace