contDiffWithinAtProp_self_target — Mathlib

English

Self-target version: ContDiffWithinAtProp I (model with corners) n f s x is equivalent to ContDiffWithinAt 𝕜 n (f ∘ I.symm) (I.symm⁻¹' s ∩ range I) (I x).

Русский

Самоцелевая версия: ContDiffWithinAtProp I (modelWithCornersSelf) n f s x эквивалентно ContDiffWithinAt 𝕜 n (f ∘ I.symm) ...

LaTeX

$$$ ContDiffWithinAtProp I 𝓘(𝕜, E') n f s x \iff ContDiffWithinAt 𝕜 n (f \circ I.symm) (I.symm \backslash s ∩ range I) (I x) $$$

Lean4

theorem contDiffWithinAtProp_self_target {f : H → E'} {s : Set H} {x : H} :
    ContDiffWithinAtProp I 𝓘(𝕜, E') n f s x ↔ ContDiffWithinAt 𝕜 n (f ∘ I.symm) (I.symm ⁻¹' s ∩ range I) (I x) :=
  Iff.rfl

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