contDiffWithinAtProp_self_source — Mathlib

English

For each n, the groupoid invariance holds globally: ContDiffWithinAtProp is locally invariant under the ContDiffGroupoid.

Русский

Для каждого n свойство локальной инвариантности сохраняется под ContDiffGroupoid.

LaTeX

$$$ (\contDiffGroupoid n I).LocalInvariantProp (\contDiffGroupoid n I') (ContDiffWithinAtProp I I' n) $$$

Lean4

theorem contDiffWithinAtProp_self_source {f : E → H'} {s : Set E} {x : E} :
    ContDiffWithinAtProp 𝓘(𝕜, E) I' n f s x ↔ ContDiffWithinAt 𝕜 n (I' ∘ f) s x := by
  simp_rw [ContDiffWithinAtProp, modelWithCornersSelf_coe, range_id, inter_univ, modelWithCornersSelf_coe_symm,
    CompTriple.comp_eq, preimage_id_eq, id_eq]

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