coe_fst' — Mathlib

English

The value of the constructed trivialization at x equals the value of e at x; i.e., the constructor preserves evaluation.

Русский

Значение сконструированной тривиализации в точке x равно значению e в точке x; конструктор сохраняет значение.

LaTeX

$$$(\mathrm{Trivialization.mk}\ e\ i\ j\ k\ l\ m)(x) = e(x)$$$

Lean4

theorem coe_fst' (ex : proj x ∈ e.baseSet) : (e x).1 = proj x :=
  e.coe_fst (e.mem_source.2 ex)

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