Theorems · Definition · global analysis

ModelWithCorners.pi

{𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {ι : Type v} →
      [inst_1 : Fintype ι] →
        {E : ι → Type w} →
          [inst_2 : (i : ι) → NormedAddCommGroup (E i)] →
            [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] →
              {H : ι → Type u'} →
                [inst_4 : (i : ι) → TopologicalSpace (H i)] →
                  ((i : ι) → ModelWithCorners 𝕜 (E i) (H i)) → ModelWithCorners 𝕜 ((i : ι) → E i) (ModelPi H)

Given a finite family of ModelWithCorners I i on (E i, H i), we define the model with corners pi I on (Π i, E i, ModelPi H). See note [Manifold type tags] for explanation about ModelPi H.

Defined in

Mathlib.Geometry.Manifold.IsManifold.Basic

Cited by

0 results in Mathlib

Foundations

Depth 166 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldFintypeNormedAddCommGroupNormedSpaceTopologicalSpace