Basic properties of tangent cones and sets with unique differentiability property

In this file we prove basic lemmas about tangentConeAt, UniqueDiffWithinAt, and UniqueDiffOn.

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

theorem tangentConeAt_mono_field {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [SMul 𝕜 E] [TopologicalSpace E] {s : Set E} {x : E} {𝕜' : Type u_3} [Monoid 𝕜'] [SMul 𝕜 𝕜'] [MulAction 𝕜' E] [IsScalarTower 𝕜 𝕜' E] : tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜' s x

Given x ∈ s and a semiring extension 𝕜 ⊆ 𝕜', the tangent cone of s at x with respect to 𝕜 is contained in the tangent cone of s at x with respect to 𝕜'.

theorem Filter.HasBasis.tangentConeAt_eq_biInter_closure {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [SMul 𝕜 E] [TopologicalSpace E] {s : Set E} {x : E} {ι : Sort u_3} {p : ι → Prop} {U : ι → Set E} (h : (nhds 0).HasBasis p U) : tangentConeAt 𝕜 s x = ⋂ (i : ι), ⋂ (_ : p i), closure (Set.univ • (U i ∩ (fun (x_2 : E) => x + x_2) ⁻¹' s))

theorem tangentConeAt_eq_biInter_closure {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [SMul 𝕜 E] [TopologicalSpace E] {s : Set E} {x : E} : tangentConeAt 𝕜 s x = ⋂ U ∈ nhds 0, closure (Set.univ • (U ∩ (fun (x_1 : E) => x + x_1) ⁻¹' s))

theorem tangentConeAt_mono_nhds {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [SMul 𝕜 E] [TopologicalSpace E] {s t : Set E} {x : E} [ContinuousAdd E] (h : nhdsWithin x s ≤ nhdsWithin x t) : tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x

theorem tangentConeAt_congr {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [SMul 𝕜 E] [TopologicalSpace E] {s t : Set E} {x : E} [ContinuousAdd 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.

theorem tangentConeAt_inter_nhds {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [SMul 𝕜 E] [TopologicalSpace E] {s t : Set E} {x : E} [ContinuousAdd 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.

theorem mem_closure_of_nonempty_tangentConeAt {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [SMul 𝕜 E] [TopologicalSpace E] {s : Set E} {x : E} [ContinuousAdd E] (h : (tangentConeAt 𝕜 s x).Nonempty) : x ∈ closure s

@[simp]

theorem tangentConeAt_closure {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [SMul 𝕜 E] [TopologicalSpace E] {s : Set E} {x : E} [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] : tangentConeAt 𝕜 (closure s) x = tangentConeAt 𝕜 s x

theorem UniqueDiffWithinAt.mono {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Semiring 𝕜] [Module 𝕜 E] [TopologicalSpace E] {s t : Set E} {x : E} (h : UniqueDiffWithinAt 𝕜 s x) (st : s ⊆ t) : UniqueDiffWithinAt 𝕜 t x

theorem UniqueDiffWithinAt.closure {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Semiring 𝕜] [Module 𝕜 E] [TopologicalSpace E] {s : Set E} {x : E} (h : UniqueDiffWithinAt 𝕜 s x) : UniqueDiffWithinAt 𝕜 (closure s) x

theorem UniqueDiffWithinAt.mono_nhds {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Semiring 𝕜] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] {s t : Set E} {x : E} (h : UniqueDiffWithinAt 𝕜 s x) (st : nhdsWithin x s ≤ nhdsWithin x t) : UniqueDiffWithinAt 𝕜 t x

theorem uniqueDiffWithinAt_congr {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Semiring 𝕜] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] {s t : Set E} {x : E} (st : nhdsWithin x s = nhdsWithin x t) : UniqueDiffWithinAt 𝕜 s x ↔ UniqueDiffWithinAt 𝕜 t x

theorem uniqueDiffWithinAt_inter {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Semiring 𝕜] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] {s t : Set E} {x : E} (ht : t ∈ nhds x) : UniqueDiffWithinAt 𝕜 (s ∩ t) x ↔ UniqueDiffWithinAt 𝕜 s x

theorem UniqueDiffWithinAt.inter {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Semiring 𝕜] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] {s t : Set E} {x : E} (hs : UniqueDiffWithinAt 𝕜 s x) (ht : t ∈ nhds x) : UniqueDiffWithinAt 𝕜 (s ∩ t) x

theorem UniqueDiffOn.inter {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Semiring 𝕜] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] {s t : Set E} (hs : UniqueDiffOn 𝕜 s) (ht : IsOpen t) : UniqueDiffOn 𝕜 (s ∩ t)

theorem uniqueDiffWithinAt_inter' {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Semiring 𝕜] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] {s t : Set E} {x : E} (ht : t ∈ nhdsWithin x s) : UniqueDiffWithinAt 𝕜 (s ∩ t) x ↔ UniqueDiffWithinAt 𝕜 s x

theorem UniqueDiffWithinAt.inter' {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Semiring 𝕜] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] {s t : Set E} {x : E} (hs : UniqueDiffWithinAt 𝕜 s x) (ht : t ∈ nhdsWithin x s) : UniqueDiffWithinAt 𝕜 (s ∩ t) x

theorem zero_mem_tangentConeAt {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Semiring 𝕜] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] {s : Set E} {x : E} (hx : x ∈ closure s) : 0 ∈ tangentConeAt 𝕜 s x

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

@[deprecated zero_mem_tangentConeAt (since := "2026-01-21")]

theorem zero_mem_tangentCone {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Semiring 𝕜] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] {s : Set E} {x : E} (hx : x ∈ closure s) : 0 ∈ tangentConeAt 𝕜 s x

Alias of zero_mem_tangentConeAt.

---

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

@[simp]

theorem zero_mem_tangentConeAt_iff {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Semiring 𝕜] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] {s : Set E} {x : E} : 0 ∈ tangentConeAt 𝕜 s x ↔ x ∈ closure s

theorem tangentConeAt_subset_zero {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Semiring 𝕜] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] {s : Set E} {x : E} [T2Space 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 s at x is a subset of {0}.

theorem AccPt.of_mem_tangentConeAt_ne_zero {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Semiring 𝕜] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] {s : Set E} {x : E} [T2Space E] {y : E} (hy : y ∈ tangentConeAt 𝕜 s x) (hy₀ : y ≠ 0) : AccPt x (Filter.principal s)

theorem UniqueDiffWithinAt.accPt {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Semiring 𝕜] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] {s : Set E} {x : E} [T2Space E] [Nontrivial E] (h : UniqueDiffWithinAt 𝕜 s x) : AccPt x (Filter.principal s)

theorem mem_tangentConeAt_of_add_smul_mem {𝕜 : Type u_1} {E : Type u_2} [DivisionSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace 𝕜] [TopologicalSpace E] [ContinuousSMul 𝕜 E] {s : Set E} {x y : E} {α : Type u_3} {l : Filter α} [l.NeBot] {c : α → 𝕜} (hc₀ : Filter.Tendsto c l (nhdsWithin 0 {0}ᶜ)) (hmem : ∀ᶠ (n : α) in l, x + c n • y ∈ s) : y ∈ tangentConeAt 𝕜 s x

@[simp]

theorem tangentConeAt_univ {𝕜 : Type u_1} {E : Type u_2} [DivisionSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace 𝕜] [TopologicalSpace E] [ContinuousSMul 𝕜 E] {x : E} [(nhdsWithin 0 {0}ᶜ).NeBot] : tangentConeAt 𝕜 Set.univ x = Set.univ

theorem tangentConeAt_of_mem_nhds {𝕜 : Type u_1} {E : Type u_2} [DivisionSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace 𝕜] [TopologicalSpace E] [ContinuousSMul 𝕜 E] {s : Set E} {x : E} [(nhdsWithin 0 {0}ᶜ).NeBot] [ContinuousAdd E] (h : s ∈ nhds x) : tangentConeAt 𝕜 s x = Set.univ

Properties of UniqueDiffWithinAt and UniqueDiffOn

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

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

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

theorem UniqueDiffWithinAt.mono_field {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s : Set E} {𝕜' : Type u_3} [Semiring 𝕜'] [SMul 𝕜 𝕜'] [Module 𝕜' E] [IsScalarTower 𝕜 𝕜' E] (hs : UniqueDiffWithinAt 𝕜 s x) : UniqueDiffWithinAt 𝕜' s x

Assume that E is a normed vector space over semirings 𝕜 ⊆ 𝕜' and that x ∈ s is a point of unique differentiability with respect to the set s and the smaller semiring 𝕜, then x is also a point of unique differentiability with respect to the set s and the larger semiring 𝕜'.

theorem UniqueDiffOn.mono_field {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {s : Set E} {𝕜' : Type u_3} [Semiring 𝕜'] [SMul 𝕜 𝕜'] [Module 𝕜' E] [IsScalarTower 𝕜 𝕜' E] (hs : UniqueDiffOn 𝕜 s) : UniqueDiffOn 𝕜' s

Assume that E is a normed vector space over semirings 𝕜 ⊆ 𝕜' and all points of s are points of unique differentiability with respect to the smaller semiring 𝕜, then they are also points of unique differentiability with respect to the larger semiring 𝕜.

@[simp]

theorem uniqueDiffWithinAt_closure {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s : Set E} [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] : UniqueDiffWithinAt 𝕜 (closure s) x ↔ UniqueDiffWithinAt 𝕜 s x

theorem UniqueDiffWithinAt.of_closure {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s : Set E} [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] : UniqueDiffWithinAt 𝕜 (closure s) x → UniqueDiffWithinAt 𝕜 s x

Alias of the forward direction of uniqueDiffWithinAt_closure.

theorem UniqueDiffWithinAt.mono_closure {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {x : E} {s t : Set E} [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] (h : UniqueDiffWithinAt 𝕜 s x) (st : s ⊆ closure t) : UniqueDiffWithinAt 𝕜 t x

@[simp]

theorem uniqueDiffWithinAt_univ {𝕜 : Type u_1} {E : Type u_2} [DivisionSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalSpace 𝕜] [(nhdsWithin 0 {0}ᶜ).NeBot] [ContinuousSMul 𝕜 E] {x : E} : UniqueDiffWithinAt 𝕜 Set.univ x

@[simp]

theorem uniqueDiffOn_univ {𝕜 : Type u_1} {E : Type u_2} [DivisionSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalSpace 𝕜] [(nhdsWithin 0 {0}ᶜ).NeBot] [ContinuousSMul 𝕜 E] : UniqueDiffOn 𝕜 Set.univ

theorem uniqueDiffWithinAt_of_mem_nhds {𝕜 : Type u_1} {E : Type u_2} [DivisionSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalSpace 𝕜] [(nhdsWithin 0 {0}ᶜ).NeBot] [ContinuousSMul 𝕜 E] {x : E} {s : Set E} [ContinuousAdd E] (h : s ∈ nhds x) : UniqueDiffWithinAt 𝕜 s x

theorem IsOpen.uniqueDiffWithinAt {𝕜 : Type u_1} {E : Type u_2} [DivisionSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalSpace 𝕜] [(nhdsWithin 0 {0}ᶜ).NeBot] [ContinuousSMul 𝕜 E] {x : E} {s : Set E} [ContinuousAdd E] (hs : IsOpen s) (xs : x ∈ s) : UniqueDiffWithinAt 𝕜 s x

theorem IsOpen.uniqueDiffOn {𝕜 : Type u_1} {E : Type u_2} [DivisionSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalSpace 𝕜] [(nhdsWithin 0 {0}ᶜ).NeBot] [ContinuousSMul 𝕜 E] {s : Set E} [ContinuousAdd E] (hs : IsOpen s) : UniqueDiffOn 𝕜 s