symmₗ — Mathlib

English

There is a fiberwise linear map symmₗ which serves as a linear inverse to the trivialization on fibers E_b.

Русский

Существует волокно-ориентированное линейное отображение symmₗ, которое действует как линейное обратное к тривиализации на волокне.

LaTeX

$$$ e.symm_\ell R b : F \to_\! R E_b \quad (b\in B).$$$

Lean4

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

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