apply_symm_apply_eq_coordChangeL — Mathlib

English

The unfolded coordinate change equals the compiled coordinate change expressed as a linear equivalence.

Русский

Развернутое изменение координат равняется записанному через линейную эквивалентность изменению координат.

LaTeX

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

Lean4

theorem apply_symm_apply_eq_coordChangeL (e e' : Trivialization F (π F E)) [e.IsLinear R] [e'.IsLinear R] {b : B}
    (hb : b ∈ e.baseSet ∩ e'.baseSet) (v : F) :
    e' (e.toOpenPartialHomeomorph.symm (b, v)) = (b, e.coordChangeL R e' b v) := by
  rw [e.mk_coordChangeL e' hb, e.mk_symm hb.1]

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