Unique differentiability property in real normed spaces

In this file we prove that

• uniqueDiffOn_convex: a convex set with nonempty interior in a real normed space has the unique differentiability property;
• uniqueDiffOn_Ioc etc: intervals on the real line have the unique differentiability property.

theorem mem_tangentConeAt_of_openSegment_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {x y : E} (h : openSegment ℝ x y ⊆ s) : y - x ∈ tangentConeAt ℝ s x

If a subset of a real vector space contains an open segment, then the direction of this segment belongs to the tangent cone at its endpoints.

@[deprecated mem_tangentConeAt_of_openSegment_subset (since := "2025-04-27")]

theorem mem_tangentCone_of_openSegment_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {x y : E} (h : openSegment ℝ x y ⊆ s) : y - x ∈ tangentConeAt ℝ s x

Alias of mem_tangentConeAt_of_openSegment_subset.

---

If a subset of a real vector space contains an open segment, then the direction of this segment belongs to the tangent cone at its endpoints.

theorem mem_tangentConeAt_of_segment_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {x y : E} (h : segment ℝ x y ⊆ s) : y - x ∈ tangentConeAt ℝ s x

If a subset of a real vector space contains a segment, then the direction of this segment belongs to the tangent cone at its endpoints.

@[deprecated mem_tangentConeAt_of_segment_subset (since := "2025-04-27")]

theorem mem_tangentCone_of_segment_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {x y : E} (h : segment ℝ x y ⊆ s) : y - x ∈ tangentConeAt ℝ s x

Alias of mem_tangentConeAt_of_segment_subset.

---

If a subset of a real vector space contains a segment, then the direction of this segment belongs to the tangent cone at its endpoints.

theorem Convex.span_tangentConeAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (conv : Convex ℝ s) (hs : (interior s).Nonempty) {x : E} (hx : x ∈ closure s) : Submodule.span ℝ (tangentConeAt ℝ s x) = ⊤

theorem uniqueDiffWithinAt_convex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (conv : Convex ℝ s) (hs : (interior s).Nonempty) {x : E} (hx : x ∈ closure s) : UniqueDiffWithinAt ℝ s x

In a real vector space, a convex set with nonempty interior is a set of unique differentiability at every point of its closure.

theorem uniqueDiffOn_convex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (conv : Convex ℝ s) (hs : (interior s).Nonempty) : UniqueDiffOn ℝ s

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

theorem uniqueDiffOn_Ici (a : ℝ) : UniqueDiffOn ℝ (Set.Ici a)

theorem uniqueDiffOn_Iic (a : ℝ) : UniqueDiffOn ℝ (Set.Iic a)

theorem uniqueDiffOn_Ioi (a : ℝ) : UniqueDiffOn ℝ (Set.Ioi a)

theorem uniqueDiffOn_Iio (a : ℝ) : UniqueDiffOn ℝ (Set.Iio a)

theorem uniqueDiffOn_Icc {a b : ℝ} (hab : a < b) : UniqueDiffOn ℝ (Set.Icc a b)

theorem uniqueDiffOn_Ico (a b : ℝ) : UniqueDiffOn ℝ (Set.Ico a b)

theorem uniqueDiffOn_Ioc (a b : ℝ) : UniqueDiffOn ℝ (Set.Ioc a b)

theorem uniqueDiffOn_Ioo (a b : ℝ) : UniqueDiffOn ℝ (Set.Ioo a b)

theorem uniqueDiffOn_Icc_zero_one : UniqueDiffOn ℝ (Set.Icc 0 1)

The real interval [0, 1] is a set of unique differentiability.

theorem uniqueDiffWithinAt_Ioo {a b t : ℝ} (ht : t ∈ Set.Ioo a b) : UniqueDiffWithinAt ℝ (Set.Ioo a b) t

theorem uniqueDiffWithinAt_Ioi (a : ℝ) : UniqueDiffWithinAt ℝ (Set.Ioi a) a

theorem uniqueDiffWithinAt_Iio (a : ℝ) : UniqueDiffWithinAt ℝ (Set.Iio a) a

theorem uniqueDiffWithinAt_Ici (x : ℝ) : UniqueDiffWithinAt ℝ (Set.Ici x) x

theorem uniqueDiffWithinAt_Iic (x : ℝ) : UniqueDiffWithinAt ℝ (Set.Iic x) x