proj_lift

Mathlib.Topology.FiberBundle.Trivialization

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

English

If b ∈ T.baseSet, then proj(T.lift z b) = b.

Русский

Если b ∈ базовое множество T, то проекция T.lift z b равна b.

LaTeX

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

Lean4

theorem proj_lift (hx : b ∈ T.baseSet) : proj (T.lift z b) = b :=
  T.proj_symm_apply <| T.mem_target.2 hx

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

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

Разделы

Аффилиация

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