drop_drop — Mathlib

English

Dropping twice along a right association returns the original drop.

Русский

Два раза подряд удаление элементов по правой ассоциации возвращает исходное удаление.

LaTeX

$$drop_drop : ∀ {ds₁ ds₂ ds₃ : List Nat} (t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)),\n t.assocRight.drop.drop = t.drop$$

Lean4

theorem drop_drop : ∀ t : HolorIndex (ds₁ ++ ds₂ ++ ds₃), t.assocRight.drop.drop = t.drop
  | ⟨is, h⟩ => Subtype.eq (by simp [assocRight, drop, cast_type, List.drop_drop])

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