English
If s is a globally UniqueDiffWithinAt set for 𝕜, then it remains UniqueDiffWithinAt for 𝕜'.
Русский
Если множество s имеет глобальную уникальную дифференцируемость относительно 𝕜, то она сохраняется при переходе к 𝕜'.
LaTeX
$$$ \\operatorname{UniqueDiffWithinAt}_{\\mathbb{k}}(s) \\Rightarrow \\operatorname{UniqueDiffWithinAt}_{\\mathbb{k}'}(s) $$$
Lean4
theorem span_tangentConeAt {s : Set G} (conv : Convex ℝ s) (hs : (interior s).Nonempty) {x : G} (hx : x ∈ closure s) :
Submodule.span ℝ (tangentConeAt ℝ s x) = ⊤ :=
by
rcases hs with ⟨y, hy⟩
suffices y - x ∈ interior (tangentConeAt ℝ s x)
by
apply (Submodule.span ℝ (tangentConeAt ℝ s x)).eq_top_of_nonempty_interior'
exact ⟨y - x, interior_mono Submodule.subset_span this⟩
rw [mem_interior_iff_mem_nhds]
replace hy : interior s ∈ 𝓝 y := IsOpen.mem_nhds isOpen_interior hy
apply mem_of_superset ((isOpenMap_sub_right x).image_mem_nhds hy)
rintro _ ⟨z, zs, rfl⟩
refine mem_tangentConeAt_of_openSegment_subset (Subset.trans ?_ interior_subset)
exact conv.openSegment_closure_interior_subset_interior hx zs
