instIsManifoldComplexModelWithCornersSelfTopWithTopENat

English

The inclusion map 𝕀(ℂ) from the complex model to itself is C^n differentiable when restricted to the lower structure.

Русский

Включение 𝕀(ℂ) из модели комплексного пространства в саму себя является C^n гладким отображением в ограничении к соответствующей структуре.

LaTeX

$$$\text{contMDiff_coe}: \text{ContMDiff } 𝓘(\mathbb{C}) 𝓘(\mathbb{C}) n ((\uparrow): \mathbb{H} \to \mathbb{C})$$$

Lean4

instance : IsManifold 𝓘(ℂ) ω ℍ :=
  UpperHalfPlane.isOpenEmbedding_coe.isManifold_singleton

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