totalSpaceMk_isEmbedding

Mathlib.Topology.FiberBundle.Basic

URI: https://scilib.ai/kg/mathlib#FiberBundle.totalSpaceMk_isEmbedding

English

For each base point x, the map TotalSpace.mk x is an embedding.

Русский

Для каждой базовой точки x отображение TotalSpace.mk x является вложением (эмбеддингом).

LaTeX

$$IsEmbedding(\operatorname{TotalSpace.mk} x)$$

Lean4

theorem totalSpaceMk_isEmbedding (x : B) : IsEmbedding (@TotalSpace.mk B F E x) :=
  ⟨totalSpaceMk_isInducing F E x, TotalSpace.mk_injective x⟩

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

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

Разделы

Аффилиация

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