instCoeFunForallProd — Mathlib

English

There is a canonical coercion from a Pretrivialization to functions, giving a map to Z → B × F.

Русский

Существует каноническое вложение из предтривиализации в функции, задающее отображение в Z → B × F.

LaTeX

$$$\text{CoeFun}(\text{Pretrivialization } F proj)\;:\; \text{Pretrivialization } F proj \to (Z \to B \times F)$$$

Lean4

instance : CoeFun (Pretrivialization F proj) fun _ => Z → B × F :=
  ⟨toFun'⟩

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