contDiffWithinAt_inter' — Mathlib

English

If t is a neighborhood of x relative to s, then f is C^n within s ∩ t at x if and only if f is C^n within s at x.

Русский

Если t является окрестностью x внутри области s, то функция f имеет гладкость C^n на s ∩ t в точке x тогда и только тогда, когда она имеет гладкость C^n на s в x.

LaTeX

$$$ t \in \mathcal{N}_s(x) \;\Rightarrow\; \ContDiffWithinAt_{\mathbb{K}}(n,f;s\cap t;x) \;\Leftrightarrow\; \ContDiffWithinAt_{\mathbb{K}}(n,f;s;x) $$$

Lean4

theorem contDiffWithinAt_inter' (h : t ∈ 𝓝[s] x) : ContDiffWithinAt 𝕜 n f (s ∩ t) x ↔ ContDiffWithinAt 𝕜 n f s x :=
  contDiffWithinAt_congr_set (mem_nhdsWithin_iff_eventuallyEq.1 h).symm

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