drop_take — Mathlib

English

Drop then take with associators preserves the relation: dropping then taking equals a single take after a drop.

Русский

Сохранение отношения при сочетании drop и take с ассоциаторами.

LaTeX

$$drop_take : ∀ {ds₁ ds₂ ds₃}, t.assocRight.drop.take = t.take.drop$$

Lean4

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

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