coordChange_linear_comp — Mathlib

English

For a VectorBundleCore Z, the composition of coordinate changes is associative: coordChange j k composed with coordChange i j equals coordChange i k on the appropriate domain.

Русский

У ядра VectorBundleCore координатные переходы удовлетворяют ассоциативности: coordChange j k ∘ coordChange i j = coordChange i k.

LaTeX

$$$\forall x \in Z.baseSet i \cap Z.baseSet j \cap Z.baseSet k,\ (Z.coordChange j k x) \circ (Z.coordChange i j x) = Z.coordChange i k x$$$

Lean4

theorem coordChange_linear_comp (i j k : ι) :
    ∀ x ∈ Z.baseSet i ∩ Z.baseSet j ∩ Z.baseSet k,
      (Z.coordChange j k x).comp (Z.coordChange i j x) = Z.coordChange i k x :=
  fun x hx => by
  ext v
  exact Z.coordChange_comp i j k x hx v

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