coordChangeL_symm_apply — Mathlib

English

The inverse of the coordinate change map between two linear trivializations equals the coordinate change map in opposite order on the swapped base sets.

Русский

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

LaTeX

$$$ (coordChangeL R e e' b)\!^{\! -1} = coordChangeL R e' e b $ when hb in intersection.$$

Lean4

theorem coordChangeL_symm_apply (e e' : Trivialization F (π F E)) [e.IsLinear R] [e'.IsLinear R] {b : B}
    (hb : b ∈ e.baseSet ∩ e'.baseSet) :
    ⇑(coordChangeL R e e' b).symm = (e'.linearEquivAt R b hb.2).symm.trans (e.linearEquivAt R b hb.1) :=
  congr_arg LinearEquiv.invFun (dif_pos hb)

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