hasMFDerivWithinAt_inter' — Mathlib

English

If t is a neighborhood of x inside s, then HasMFDerivWithinAt I I' f (s ∩ t) x f' holds iff HasMFDerivWithinAt I I' f s x f'.

Русский

Пусть t является окрестностью x внутри s; тогда HasMFDerivWithinAt I I' f (s ∩ t) x f' эквивалентно HasMFDerivWithinAt I I' f s x f'.

LaTeX

$$$\text{t} \in \mathcal{N}_s(x) \;:\; HasMFDerivWithinAt I I' f (s \cap t) x f' \iff HasMFDerivWithinAt I I' f s x f'$$$

Lean4

theorem hasMFDerivWithinAt_inter' (h : t ∈ 𝓝[s] x) :
    HasMFDerivWithinAt I I' f (s ∩ t) x f' ↔ HasMFDerivWithinAt I I' f s x f' :=
  by
  rw [HasMFDerivWithinAt, HasMFDerivWithinAt, extChartAt_preimage_inter_eq, hasFDerivWithinAt_inter',
    continuousWithinAt_inter' h]
  exact extChartAt_preimage_mem_nhdsWithin h

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