eq_trivialization — Mathlib

English

If e is a trivialization for the trivial bundle and belongs to the trivial atlas, then e equals the canonical trivialization.

Русский

Если e — тривиализация тривиального расслоения и принадлежит тривиальному атласу, то e совпадает с канонической тривиализацией.

LaTeX

$$$\forall e\, [i : \mathrm{MemTrivializationAtlas}(e)],\ e = \mathrm{trivialization}(B,F)$$$

Lean4

theorem eq_trivialization (e : Trivialization F (π F(Bundle.Trivial B F))) [i : MemTrivializationAtlas e] :
    e = trivialization B F :=
  i.out

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