Theorems · Definition · global analysis

UniqueMDiffWithinAt

{𝕜 : 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 →
                {M : Type u_4} → [inst : TopologicalSpace M] → [ChartedSpace H M] → Set M → M → Prop

Predicate ensuring that, at a point and within a set, a function can have at most one derivative. This is expressed using the preferred chart at the considered point.

Defined in

Mathlib.Geometry.Manifold.MFDeriv.Defs

Cited by

83 results in Mathlib

Foundations

Depth 46 from the axioms · uses propext, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpace