proj_clift

Mathlib.Topology.FiberBundle.Trivialization

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

English

For any hx ∈ T.baseSet, the projection of T.lift z hx equals hx.

Русский

Пусть hx ∈ базового множества T, тогда проекция T.lift z hx равна hx.

LaTeX

$$$$\operatorname{proj}(T.lift(z, b))=b\quad\text{whenever } b\in T.baseSet.$$$$

Lean4

theorem proj_clift : proj (T.clift (e, γ) i) = γ i := by simp [clift, liftCM, proj_lift]

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

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

Разделы

Аффилиация

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