linear — Mathlib

English

For a linear trivialization e and any b in its base set, the fiberwise map y ↦ (e⟨b,y⟩).2 is a linear map from the fiber E_b to the model space F.

Русский

Для линейной тривиализации e и любого b из её базового множества отображение вдоль волокна y ↦ (e⟨b,y⟩).2 есть линейное отображение из волокна E_b в модельное пространство F.

LaTeX

$$$\forall b \in e.baseSet,\; e.linearMapAt R b : E_b \to F \text{ is linear}.$$

Lean4

protected theorem linear [AddCommMonoid F] [Module R F] [∀ x, AddCommMonoid (E x)] [∀ x, Module R (E x)] [e.IsLinear R]
    {b : B} (hb : b ∈ e.baseSet) : IsLinearMap R fun y : E b => (e ⟨b, y⟩).2 :=
  Trivialization.IsLinear.linear b hb

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