mk — Mathlib · SciLib

English

The component v of the constructed cochain mk satisfies a defining relation with respect to the underlying HomComplex.Cochain, i.e., the mk components match by construction.

Русский

Компонента v сконструированного коцепана mk удовлетворяет заданному соотношению относительно базовой Cоchain, т.е. компоненты mk соответствуют по построению.

LaTeX

$$$\mathrm{Cochain.mk}\; v\; .v p q hpq = v p q hpq$$$

Lean4

/-- A practical constructor for cochains. -/
def mk (v : ∀ (p q : ℤ) (_ : p + n = q), F.X p ⟶ G.X q) : Cochain F G n := fun ⟨p, q, hpq⟩ => v p q hpq

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