take_take — Mathlib

English

Take is stable under repeated taking: taking twice equals taking once after a right associator.

Русский

Стабильность take при повторном взятии: take(t.assocRight) = take(t).take.

LaTeX

$$take_take : ∀ t : HolorIndex (ds₁ ++ ds₂ ++ ds₃), t.assocRight.take = t.take.take$$

Lean4

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

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