apply_mk_symm

Mathlib.Topology.FiberBundle.Trivialization

URI: https://scilib.ai/kg/mathlib#Trivialization.apply_mk_symm

← MathLib Explorer

English

Applying e to the pair (b, e.symm b y) recovers the original pair (b, y).

Русский

Применение e к пару (b, e.symm b y) восстанавливает (b, y).

LaTeX

$$$e \\langle b, e.symm\\, b\\, y \\rangle = (b, y)$$$

Lean4

theorem apply_mk_symm (e : Trivialization F (π F E)) {b : B} (hb : b ∈ e.baseSet) (y : F) :
    e ⟨b, e.symm b y⟩ = (b, y) :=
  e.toPretrivialization.apply_mk_symm hb y

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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