uniqueDiffWithinAt_convex — Mathlib

English

If x ∈ s and 𝕜 ⊆ 𝕜', then tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜' s x.

Русский

Если x ∈ s и 𝕜 ⊆ 𝕜', тогда касательный конус в точке x относительно 𝕜 включён в касательный конус относительно 𝕜'.

LaTeX

$$$ \\text{tangentConeAt}_{\\mathbb{k}}(s,x) \\subseteq \\text{tangentConeAt}_{\\mathbb{k}'}(s,x) $$$

Lean4

/-- In a real vector space, a convex set with nonempty interior is a set of unique
differentiability at every point of its closure. -/
theorem uniqueDiffWithinAt_convex {s : Set G} (conv : Convex ℝ s) (hs : (interior s).Nonempty) {x : G}
    (hx : x ∈ closure s) : UniqueDiffWithinAt ℝ s x := by
  simp [uniqueDiffWithinAt_iff, conv.span_tangentConeAt hs hx, hx]

Похожие утверждения