drop — Mathlib

English

Drop First Elements of HolorIndex: drop from HolorIndex (ds₁ ++ ds₂) to HolorIndex ds₂.

Русский

Удаление первых элементов HolorIndex: drop из HolorIndex (ds₁ ++ ds₂) в HolorIndex ds₂.

LaTeX

$$drop : ∀ {ds₁ : List ℕ}, HolorIndex (ds₁ ++ ds₂) → HolorIndex ds₂$$

Lean4

/-- Drop the first elements of a `HolorIndex`. -/
def drop : ∀ {ds₁ : List ℕ}, HolorIndex (ds₁ ++ ds₂) → HolorIndex ds₂
  | ds, is => ⟨List.drop (length ds) is.1, forall₂_drop_append is.1 ds ds₂ is.2⟩

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