of_real

Mathlib.Analysis.RCLike.TangentCone

URI: https://scilib.ai/kg/mathlib#UniqueDiffOn.of_real

English

If hs holds for Real, then it holds for 𝕜: UniqueDiffOn 𝕜 s.

Русский

Если для Real верна уникальная дифференцируемость множества, то для 𝕜 тоже: UniqueDiffOn 𝕜 s.

LaTeX

$$$\\mathrm{UniqueDiffOn}_{\\mathbb{R}}(s) \\Rightarrow \\mathrm{UniqueDiffOn}_{\\mathbb{K}}(s)$$$

Lean4

theorem of_real (hs : UniqueDiffOn ℝ s) : UniqueDiffOn 𝕜 s := fun x hx ↦ (hs x hx).of_real

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru