coe_copy — Mathlib

English

The underlying function of a copied generalized loop is exactly the new map g; i.e., the coefficient/coe of copy(f,g,h) equals g.

Русский

У копированного обобщённого цикла основанная мапа равна новой функции g; то есть коe копирования совпадает с g.

LaTeX

$$$\\mathrm{GenLoop.instFunLike.coe}(\\mathrm{GenLoop.copy}(f,g,h)) = g$$$

Lean4

theorem coe_copy (f : Ω^ N X x) {g : (I^N) → X} (h : g = f) : ⇑(copy f g h) = g :=
  rfl

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