localTrivAt_apply_mk

Mathlib.Topology.FiberBundle.Basic

URI: https://scilib.ai/kg/mathlib#FiberBundleCore.localTrivAt_apply_mk

English

The local trivialization at b applied to the pair (b,a) yields (b,a).

Русский

Применение локальной тривиализации к пару (b,a) даёт (b,a).

LaTeX

$$$\\big(\\text{localTrivAt } b\\big)\\, \\langle b,a \\rangle = \\langle b,a \\rangle$$$

Lean4

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

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

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

Разделы

Аффилиация

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