comp_continuousLinearEquivAt_eq_coord_change

English

The forward map of a trivialization, viewed as a continuous linear isomorphism, acts as the evaluation map on fibers.

Русский

Переход линейной эквивалентности тривиализации действует как отображение отображения координат на фибре.

LaTeX

$$$\forall b,\ \text{the map } e.continuousLinearEquivAt(R,b)\text{ sends } E_b \text{ onto } F$ continuously$$

Lean4

theorem comp_continuousLinearEquivAt_eq_coord_change (e e' : Trivialization F (π F E)) [e.IsLinear R] [e'.IsLinear R]
    {b : B} (hb : b ∈ e.baseSet ∩ e'.baseSet) :
    (e.continuousLinearEquivAt R b hb.1).symm.trans (e'.continuousLinearEquivAt R b hb.2) = coordChangeL R e e' b :=
  by
  ext v
  rw [coordChangeL_apply e e' hb]
  rfl

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