English
For n,m with m ≤ n, the local invariant property holds: (contDiffGroupoid n I).LocalInvariantProp (contDiffGroupoid n I') (ContDiffWithinAtProp I I' m).
Русский
При n,m с m ≤ n выполняется локальная инвариантная свойств: contDiffGroupoid n I сохраняет ContDiffWithinAtProp I I' m.
LaTeX
$$$ (\contDiffGroupoid n I).LocalInvariantProp (\contDiffGroupoid n I') (ContDiffWithinAtProp I I' m) $$$
Lean4
/-- Property in the model space of a model with corners of being `C^n` within at set at a point,
when read in the model vector space. This property will be lifted to manifolds to define `C^n`
functions between manifolds. -/
def ContDiffWithinAtProp (n : WithTop ℕ∞) (f : H → H') (s : Set H) (x : H) : Prop :=
ContDiffWithinAt 𝕜 n (I' ∘ f ∘ I.symm) (I.symm ⁻¹' s ∩ range I) (I x)
