contDiffWithinAtProp_id — Mathlib

English

Equivalence of ContDiffWithinAtProp when using modelWithCornersSelf maps.

Русский

Эквивалентность ContDiffWithinAtProp при использовании self-моделей.

LaTeX

$$$ ContDiffWithinAtProp I 𝓘(\mathbb{k}, E') n f s x \iff ContDiffWithinAt 𝕜 n f s x $$$

Lean4

theorem contDiffWithinAtProp_id (x : H) : ContDiffWithinAtProp I I n id univ x :=
  by
  simp only [ContDiffWithinAtProp, id_comp, preimage_univ, univ_inter]
  have : ContDiffWithinAt 𝕜 n id (range I) (I x) := contDiff_id.contDiffAt.contDiffWithinAt
  refine this.congr (fun y hy => ?_) ?_
  · simp only [ModelWithCorners.right_inv I hy, mfld_simps]
  · simp only [mfld_simps]

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