Theorems · Definition · global analysis

DifferentiableWithinAtProp

{𝕜 : 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' → (H → H') → Set H → H → Prop

Property in the model space of a model with corners of being differentiable within a set at a point, when read in the model vector space. This property will be lifted to manifolds to define differentiable functions between manifolds.

Defined in

Mathlib.Geometry.Manifold.MFDeriv.Defs

Cited by

13 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpaceNormedAddCommGroupNormedSpaceTopologicalSpace