Theorems · Theorem · global analysis

uniqueDiffOn_convex

∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousSMul ℝ E]
  {s : Set E} [IsTopologicalAddGroup E], Convex ℝ s → (interior s).Nonempty → UniqueDiffOn ℝ s

In a real vector space, a convex set with nonempty interior is a set of unique differentiability.

Defined in

Mathlib.Analysis.Calculus.TangentCone.Real

Cited by

7 results in Mathlib

Foundations

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

Assumes

AddCommGroupModuleTopologicalSpaceContinuousSMulIsTopologicalAddGroup