uniqueDiffOn_convex_of_isRCLikeNormedField

English

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

Русский

В реальном или комплексном векторном пространстве выпуклое множество с непустым Interior обладает уникальной дифференцируемостью.

LaTeX

$$$Convex\\ Real\\ s \\to (\\operatorname{interior}(s)).Nonempty \\to \\mathrm{UniqueDiffOn}_{\\mathbb{K}}(s)$$$

Lean4

/-- In a real or complex vector space, a convex set with nonempty interior is a set of unique
differentiability. -/
theorem uniqueDiffOn_convex_of_isRCLikeNormedField (conv : Convex ℝ s) (hs : (interior s).Nonempty) :
    UniqueDiffOn 𝕜 s :=
  UniqueDiffOn.of_real (uniqueDiffOn_convex conv hs)

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