mk_v — Mathlib

English

Extensionality principle for Cochain: two cochains are equal if all their v components agree on every triplet.

Русский

Принцип экстентности для коцепана: две коцепаны равны, если совпадают их компоненты v на всех троях.

LaTeX

$$$\forall z_1,z_2,\; (\forall p,q, hpq, z_1.v\; p\; q\; hpq = z_2.v\; p\; q\; hpq) \Rightarrow z_1 = z_2$$$

Lean4

@[simp]
theorem mk_v (v : ∀ (p q : ℤ) (_ : p + n = q), F.X p ⟶ G.X q) (p q : ℤ) (hpq : p + n = q) :
    (Cochain.mk v).v p q hpq = v p q hpq :=
  rfl

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