totalSpaceMk_isInducing

Mathlib.Topology.FiberBundle.Basic

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

English

The total space construction map TotalSpace.mk b is an inducing map.

Русский

Отображение TotalSpace.mk b является индукционирующим отображением.

LaTeX

$$$$ \\text{IsInducing}(\\mathrm{TotalSpace.mk}\\, b). $$$$

Lean4

theorem totalSpaceMk_isInducing : IsInducing (@TotalSpace.mk B F E b) :=
  totalSpaceMk_isInducing' b

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

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

Разделы

Аффилиация

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