coe_symmₗ

Mathlib.Topology.VectorBundle.Basic

URI: https://scilib.ai/kg/mathlib#Trivialization.coe_symmₗ

English

The underlying function of the fiberwise inverse symmₗ is exactly the basewise symm map: coe(symmₗ) = symm.

Русский

Функция-основание симмₗ совпадает с симм: coe(symmₗ) = symm.

LaTeX

$$$ \mathrm{coe} (e.symm_\ell R b) = e.symm b$.$$

Lean4

theorem coe_symmₗ (e : Trivialization F (π F E)) [e.IsLinear R] (b : B) : ⇑(e.symmₗ R b) = e.symm b :=
  rfl

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

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

Разделы

Аффилиация

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