localTrivAt_def

Mathlib.Topology.VectorBundle.Basic

URI: https://scilib.ai/kg/mathlib#VectorBundleCore.localTrivAt_def

English

The two notions of local trivialization at b agree: localTrivAt b equals localTriv (indexAt b).

Русский

Пусть локальная тривиализацияAt в точке b совпадает с локальной тривиализацией по indexAt(b).

LaTeX

$$$Z.localTrivAt b = Z.localTriv (Z.indexAt b)$$$

Lean4

@[simp, mfld_simps]
theorem localTrivAt_def : Z.localTriv (Z.indexAt b) = Z.localTrivAt b :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru