copy — Mathlib

English

Given a generalized loop f and a function g equal to f, one can package g as the new underlying loop by copying f with g as the new pointwise map.

Русский

Пусть дан обобщённый цикл f и функция g такая, что g=f. Тогда можно получить новый обобщённый цикл, копируя f и заменяя его мапу на g.

LaTeX

$$$\\text{GenLoop.copy} (f,g,h) = \\text{GenLoop N X x with underlying map } g$$$

Lean4

/-- Copy of a `GenLoop` with a new map from the unit cube equal to the old one.
  Useful to fix definitional equalities. -/
def copy (f : Ω^ N X x) (g : (I^N) → X) (h : g = f) : Ω^ N X x :=
  ⟨⟨g, h.symm ▸ f.1.2⟩, by convert f.2⟩

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