mkCoinductiveAux₂_add_one — Mathlib

English

A simplification lemma describing how mkCoinductiveAux₂ behaves when increasing the index by one, expressed as equality of two recursively defined diagrams.

Русский

Лемма упрощения, описывающая поведение mkCoinductiveAux₂ при приращении индекса на единицу: равенство двух рекурсивно определённых диаграмм.

LaTeX

$$mkCoinductiveAux₂ (n+1) = ⟨I.1 ≫ (Q.xPrevIso rfl).inv, (P.xNextIso rfl).hom ≫ I.2.1, ...⟩$$

Lean4

@[simp]
theorem mkCoinductiveAux₂_add_one (n) :
    mkCoinductiveAux₂ e zero comm_zero one comm_one succ (n + 1) =
      letI I := mkCoinductiveAux₁ e zero one comm_one succ n
      ⟨I.1 ≫ (Q.xPrevIso rfl).inv, (P.xNextIso rfl).hom ≫ I.2.1, by simpa using I.2.2⟩ :=
  rfl

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