isManifold — Mathlib

English

Analytic manifolds are smooth manifolds; the analytic structure implies a compatible smooth structure.

Русский

Аналитические многообразия являются гладкими многообразиями; аналитическая структура совместима со гладкой структурой.

LaTeX

$$IsManifold I ∞ M, if M has ChartedSpace structure with analytic atlas, then M is a smooth manifold with the induced structure.$$

Lean4

/-- Analytic manifolds are smooth manifolds. -/
instance isManifold [ChartedSpace H M] [cm : AnalyticManifold I M] : IsManifold I ∞ M where
  compatible hf
    hg :=
    ⟨(cm.compatible hf hg).1.contDiffOn I.uniqueDiffOn_preimage_source,
      (cm.compatible hg hf).1.contDiffOn I.uniqueDiffOn_preimage_source⟩

Похожие утверждения