instCoePretrivialization — Mathlib

English

Every trivialization determines a canonical pretivialization; there is a natural map toPretrivialization(e).

Русский

Каждая тривиализация определяет каноническую претривиализацию; существует естественное отображение e ↦ e.toPretrivialization.

LaTeX

$$$\operatorname{toPretrivialization}(e) \in \mathrm{Pretrivialization}(F, \mathrm{proj})$$$

Lean4

instance : Coe (Trivialization F proj) (Pretrivialization F proj) :=
  ⟨toPretrivialization⟩

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