linearMapAt_def_of_notMem — Mathlib

English

The function e.linearMapAt R e b assigns the fiberwise linear map y ↦ (e⟨b,y⟩).2, and this is the linear map from E_b to F; it equals this second component when b is in the base set.

Русский

Функция e.linearMapAt R e b задаёт линейное вдоль волокна отображение y → (e⟨b,y⟩).2, являющееся линейным отображением E_b → F; при b ∈ базовое множество совпадает с двумя компонентами.

LaTeX

$$$ e.linearMapAt R b = \text{the linear map } E_b \to F, \; y \mapsto (e ⟨b,y⟩).2.$$$

Lean4

theorem linearMapAt_def_of_notMem (e : Trivialization F (π F E)) [e.IsLinear R] {b : B} (hb : b ∉ e.baseSet) :
    e.linearMapAt R b = 0 :=
  dif_neg hb

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