coordChangeL — Mathlib

English

The coordChange between two pretrivializations is linear on fibers and respects base changes.

Русский

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

LaTeX

$$$$ coordChange \colon a.pretrivializationAtlas \times a.pretrivializationAtlas \to (F\\to_L F) $$$$

Lean4

theorem coordChangeL (b : B) :
    (trivialization B F).coordChangeL 𝕜 (trivialization B F) b = ContinuousLinearEquiv.refl 𝕜 F :=
  by
  ext v
  rw [Trivialization.coordChangeL_apply']
  exacts [rfl, ⟨mem_univ _, mem_univ _⟩]

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