localTriv_apply — Mathlib

English

The standard local trivializations of the vector bundle constructed from the core are linear, i.e., they are R-linear maps on fibers.

Русский

Стандартные локальные тривиализации векторного расслоения, построенного из ядра, являются линейными по структуре над полем R.

LaTeX

$$$\forall i, \; (Z.localTriv i).\mathrm{IsLinear}\, \mathbb{R}$$$

Lean4

@[simp, mfld_simps]
theorem localTriv_apply {i : ι} (p : Z.TotalSpace) :
    (Z.localTriv i) p = ⟨p.1, Z.coordChange (Z.indexAt p.1) i p.1 p.2⟩ :=
  rfl

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