slice — Mathlib

English

A slice extracts a subholor consisting of all entries with a fixed initial index i.

Русский

Срез извлекает подпроход Holor, состоящий из всех элементов с фиксированным начальным индексом i.

LaTeX

$$$\text{slice} : Holor\, \alpha\,(d \colon ds) \to (i : \mathbb{N}) \to i < d \to Holor\, \alpha\, ds$$$

Lean4

/-- A slice is a subholor consisting of all entries with initial index i. -/
def slice (x : Holor α (d :: ds)) (i : ℕ) (h : i < d) : Holor α ds := fun is : HolorIndex ds =>
  x ⟨i :: is.1, Forall₂.cons h is.2⟩

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