mk_d_2_0 — Mathlib

English

The (1,2) differential of mk equals the second given differential d1.

Русский

Дифференциал mk между ступенями 1 и 2 равен d1.

LaTeX

$$$\\big(\\mathrm{mk}\\; X_0 X_1 X_2 d_0 d_1 s succ\\big).d_{1 2} = d_1$$$

Lean4

@[simp]
theorem mk_d_2_0 : (mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 2 = d₁ :=
  by
  change ite (2 = 1 + 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.

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