isLinear — Mathlib

English

For each i, the localTriv i is a linear trivialization in the sense that it preserves addition and scalar multiplication on fibers.

Русский

Для каждого i локальная тривиализация i сохраняет сумму и умножение на скаляры на волокнах.

LaTeX

$$$\forall i,\; (Z.localTriv i).IsLinear\, R$$$

Lean4

/-- The standard local trivializations of a vector bundle constructed from core are linear. -/
instance isLinear (i : ι) : (Z.localTriv i).IsLinear R where
  linear x
    _ :=
    { map_add := fun _ _ => by simp only [map_add, localTriv_apply, mfld_simps]
      map_smul := fun _ _ => by simp only [map_smul, localTriv_apply, mfld_simps] }

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