mk_coordChangeL — Mathlib

English

A version of coordChangeL that unfolds coordChange; the equality holds by unfolding definitions.

Русский

Версия coordChangeL, которая полностью разворачивает coordChange; равенство выполняется развёртыванием определений.

LaTeX

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

Lean4

theorem mk_coordChangeL (e e' : Trivialization F (π F E)) [e.IsLinear R] [e'.IsLinear R] {b : B}
    (hb : b ∈ e.baseSet ∩ e'.baseSet) (y : F) : (b, coordChangeL R e e' b y) = e' ⟨b, e.symm b y⟩ :=
  by
  ext
  · rw [e.mk_symm hb.1 y, e'.coe_fst', e.proj_symm_apply' hb.1]
    rw [e.proj_symm_apply' hb.1]
    exact hb.2
  · exact e.coordChangeL_apply e' hb y

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