localTrivAt_apply_mk — Mathlib

English

For hb in baseSet, the value of the local trivialization's continuous linear map at b equals the core’s coordChange between the appropriate indices.

Русский

Для hb в базовом множестве, значение непрерывного линейного отображения локальной тривиализации в точке b равно переходу coordChange ядра между соответствующими индексами.

LaTeX

$$$\text{if } hb:\; b \in (Z.localTriv i).baseSet,\; (Z.localTriv i).continuousLinearMapAt\; R\; b = Z.coordChange (Z.indexAt b) i b$$$

Lean4

@[simp, mfld_simps]
theorem localTrivAt_apply_mk (b : B) (a : F) : Z.localTrivAt b ⟨b, a⟩ = ⟨b, a⟩ :=
  Z.localTrivAt_apply _

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