linearEquivAt_apply — Mathlib

English

The application of the linear equivalence at b to a vector v in E_b yields the second component of the trivialization on (b,v).

Русский

Применение линейной эквивалентности в точке b к вектору v в E_b даёт вторую компоненту тривиализации в паре (b, v).

LaTeX

$$$ e.linearEquivAt R b hb (v) = (e ⟨b, v⟩).2, \quad v \in E_b.$$

Lean4

@[simp]
theorem linearEquivAt_apply (e : Trivialization F (π F E)) [e.IsLinear R] (b : B) (hb : b ∈ e.baseSet) (v : E b) :
    e.linearEquivAt R b hb v = (e ⟨b, v⟩).2 :=
  rfl

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