symmₗ_linearMapAt — Mathlib

English

The linear structure transfers to the pretrivialization; if the trivialization is linear, so is its pretrivialization.

Русский

Линейная структура переходит к предтривиализации; если тривиализация линейна, то и её предтривиализация линейна.

LaTeX

$$$\text{Pretrivialization.IsLinear } R\ e.toPretrivialization$$$

Lean4

theorem symmₗ_linearMapAt (e : Trivialization F (π F E)) [e.IsLinear R] {b : B} (hb : b ∈ e.baseSet) (y : E b) :
    e.symmₗ R b (e.linearMapAt R b y) = y :=
  e.toPretrivialization.symmₗ_linearMapAt hb y

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