English
If for all e,e' in atlas H M the transition maps I ∘ e.symm ≫ₕ e' ∘ I.symm are C^n on the appropriate domain, then IsManifold I n M.
Русский
Если для всех e,e' из атласа переходные отображения удовлетворяют C^n на нужной области, то IsManifold.
LaTeX
$$$\forall e,e' \in atlas\ H M,\ ContDiffOn 𝕜 n (I \circ e^{-1} \circ e' \circ I^{-1}) (I^{-1} \;^{-1} (e^{-1} \circ e') .source \cap range I)$$$
Lean4
theorem isManifold_of_contDiffOn {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E]
[NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (M : Type*)
[TopologicalSpace M] [ChartedSpace H M]
(h :
∀ e e' : OpenPartialHomeomorph M H,
e ∈ atlas H M →
e' ∈ atlas H M → ContDiffOn 𝕜 n (I ∘ e.symm ≫ₕ e' ∘ I.symm) (I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range I)) :
IsManifold I n M where
compatible := by
haveI : HasGroupoid M (contDiffGroupoid n I) := hasGroupoid_of_pregroupoid _ (h _ _)
apply StructureGroupoid.compatible
