symmₗ_linearMapAt — Mathlib

English

There is a fiberwise linear inverse map symmₗ to the forward map for b ∈ e.baseSet, giving a linear map F → E_b that inverts the forward map on that fiber.

Русский

Существует линейное по фибрам обратное отображение symmₗ к прямому отображению для b в e.baseSet, образующее линейное отображение F → E_b, обратное на этом волокне.

LaTeX

$$$ e.symmₗ R b (e.linearMapAt R b y) = y $ when hb : b ∈ e.baseSet$$

Lean4

theorem symmₗ_linearMapAt (e : Pretrivialization 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 :=
  by
  rw [e.linearMapAt_def_of_mem hb]
  exact (e.linearEquivAt R b hb).left_inv y

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