Theorems · Definition · global analysis

UniqueDiffOn

(R : Type u) →
  {E : Type v} → [inst : Semiring R] → [inst_1 : AddCommGroup E] → [Module R E] → [TopologicalSpace E] → Set E → Prop

A property ensuring that the tangent cone to s at any of its points spans a dense subset of the whole space. The main role of this property is to ensure that the differential along s is unique, hence this name. The uniqueness it asserts is proved in UniqueDiffOn.eq in Mathlib/Analysis/Calculus/FDeriv/Basic.lean.

Defined in

Mathlib.Analysis.Calculus.TangentCone.Defs

Cited by

215 results in Mathlib

Foundations

Depth 7 from the axioms, rests on 29 definitions · uses no axioms

Assumes

SemiringAddCommGroupModuleTopologicalSpace