Fiber — Mathlib

English

A VectorBundleCore provides the data for a vector bundle, including base space, fibers, and coordinate changes, and can be used to reconstruct a FiberBundleCore.

Русский

Ядро векторного расслоения задаёт данные для расслоения: базовую базу, волокна и переходы координат, и может быть использовано для реконструкции FiberBundleCore.

LaTeX

$$$Z : VectorBundleCore R B F ι$ encodes base, fibers, coordChange$$

Lean4

/-- The fiber of a vector bundle core, as a convenience function for dot notation and
typeclass inference -/
@[nolint unusedArguments]
def Fiber : B → Type _ :=
  Z.toFiberBundleCore.Fiber

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