Base

Mathlib.Topology.FiberBundle.Basic

URI: https://scilib.ai/kg/mathlib#FiberBundleCore.Base

← MathLib Explorer

English

The index of a fiber bundle core is the index set ι.

Русский

Индекс ядра фибробандла совпадает с индексным множеством ι.

LaTeX

$$Index (Z : FiberBundleCore ι B F) = ι$$

Lean4

/-- The base space of a fiber bundle core, as a convenience function for dot notation -/
@[nolint unusedArguments, reducible]
def Base (_Z : FiberBundleCore ι B F) :=
  B

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

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

Разделы

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

Аффилиация

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