length_mem_splitLengths — Mathlib

English

If every element of sz is ≤ b, then every piece l₂ in sz.splitLengths l has length ≤ b.

Русский

Если для каждого n ∈ sz выполняется n ≤ b, то для каждого элемента l₂ в sz.splitLengths l выполняется l₂.length ≤ b.

LaTeX

$$$ \\forall l₂ \\in (sz.splitLengths l), \\ l₂.length ≤ b $$$

Lean4

theorem length_mem_splitLengths {α : Type*} (l : List α) (sz : List ℕ) (b : ℕ) (h : ∀ n ∈ sz, n ≤ b) :
    ∀ l₂ ∈ sz.splitLengths l, l₂.length ≤ b :=
  by
  rw [← List.forall_getElem]
  intro i hi
  have := length_splitLengths_getElem_le l sz (hi := hi)
  have := h (sz[i]'(by simpa using hi)) (getElem_mem ..)
  cutsat

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