mdifferentiable_coe — Mathlib

English

The inclusion map ℍ → ℂ is MDifferentiable between the complex model spaces.

Русский

Включение ℍ → ℂ является MDifferentiable между соответствующими моделями комплексного пространства.

LaTeX

$$$\text{mdifferentiable_coe}: \text{MDifferentiable } 𝓘(\mathbb{C}) 𝓘(\mathbb{C}) ((\uparrow) : \mathbb{H} \to \mathbb{C})$$$

Lean4

/-- The inclusion map `ℍ → ℂ` is a differentiable map of manifolds. -/
theorem mdifferentiable_coe : MDifferentiable 𝓘(ℂ) 𝓘(ℂ) ((↑) : ℍ → ℂ) :=
  contMDiff_coe.mdifferentiable le_top

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