of_real — Mathlib

English

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

Русский

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

LaTeX

$$$\\forall s x,\\, \\mathrm{UniqueDiffWithinAt}_{\\mathbb{R}}(s,x) \\Rightarrow \\mathrm{UniqueDiffWithinAt}_{\\mathbb{K}}(s,x)$$$

Lean4

theorem of_real (hs : UniqueDiffWithinAt ℝ s x) : UniqueDiffWithinAt 𝕜 s x :=
  by
  letI := h𝕜.rclike
  exact hs.mono_field

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