embeddingPiTangent — Mathlib

English

There exists a smooth embedding into a finite-dimensional Euclidean space obtained via an embedding that records tangent data by collecting values of a bump-covering.

Русский

Существует гладкое вложение в конечномерное евклидово пространство, полученное из поля плавного «бамп-покрытия», фиксирующее касательное данные.

LaTeX

$$$\exists \iota, E, H, I, M, n, e \text{ such that } e = f\!\circ \text{embeddingPiTangent} \text{ is a smooth embedding into } \mathbb{R}^n.$$$

Lean4

/-- Smooth embedding of `M` into `(E × ℝ) ^ ι`. -/
def embeddingPiTangent : C^∞⟮I, M; 𝓘(ℝ, ι → E × ℝ), ι → E × ℝ⟯
    where
  val x i := (f i x • extChartAt I (f.c i) x, f i x)
  property := contMDiff_pi_space.2 fun i => ((f i).contMDiff_smul contMDiffOn_extChartAt).prodMk_space (f i).contMDiff

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