linearMapAt — Mathlib

English

The fiberwise linear map at b is exactly e.toPretrivialization.linearMapAt; it is the fiberwise map from E_b to F that is linear and equals the local coordinate on the base set.

Русский

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

LaTeX

$$$ e.linearMapAt R b = e.toPretrivialization.linearMapAt R b$.$$

Lean4

/-- A fiberwise linear map equal to `e` on `e.baseSet`. -/
protected def linearMapAt (e : Trivialization F (π F E)) [e.IsLinear R] (b : B) : E b →ₗ[R] F :=
  e.toPretrivialization.linearMapAt R b

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