standardσ_cons — Mathlib

English

The equality standardσ (a :: L) h = standardσ L (by grind) ≫ σ(Fin.ofNat (m₂+1) a) expresses compatibility with cons.

Русский

Согласованность стандартσ при добавлении в голову списка.

LaTeX

$$$\\\\text{standardσ}(a :: L) = \\text{standardσ}(L) \\\\circ σ( F i n . ofNat( m_2+1 )\\ a )$$$

Lean4

@[simp, reassoc]
theorem standardσ_cons (L : List ℕ) (a : ℕ) {m₁ m₂ : ℕ} (h : m₂ + (a :: L).length = m₁) :
    standardσ (L.cons a) h = standardσ L (by grind) ≫ σ (Fin.ofNat _ a) :=
  rfl

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