coe_coordChangeL — Mathlib

English

The coordChangeL and its variant coordChangeL' are equal when both are defined; they express the same fiberwise coordinate change on the intersection.

Русский

Изменение координат coordChangeL и его вариант coordChangeL' совпадают на пересечении областей определения.

LaTeX

$$$ coordChangeL R e e' b = (e.linearEquivAt R b hb)^{-1} \circ (e'.linearEquivAt R b hb').$$$

Lean4

theorem coe_coordChangeL (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) = (e.linearEquivAt R b hb.1).symm.trans (e'.linearEquivAt R b hb.2) :=
  congr_arg (fun f : F ≃ₗ[R] F ↦ ⇑f) (dif_pos hb)

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