English
If s ⊆ t in nhds of x, ContDiffWithinAtProp on s implies ContDiffWithinAtProp on t.
Русский
Если s ⊆ t в окрестности x, гладкость на s имплицирует гладкость на t.
LaTeX
$$$ (nhdsWithin x t ∋ s) \Rightarrow (ContDiffWithinAtProp I I' n f s x) \Rightarrow (ContDiffWithinAtProp I I' n f t x) $$$
Lean4
/-- Being `Cⁿ` in the model space is a local property, invariant under `Cⁿ` maps. Therefore,
it lifts nicely to manifolds. -/
theorem contDiffWithinAt_localInvariantProp_of_le (n m : WithTop ℕ∞) (hmn : m ≤ n) :
(contDiffGroupoid n I).LocalInvariantProp (contDiffGroupoid n I') (ContDiffWithinAtProp I I' m)
where
is_local {s x u f} u_open
xu :=
by
have : I.symm ⁻¹' (s ∩ u) ∩ range I = I.symm ⁻¹' s ∩ range I ∩ I.symm ⁻¹' u := by
simp only [inter_right_comm, preimage_inter]
rw [ContDiffWithinAtProp, ContDiffWithinAtProp, this]
symm
apply contDiffWithinAt_inter
have : u ∈ 𝓝 (I.symm (I x)) := by
rw [ModelWithCorners.left_inv]
exact u_open.mem_nhds xu
apply ContinuousAt.preimage_mem_nhds I.continuous_symm.continuousAt this
right_invariance' {s x f e} he hx
h := by
rw [ContDiffWithinAtProp] 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 ∩ range I := by simp only [hx, mfld_simps]
have := (mem_groupoid_of_pregroupoid.2 he).2.contDiffWithinAt this
convert (h.comp_inter _ (this.of_le hmn)).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 [mem_preimage, I.left_inv, e.mapsTo hx], ?_⟩
mfld_set_tac
congr_of_forall {s x f g} h hx
hf := by
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' {s x f e'} he' hs hx
h := by
rw [ContDiffWithinAtProp] at h ⊢
have A : (I' ∘ f ∘ I.symm) (I x) ∈ I'.symm ⁻¹' e'.source ∩ range I' := by simp only [hx, mfld_simps]
have := (mem_groupoid_of_pregroupoid.2 he').1.contDiffWithinAt A
convert (this.of_le hmn).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
