toPartialEquiv_injective — Mathlib

English

If the fiber is nonempty, then the map toPartialEquiv: Pretrivialization F proj → PartialEquiv Z (B × F) is injective.

Русский

Если волокно непустое, то отображение toPartialEquiv: Pretrivialization F proj → PartialEquiv Z (B × F) инъективно.

LaTeX

$$$[\text{Nonempty } F]\Rightarrow \forall e,e',\ toPartialEquiv(e)=toPartialEquiv(e') ⇔ e=e'$$$

Lean4

/-- If the fiber is nonempty, then the projection also is. -/
theorem toPartialEquiv_injective [Nonempty F] :
    Injective (toPartialEquiv : Pretrivialization F proj → PartialEquiv Z (B × F)) :=
  by
  refine fun e e' h ↦ ext' _ _ h ?_
  simpa only [fst_image_prod, univ_nonempty, target_eq] using congr_arg (Prod.fst '' PartialEquiv.target ·) h

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