lift_of — Mathlib

English

The lift at the direct limit sends the image of an element from a component to its corresponding image on the target, agreeing with the chosen system maps.

Русский

Лифт в прямом пределе отображает образ элемента из компонента в соответствующий образ на целевом объекте, согласуясь с переходными отображениями системы.

LaTeX

$$$\mathrm{lift}_{L,\iota,G,f,gHg}(\mathrm{of}_{L,\iota,G,f,i}(x)) = g_i(x).$$$

Lean4

theorem lift_of {i} (x : G i) : lift L ι G f g Hg (of L ι G f i x) = g i x := by simp

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