continuousLinearEquivAt_apply' — Mathlib

English

In a vector bundle core, the product structure ensures that the update of coordinates across trivializations respects composition of coord changes.

Русский

В ядре векторного расслоения переход координат по тривиализациям корректно согласуется с композицией переходов.

LaTeX

$$$\coordChange j k x \circ \coordChange i j x = \coordChange i k x$ for appropriate indices and base points$$

Lean4

@[simp]
theorem continuousLinearEquivAt_apply' (e : Trivialization F (π F E)) [e.IsLinear R] (x : TotalSpace F E)
    (hx : x ∈ e.source) : e.continuousLinearEquivAt R x.proj (e.mem_source.1 hx) x.2 = (e x).2 :=
  rfl

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