surjective_proj — Mathlib

English

If the fiber is nonempty, the projection map is surjective onto the base space.

Русский

Если волокно непустое, проекция отображения проекции на базовое пространство сюръективна.

LaTeX

$$[Nonempty F] → Function.Surjective(π F E)$$

Lean4

/-- The projection from a fiber bundle with a nonempty fiber to its base is a surjective
map. -/
theorem surjective_proj [Nonempty F] : Function.Surjective (π F E) := fun b =>
  let ⟨p, _, hpb⟩ := (trivializationAt F E b).proj_surjOn_baseSet (mem_baseSet_trivializationAt F E b)
  ⟨p, hpb⟩

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