contMDiffWithinAt_inter' — Mathlib

English

If ContMDiffWithinAt holds for a set s and t is a subset of s, then ContMDiffWithinAt also holds for t.

Русский

Если ContMDiffWithinAt выполняется на s, то при подмножестве t ContMDiffWithinAt также выполняется.

LaTeX

$$$ ContMDiffWithinAt I I' n f s x \rightarrow t \subseteq s \Rightarrow ContMDiffWithinAt I I' n f t x $$$

Lean4

theorem contMDiffWithinAt_inter' (ht : t ∈ 𝓝[s] x) :
    ContMDiffWithinAt I I' n f (s ∩ t) x ↔ ContMDiffWithinAt I I' n f s x :=
  (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_inter' ht

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