coe_linearMapAt — Mathlib

English

The coordinate change between two linear trivializations is given by the pair of linear equivalences on the common base set, provided b lies in the intersection of base sets.

Русский

Изменение координат между двумя линейными тривиализациями задаётся через пару линейных эквивалентностей на пересечении их базовых множеств.

LaTeX

$$$ \text{If } b \in e.baseSet \cap e'.baseSet,\; coordChangeL R e e' b = (e.linearEquivAt R b hb).symm.trans (e'.linearEquivAt R b hb').$$$

Lean4

theorem coe_linearMapAt (e : Trivialization F (π F E)) [e.IsLinear R] (b : B) :
    ⇑(e.linearMapAt R b) = fun y => if b ∈ e.baseSet then (e ⟨b, y⟩).2 else 0 :=
  e.toPretrivialization.coe_linearMapAt b

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