mk'_d_1_0 — Mathlib

English

Re-statement of mk'_d_1_0: the 0→1 differential for mk' equals d0.

Русский

Повторно сформулирован дифференциал 0→1 для mk' равен d0.

LaTeX

$$$\\big(\\mathrm{mk}'\\; X_0 X_1 d_0 succ'\\big).d_{0 1} = d_0$$$

Lean4

@[simp]
theorem mk'_d_1_0 : (mk' X₀ X₁ d₀ succ').d 0 1 = d₀ :=
  by
  change ite (1 = 0 + 1) (d₀ ≫ 𝟙 X₁) 0 = d₀
  rw [if_pos rfl, Category.comp_id]
    -- TODO simp lemmas for the inductive steps? It's not entirely clear that they are needed.

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