proj_surjOn_baseSet

Mathlib.Topology.FiberBundle.Trivialization

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

English

If F is nonempty, proj maps e.source surjectively onto e.baseSet.

Русский

Если F непусто, отображение proj на e.source является сюръектом в e.baseSet.

LaTeX

$$$\mathrm{SurjOn}(\mathrm{proj}, e.source, e.baseSet)$$$

Lean4

theorem proj_surjOn_baseSet [Nonempty F] : Set.SurjOn proj e.source e.baseSet :=
  e.toPretrivialization.proj_surjOn_baseSet

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

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

Разделы

Аффилиация

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