Theorems · Definition · global analysis

ContDiffWithinAtProp

{𝕜 : 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 →
                {E' : Type u_5} →
                  [inst_4 : NormedAddCommGroup E'] →
                    [inst_5 : NormedSpace 𝕜 E'] →
                      {H' : Type u_6} →
                        [inst_6 : TopologicalSpace H'] →
                          ModelWithCorners 𝕜 E' H' → WithTop ℕ∞ → (H → H') → Set H → H → Prop

Property in the model space of a model with corners of being C^n within a set at a point, when read in the model vector space. This property will be lifted to manifolds to define C^n functions between manifolds. The parameter n belongs to ℕ∞ω (accessible in the ContDiff scope), i.e. it can be a natural number, ∞, or ω, where C^ω corresponds to analytic functions.

Defined in

Mathlib.Geometry.Manifold.ContMDiff.Defs

Cited by

21 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpaceNormedAddCommGroupNormedSpaceTopologicalSpace