linearEquivAt_symm_apply — Mathlib

English

The inverse of the linear fiber map acts by taking the second coordinate of the trivialization: the symm of linearEquivAt sends a model vector back to the fiber component.

Русский

Обратное линейного отображения вдоль волокна переводит вектор из модельного пространства обратно в вторую компоненту тривиализации.

LaTeX

$$$ (e.linearEquivAt R b hb)^{-1}(v) = e.symm b v,\; v\in F$.$$

Lean4

@[simp]
theorem linearEquivAt_symm_apply (e : Trivialization F (π F E)) [e.IsLinear R] (b : B) (hb : b ∈ e.baseSet) (v : F) :
    (e.linearEquivAt R b hb).symm v = e.symm b v :=
  rfl

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