topologicalSpaceFiber

Mathlib.Topology.FiberBundle.Basic

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

English

For a fiber bundle core Z and a base point x, the fiber is the type F (independent of x).

Русский

Для ядра Z и точки базиса x волокно равно фиксированному типу F, независимо от x.

LaTeX

$$Fiber (Z) = F$$

Lean4

instance topologicalSpaceFiber (x : B) : TopologicalSpace (Z.Fiber x) :=
  ‹_›

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

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

Разделы

Аффилиация

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