mdifferentiableWithinAt_inter' — Mathlib

English

If hs holds for s and ht ∈ nhds x, then the intersection s ∩ t has the unique MDiff property at x.

Русский

Если у hs выполняется для s и ht ∈ nhds x, то пересечение s ∩ t имеет уникальное MDiff в x.

LaTeX

$$hs : UniqueMDiffWithinAt I s x → ht : t ∈ 𝓝 x → UniqueMDiffWithinAt I (s ∩ t) x$$

Lean4

theorem mdifferentiableWithinAt_inter' (ht : t ∈ 𝓝[s] x) :
    MDifferentiableWithinAt I I' f (s ∩ t) x ↔ MDifferentiableWithinAt I I' f s x := by
  rw [MDifferentiableWithinAt, MDifferentiableWithinAt,
    differentiableWithinAt_localInvariantProp.liftPropWithinAt_inter' ht]

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