uniqueDiffWithinAt_closure — Mathlib

English

Unique differentiability at x with respect to closure(s) is equivalent to unique differentiability with respect to s.

Русский

Уникальная дифференцируемость в точке x относительно замыкания s эквивалентна уникальной дифференцируемости относительно самого s.

LaTeX

$$$ \\operatorname{UniqueDiffWithinAt}_{\\mathbb{k}}(\\overline{s},x) \\iff \\operatorname{UniqueDiffWithinAt}_{\\mathbb{k}}(s,x) $$$

Lean4

@[simp]
theorem uniqueDiffWithinAt_closure : UniqueDiffWithinAt 𝕜 (closure s) x ↔ UniqueDiffWithinAt 𝕜 s x := by
  simp [uniqueDiffWithinAt_iff]

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