uniqueDiffOn — Mathlib

English

If s is open, then s has unique differentiability at every point, i.e., UniqueDiffOn 𝕜 s.

Русский

Если s открыто, то в каждой точке множества s выполняется уникальная дифференцируемость.

LaTeX

$$$ \\text{IsOpen}(s) \\Rightarrow \\operatorname{UniqueDiffOn}_{\\mathbb{k}}(s) $$$

Lean4

theorem uniqueDiffOn (hs : IsOpen s) : UniqueDiffOn 𝕜 s := fun _ hx => IsOpen.uniqueDiffWithinAt hs hx

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