contDiffWithinAtProp_self — Mathlib

English

A specialized self-reference lemma: ContDiffWithinAtProp self is equivalent to standard ContDiffWithinAt after changing model to self.

Русский

Лемма самоссылки: ContDiffWithinAtProp self эквивалентна обычной ContDiffWithinAt после замены модели на self.

LaTeX

$$$ ContDiffWithinAtProp (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s x \iff ContDiffWithinAt 𝕜 n f s x $$$

Lean4

theorem contDiffWithinAtProp_self {f : E → E'} {s : Set E} {x : E} :
    ContDiffWithinAtProp 𝓘(𝕜, E) 𝓘(𝕜, E') n f s x ↔ ContDiffWithinAt 𝕜 n f s x :=
  contDiffWithinAtProp_self_source

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