contDiffWithinAt_inter — Mathlib

English

If t is a neighborhood of x, then ContDiffWithinAt on s ∩ t at x is equivalent to ContDiffWithinAt on s at x.

Русский

Если t является окрестностью x в пространстве, то ContDiffWithinAt на s ∩ t в x эквивалентно ContDiffWithinAt на s в x.

LaTeX

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

Lean4

theorem contDiffWithinAt_inter (h : t ∈ 𝓝 x) : ContDiffWithinAt 𝕜 n f (s ∩ t) x ↔ ContDiffWithinAt 𝕜 n f s x :=
  contDiffWithinAt_inter' (mem_nhdsWithin_of_mem_nhds h)

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