English
The tangent bundle core (tangentBundleCore I M) is ContMDiff along I at level n, given that I is a manifold of level (n+1).
Русский
Ядро касательного расслоения (tangentBundleCore I M) является ContMDiff вдоль I на уровне n, если I задаёт многообразие уровня (n+1).
LaTeX
$$ContMDiff tangentBundleCore I M I n$$
Lean4
theorem isContMDiff [h : IsManifold I (n + 1) M] :
haveI : IsManifold I 1 M := .of_le (n := n + 1) le_add_self
(tangentBundleCore I M).IsContMDiff I n :=
by
have : IsManifold I n M := .of_le (n := n + 1) (le_self_add)
refine ⟨fun i j => ?_⟩
rw [contMDiffOn_iff_source_of_mem_maximalAtlas (subset_maximalAtlas i.2), contMDiffOn_iff_contDiffOn]
· refine ((contDiffOn_fderiv_coord_change (I := I) i j).congr fun x hx => ?_).mono ?_
· rw [PartialEquiv.trans_source'] at hx
simp_rw [Function.comp_apply, tangentBundleCore_coordChange, (i.1.extend I).right_inv hx.1]
· exact (i.1.extend_image_source_inter j.1).subset
· apply inter_subset_left
