apply — Mathlib

English

The Simps.apply projection returns the trivialization as a function; i.e., the map equals e.

Русский

Проекция Simps.apply возвращает тривиализацию как функцию; то есть отображение совпадает с e.

LaTeX

$$$(\mathrm{Trivialization.Simps.apply}(\mathrm{proj}, e))(x) = e(x) \quad \text{for all } x \in Z$$$

Lean4

/-- See Note [custom simps projection] -/
def apply (proj : Z → B) (e : Trivialization F proj) : Z → B × F :=
  e

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