coordChangeL_apply — Mathlib

English

The coordinate change map is invertible along the base intersection; its inverse corresponds to swapping the roles of e and e'.

Русский

Изменение координат взаимно однозначно на пересечении базовых областей; его обратное отображение меняет местами роли e и e'.

LaTeX

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

Lean4

theorem coordChangeL_apply (e e' : Trivialization F (π F E)) [e.IsLinear R] [e'.IsLinear R] {b : B}
    (hb : b ∈ e.baseSet ∩ e'.baseSet) (y : F) : coordChangeL R e e' b y = (e' ⟨b, e.symm b y⟩).2 :=
  congr_fun (coe_coordChangeL e e' hb) y

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