Index — Mathlib

English

The TotalSpace associated to a VectorBundleCore is naturally identified with Bundle.TotalSpace F Z.Fiber.

Русский

Обобщённое полное пространство для ядра векторного расслоения естественно идентифицируется с полным пространством оболочки F Z.Fiber.

LaTeX

$$$\text{TotalSpace } Z = \text{Bundle.TotalSpace } F Z.Fiber$$$

Lean4

/-- The index set of a vector bundle core, as a convenience function for dot notation -/
@[nolint unusedArguments]
def Index :=
  ι

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