surjective_proj — Mathlib

English

Let the fiber be nonempty and the bundle be a trivial fiber bundle with projection proj: Z → B. Then the projection is surjective: for every b ∈ B there exists z ∈ Z with proj(z) = b.

Русский

Пусть волокно непустое, пучок тривиален, проекция proj: Z → B. Тогда проекция сюръективна: для каждого b ∈ B существует z ∈ Z, такое что proj(z) = b.

LaTeX

$$$\forall b \in B,\ \exists z \in Z,\ proj(z) = b$$$

Lean4

/-- The projection from a trivial fiber bundle to its base is surjective. -/
protected theorem surjective_proj [Nonempty F] (h : IsHomeomorphicTrivialFiberBundle F proj) :
    Function.Surjective proj := by
  obtain ⟨e, rfl⟩ := h.proj_eq
  exact Prod.fst_surjective.comp e.surjective

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