Tangent cone

In this file, we define two predicates UniqueDiffWithinAt 𝕜 s x and UniqueDiffOn 𝕜 s ensuring that, if a function has two derivatives, then they have to coincide. As a direct definition of this fact (quantifying on all target types and all functions) would depend on universes, we use a more intrinsic definition: if all the possible tangent directions to the set s at the point x span a dense subset of the whole subset, it is easy to check that the derivative has to be unique.

Therefore, we introduce the set of all tangent directions, named tangentConeAt, and express UniqueDiffWithinAt and UniqueDiffOn in terms of it. One should however think of this definition as an implementation detail: the only reason to introduce the predicates UniqueDiffWithinAt and UniqueDiffOn is to ensure the uniqueness of the derivative. This is why their names reflect their uses, and not how they are defined.

Implementation details

Note that this file is imported by Mathlib.Analysis.Calculus.FDeriv.Basic. Hence, derivatives are not defined yet. The property of uniqueness of the derivative is therefore proved in Mathlib.Analysis.Calculus.FDeriv.Basic, but based on the properties of the tangent cone we prove here.

def tangentConeAt (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : Set E

The set of all tangent directions to the set s at the point x.

Equations

• One or more equations did not get rendered due to their size.

structure UniqueDiffWithinAt (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : Prop

A property ensuring that the tangent cone to s at x spans a dense subset of the whole space. The main role of this property is to ensure that the differential within s at x is unique, hence this name. The uniqueness it asserts is proved in UniqueDiffWithinAt.eq in Mathlib.Analysis.Calculus.FDeriv.Basic. To avoid pathologies in dimension 0, we also require that x belongs to the closure of s (which is automatic when E is not 0-dimensional).

• dense_tangentConeAt : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x))
• mem_closure : x ∈ closure s

theorem uniqueDiffWithinAt_iff (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) (x : E) : UniqueDiffWithinAt 𝕜 s x ↔ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure s

@[deprecated UniqueDiffWithinAt.dense_tangentConeAt (since := "2025-04-27")]

theorem UniqueDiffWithinAt.dense_tangentCone {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] {s : Set E} {x : E} (self : UniqueDiffWithinAt 𝕜 s x) : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x))

Alias of UniqueDiffWithinAt.dense_tangentConeAt.

def UniqueDiffOn (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (s : 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.

Equations

• UniqueDiffOn 𝕜 s = ∀ x ∈ s, UniqueDiffWithinAt 𝕜 s x

theorem mem_tangentConeAt_of_pow_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x y : E} {s : Set E} {r : 𝕜} (hr₀ : r ≠ 0) (hr : ‖r‖ < 1) (hs : ∀ᶠ (n : ℕ) in Filter.atTop, x + r ^ n • y ∈ s) : y ∈ tangentConeAt 𝕜 s x

@[simp]

theorem tangentConeAt_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} : tangentConeAt 𝕜 Set.univ x = Set.univ

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

theorem tangentCone_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} : tangentConeAt 𝕜 Set.univ x = Set.univ

Alias of tangentConeAt_univ.

theorem tangentConeAt_mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s t : Set E} (h : s ⊆ t) : tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x

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

theorem tangentCone_mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s t : Set E} (h : s ⊆ t) : tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x

Alias of tangentConeAt_mono.

@[simp]

theorem tangentConeAt_closure {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} : tangentConeAt 𝕜 (closure s) x = tangentConeAt 𝕜 s x

theorem tangentConeAt.lim_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {y : E} {α : Type u_5} (l : Filter α) {c : α → 𝕜} {d : α → E} (hc : Filter.Tendsto (fun (n : α) => ‖c n‖) l Filter.atTop) (hd : Filter.Tendsto (fun (n : α) => c n • d n) l (nhds y)) : Filter.Tendsto d l (nhds 0)

Auxiliary lemma ensuring that, under the assumptions defining the tangent cone, the sequence d tends to 0 at infinity.

theorem tangentConeAt_mono_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s t : Set E} (h : nhdsWithin x s ≤ nhdsWithin x t) : tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x

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

theorem tangentCone_mono_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s t : Set E} (h : nhdsWithin x s ≤ nhdsWithin x t) : tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x

Alias of tangentConeAt_mono_nhds.

theorem tangentConeAt_congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s t : Set E} (h : nhdsWithin x s = nhdsWithin x t) : tangentConeAt 𝕜 s x = tangentConeAt 𝕜 t x

Tangent cone of s at x depends only on 𝓝[s] x.

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

theorem tangentCone_congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s t : Set E} (h : nhdsWithin x s = nhdsWithin x t) : tangentConeAt 𝕜 s x = tangentConeAt 𝕜 t x

Alias of tangentConeAt_congr.

---

Tangent cone of s at x depends only on 𝓝[s] x.

theorem tangentConeAt_inter_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s t : Set E} (ht : t ∈ nhds x) : tangentConeAt 𝕜 (s ∩ t) x = tangentConeAt 𝕜 s x

Intersecting with a neighborhood of the point does not change the tangent cone.

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

theorem tangentCone_inter_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s t : Set E} (ht : t ∈ nhds x) : tangentConeAt 𝕜 (s ∩ t) x = tangentConeAt 𝕜 s x

Alias of tangentConeAt_inter_nhds.

---

Intersecting with a neighborhood of the point does not change the tangent cone.

theorem subset_tangentConeAt_prod_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} {t : Set F} {y : F} (ht : y ∈ closure t) : ⇑(LinearMap.inl 𝕜 E F) '' tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y)

The tangent cone of a product contains the tangent cone of its left factor.

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

theorem subset_tangentCone_prod_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} {t : Set F} {y : F} (ht : y ∈ closure t) : ⇑(LinearMap.inl 𝕜 E F) '' tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y)

Alias of subset_tangentConeAt_prod_left.

---

The tangent cone of a product contains the tangent cone of its left factor.

theorem subset_tangentConeAt_prod_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} {t : Set F} {y : F} (hs : x ∈ closure s) : ⇑(LinearMap.inr 𝕜 E F) '' tangentConeAt 𝕜 t y ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y)

The tangent cone of a product contains the tangent cone of its right factor.

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

theorem subset_tangentCone_prod_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} {t : Set F} {y : F} (hs : x ∈ closure s) : ⇑(LinearMap.inr 𝕜 E F) '' tangentConeAt 𝕜 t y ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y)

Alias of subset_tangentConeAt_prod_right.

---

The tangent cone of a product contains the tangent cone of its right factor.

theorem mapsTo_tangentConeAt_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_5} [DecidableEq ι] {E : ι → Type u_6} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] {s : (i : ι) → Set (E i)} {x : (i : ι) → E i} {i : ι} (hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)) : Set.MapsTo (⇑(LinearMap.single 𝕜 E i)) (tangentConeAt 𝕜 (s i) (x i)) (tangentConeAt 𝕜 (Set.univ.pi s) x)

The tangent cone of a product contains the tangent cone of each factor.

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

theorem mapsTo_tangentCone_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_5} [DecidableEq ι] {E : ι → Type u_6} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] {s : (i : ι) → Set (E i)} {x : (i : ι) → E i} {i : ι} (hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)) : Set.MapsTo (⇑(LinearMap.single 𝕜 E i)) (tangentConeAt 𝕜 (s i) (x i)) (tangentConeAt 𝕜 (Set.univ.pi s) x)

Alias of mapsTo_tangentConeAt_pi.

---

The tangent cone of a product contains the tangent cone of each factor.

theorem mem_tangentConeAt_of_openSegment_subset {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {s : Set G} {x y : G} (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 {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {s : Set G} {x y : G} (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 {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {s : Set G} {x y : G} (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 {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {s : Set G} {x y : G} (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 zero_mem_tangentCone {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x : E} (hx : x ∈ closure s) : 0 ∈ tangentConeAt 𝕜 s x

The tangent cone at a non-isolated point contains 0.

theorem tangentConeAt_subset_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} (hx : ¬AccPt x (Filter.principal s)) : tangentConeAt 𝕜 s x ⊆ 0

If x is not an accumulation point of s, then the tangent cone of satxis a subset of{0}`.

theorem UniqueDiffWithinAt.accPt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} [Nontrivial E] (h : UniqueDiffWithinAt 𝕜 s x) : AccPt x (Filter.principal s)

theorem tangentConeAt_nonempty_of_properSpace {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [ProperSpace E] {s : Set E} {x : E} (hx : AccPt x (Filter.principal s)) : (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty

In a proper space, the tangent cone at a non-isolated point is nontrivial.

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

theorem tangentCone_nonempty_of_properSpace {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [ProperSpace E] {s : Set E} {x : E} (hx : AccPt x (Filter.principal s)) : (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty

Alias of tangentConeAt_nonempty_of_properSpace.

---

In a proper space, the tangent cone at a non-isolated point is nontrivial.

theorem tangentConeAt_eq_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : Set 𝕜} {x : 𝕜} (hx : AccPt x (Filter.principal s)) : tangentConeAt 𝕜 s x = Set.univ

The tangent cone at a non-isolated point in dimension 1 is the whole space.

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

theorem tangentCone_eq_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : Set 𝕜} {x : 𝕜} (hx : AccPt x (Filter.principal s)) : tangentConeAt 𝕜 s x = Set.univ

Alias of tangentConeAt_eq_univ.

---

The tangent cone at a non-isolated point in dimension 1 is the whole space.

Properties of UniqueDiffWithinAt and UniqueDiffOn

This section is devoted to properties of the predicates UniqueDiffWithinAt and UniqueDiffOn.

theorem UniqueDiffOn.uniqueDiffWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {s : Set E} {x : E} (hs : UniqueDiffOn 𝕜 s) (h : x ∈ s) : UniqueDiffWithinAt 𝕜 s x

theorem uniqueDiffWithinAt_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} : UniqueDiffWithinAt 𝕜 Set.univ x

theorem uniqueDiffOn_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] : UniqueDiffOn 𝕜 Set.univ

theorem uniqueDiffOn_empty {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] : UniqueDiffOn 𝕜 ∅

theorem UniqueDiffWithinAt.congr_pt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x y : E} {s : Set E} (h : UniqueDiffWithinAt 𝕜 s x) (hy : x = y) : UniqueDiffWithinAt 𝕜 s y

@[simp]

theorem uniqueDiffWithinAt_closure {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} : UniqueDiffWithinAt 𝕜 (closure s) x ↔ UniqueDiffWithinAt 𝕜 s x

theorem UniqueDiffWithinAt.of_closure {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} : UniqueDiffWithinAt 𝕜 (closure s) x → UniqueDiffWithinAt 𝕜 s x

Alias of the forward direction of uniqueDiffWithinAt_closure.

theorem UniqueDiffWithinAt.closure {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} : UniqueDiffWithinAt 𝕜 s x → UniqueDiffWithinAt 𝕜 (closure s) x

Alias of the reverse direction of uniqueDiffWithinAt_closure.

theorem UniqueDiffWithinAt.mono_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s t : Set E} (h : UniqueDiffWithinAt 𝕜 s x) (st : nhdsWithin x s ≤ nhdsWithin x t) : UniqueDiffWithinAt 𝕜 t x

theorem UniqueDiffWithinAt.mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s t : Set E} (h : UniqueDiffWithinAt 𝕜 s x) (st : s ⊆ t) : UniqueDiffWithinAt 𝕜 t x

theorem UniqueDiffWithinAt.mono_closure {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s t : Set E} (h : UniqueDiffWithinAt 𝕜 s x) (st : s ⊆ closure t) : UniqueDiffWithinAt 𝕜 t x

theorem uniqueDiffWithinAt_congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s t : Set E} (st : nhdsWithin x s = nhdsWithin x t) : UniqueDiffWithinAt 𝕜 s x ↔ UniqueDiffWithinAt 𝕜 t x

theorem uniqueDiffWithinAt_inter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s t : Set E} (ht : t ∈ nhds x) : UniqueDiffWithinAt 𝕜 (s ∩ t) x ↔ UniqueDiffWithinAt 𝕜 s x

theorem UniqueDiffWithinAt.inter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s t : Set E} (hs : UniqueDiffWithinAt 𝕜 s x) (ht : t ∈ nhds x) : UniqueDiffWithinAt 𝕜 (s ∩ t) x

theorem uniqueDiffWithinAt_inter' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s t : Set E} (ht : t ∈ nhdsWithin x s) : UniqueDiffWithinAt 𝕜 (s ∩ t) x ↔ UniqueDiffWithinAt 𝕜 s x

theorem UniqueDiffWithinAt.inter' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s t : Set E} (hs : UniqueDiffWithinAt 𝕜 s x) (ht : t ∈ nhdsWithin x s) : UniqueDiffWithinAt 𝕜 (s ∩ t) x

theorem uniqueDiffWithinAt_of_mem_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} (h : s ∈ nhds x) : UniqueDiffWithinAt 𝕜 s x

theorem IsOpen.uniqueDiffWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} (hs : IsOpen s) (xs : x ∈ s) : UniqueDiffWithinAt 𝕜 s x

theorem UniqueDiffOn.inter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s t : Set E} (hs : UniqueDiffOn 𝕜 s) (ht : IsOpen t) : UniqueDiffOn 𝕜 (s ∩ t)

theorem IsOpen.uniqueDiffOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} (hs : IsOpen s) : UniqueDiffOn 𝕜 s

theorem UniqueDiffWithinAt.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} {t : Set F} {y : F} (hs : UniqueDiffWithinAt 𝕜 s x) (ht : UniqueDiffWithinAt 𝕜 t y) : UniqueDiffWithinAt 𝕜 (s ×ˢ t) (x, y)

The product of two sets of unique differentiability at points x and y has unique differentiability at (x, y).

theorem UniqueDiffWithinAt.univ_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (ι : Type u_5) [Finite ι] (E : ι → Type u_6) [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (s : (i : ι) → Set (E i)) (x : (i : ι) → E i) (h : ∀ (i : ι), UniqueDiffWithinAt 𝕜 (s i) (x i)) : UniqueDiffWithinAt 𝕜 (Set.univ.pi s) x

theorem UniqueDiffWithinAt.pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (ι : Type u_5) [Finite ι] (E : ι → Type u_6) [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (s : (i : ι) → Set (E i)) (x : (i : ι) → E i) (I : Set ι) (h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)) : UniqueDiffWithinAt 𝕜 (I.pi s) x

theorem UniqueDiffOn.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {t : Set F} (hs : UniqueDiffOn 𝕜 s) (ht : UniqueDiffOn 𝕜 t) : UniqueDiffOn 𝕜 (s ×ˢ t)

The product of two sets of unique differentiability is a set of unique differentiability.

theorem UniqueDiffOn.pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (ι : Type u_5) [Finite ι] (E : ι → Type u_6) [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (s : (i : ι) → Set (E i)) (I : Set ι) (h : ∀ i ∈ I, UniqueDiffOn 𝕜 (s i)) : UniqueDiffOn 𝕜 (I.pi s)

The finite product of a family of sets of unique differentiability is a set of unique differentiability.

theorem UniqueDiffOn.univ_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (ι : Type u_5) [Finite ι] (E : ι → Type u_6) [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (s : (i : ι) → Set (E i)) (h : ∀ (i : ι), UniqueDiffOn 𝕜 (s i)) : UniqueDiffOn 𝕜 (Set.univ.pi s)

The finite product of a family of sets of unique differentiability is a set of unique differentiability.

theorem uniqueDiffWithinAt_convex {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {s : Set G} (conv : Convex ℝ s) (hs : (interior s).Nonempty) {x : G} (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 {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℝ G] {s : Set G} (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_iff_accPt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : Set 𝕜} {x : 𝕜} : UniqueDiffWithinAt 𝕜 s x ↔ AccPt x (Filter.principal s)

In one dimension, a point is a point of unique differentiability of a set iff it is an accumulation point of the set.

theorem AccPt.uniqueDiffWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : Set 𝕜} {x : 𝕜} : AccPt x (Filter.principal s) → UniqueDiffWithinAt 𝕜 s x

Alias of the reverse direction of uniqueDiffWithinAt_iff_accPt.

---

In one dimension, a point is a point of unique differentiability of a set iff it is an accumulation point of the set.

@[deprecated uniqueDiffWithinAt_iff_accPt (since := "2025-04-20")]

theorem uniqueDiffWithinAt_or_nhdsWithin_eq_bot {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (s : Set 𝕜) (x : 𝕜) : UniqueDiffWithinAt 𝕜 s x ∨ nhdsWithin x (s \ {x}) = ⊥

In one dimension, every point is either a point of unique differentiability, or isolated.