embeddingPiTangent_injective

Mathlib.Geometry.Manifold.WhitneyEmbedding

URI: https://scilib.ai/kg/mathlib#SmoothBumpCovering.embeddingPiTangent_injective

← MathLib Explorer

English

The mfderiv of embeddingPiTangent is injective on s.

Русский

mfderiv отображения embeddingPiTangent инъективен на s.

LaTeX

$$$\operatorname{ker}\,\mathrm{mfderiv}\big(I,\mathcal I(\mathbb R,\iota\to E\times\mathbb R)\, f.embeddingPiTangent\, x\big) = \{0\}$ for x in s$$

Lean4

theorem embeddingPiTangent_injective (f : SmoothBumpCovering ι I M) : Injective f.embeddingPiTangent :=
  injective_iff_injOn_univ.2 f.embeddingPiTangent_injOn

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru