symmL_continuousLinearMapAt — Mathlib

English

A linear trivialization yields a continuous linear equivalence between the fiber E_b and the model fiber F, with the inverse given by the backward map.

Русский

Линейная тривиализация порождает непрерывное линейное биективное отображение между фиброй $E_b$ и модельной фиброй $F$, обратное задаётся через обратное отображение.

LaTeX

$$$\exists\; E_b \cong_L[R] F\quad(\text{depending on } b)$, with inverse given by $\mathrm{symmL}$$$

Lean4

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

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