English
The local invariance property of differentiability within at under smooth changes of charts is established.
Русский
Локальная инвариантность дифференцируемости внутри при переходах между гладкими координатными картами.
LaTeX
$$$\text{differentiableWithinAt_localInvariantProp } :\ (contDiffGroupoid 1 I).LocalInvariantProp (contDiffGroupoid 1 I') (DifferentiableWithinAtProp I I')$$$
Lean4
/-- Being differentiable in the model space is a local property, invariant under smooth maps.
Therefore, it will lift nicely to manifolds. -/
theorem differentiableWithinAt_localInvariantProp :
(contDiffGroupoid 1 I).LocalInvariantProp (contDiffGroupoid 1 I') (DifferentiableWithinAtProp I I') :=
{ is_local := by
intro s x u f u_open xu
have : I.symm ⁻¹' (s ∩ u) ∩ Set.range I = I.symm ⁻¹' s ∩ Set.range I ∩ I.symm ⁻¹' u := by
simp only [Set.inter_right_comm, Set.preimage_inter]
rw [DifferentiableWithinAtProp, DifferentiableWithinAtProp, this]
symm
apply differentiableWithinAt_inter
have : u ∈ 𝓝 (I.symm (I x)) := by
rw [ModelWithCorners.left_inv]
exact u_open.mem_nhds xu
apply I.continuous_symm.continuousAt this
right_invariance' := by
intro s x f e he hx h
rw [DifferentiableWithinAtProp] at h ⊢
have : I x = (I ∘ e.symm ∘ I.symm) (I (e x)) := by simp only [hx, mfld_simps]
rw [this] at h
have : I (e x) ∈ I.symm ⁻¹' e.target ∩ Set.range I := by simp only [hx, mfld_simps]
have := (mem_groupoid_of_pregroupoid.2 he).2.contDiffWithinAt this
convert (h.comp' _ (this.differentiableWithinAt le_rfl)).mono_of_mem_nhdsWithin _ using 1
· ext y; simp only [mfld_simps]
refine
mem_nhdsWithin.mpr
⟨I.symm ⁻¹' e.target, e.open_target.preimage I.continuous_symm, by
simp_rw [Set.mem_preimage, I.left_inv, e.mapsTo hx], ?_⟩
mfld_set_tac
congr_of_forall := by
intro s x f g h hx hf
apply hf.congr
· intro y hy
simp only [mfld_simps] at hy
simp only [h, hy, mfld_simps]
· simp only [hx, mfld_simps]
left_invariance' := by
intro s x f e' he' hs hx h
rw [DifferentiableWithinAtProp] at h ⊢
have A : (I' ∘ f ∘ I.symm) (I x) ∈ I'.symm ⁻¹' e'.source ∩ Set.range I' := by simp only [hx, mfld_simps]
have := (mem_groupoid_of_pregroupoid.2 he').1.contDiffWithinAt A
convert (this.differentiableWithinAt le_rfl).comp _ h _
· ext y; simp only [mfld_simps]
· intro y hy; simp only [mfld_simps] at hy; simpa only [hy, mfld_simps] using hs hy.1 }
