toPretrivialization_injective — Mathlib

English

The map e ↦ e.toPretrivialization is injective; different trivializations give different pretivializations.

Русский

Отображение e ↦ e.toPretrivialization инъективно; разные тривиализации дают разные претривиализации.

LaTeX

$$$\forall e,e',\ e.toPretrivialization = e'.toPretrivialization\Rightarrow e = e'$$$

Lean4

theorem toPretrivialization_injective : Function.Injective fun e : Trivialization F proj => e.toPretrivialization :=
  fun e e' h => by
  ext1
  exacts [OpenPartialHomeomorph.toPartialEquiv_injective (congr_arg Pretrivialization.toPartialEquiv h),
    congr_arg Pretrivialization.baseSet h]

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