take — Mathlib

English

Take First Elements of HolorIndex: the take function returns the prefix HolorIndex ds₁ from HolorIndex (ds₁ ++ ds₂).

Русский

Взятие первых элементов HolorIndex: функция take возвращает префикс HolorIndex ds₁ из HolorIndex (ds₁ ++ ds₂).

LaTeX

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

Lean4

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

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