English
Two pretrivializations are equal if they agree on all point evaluations and on the inverse maps, and have the same base set.
Русский
Две предтривиализации равны, если они совпадают на всех точечных значениях и их обратные отображения совпадают, а также базовое множество совпадает.
LaTeX
$$$\forall x: Z,\ e(x)=e'(x) \;\land\; \forall x: Z,\ e.toPartialEquiv^{-1}(x)=e'.toPartialEquiv^{-1}(x) \;\land\; e.baseSet=e'.baseSet \Rightarrow e=e'$$$
Lean4
theorem ext {e e' : Pretrivialization F proj} (h₁ : ∀ x, e x = e' x)
(h₂ : ∀ x, e.toPartialEquiv.symm x = e'.toPartialEquiv.symm x) (h₃ : e.baseSet = e'.baseSet) : e = e' :=
by
ext1 <;> [ext1; exact h₃]
· apply h₁
· apply h₂
· rw [e.source_eq, e'.source_eq, h₃]
