sublistsLen_of_length_lt — Mathlib

English

If the length of l is less than n, then there are no sublists of length n in l.

Русский

Если длина списка l меньше n, тогда подсписков длины n в l нет.

LaTeX

$$$(\\operatorname{length}(l) < n) \\Rightarrow \\operatorname{sublistsLen}(n, l) = []$$$

Lean4

theorem sublistsLen_of_length_lt {n} {l : List α} (h : l.length < n) : sublistsLen n l = [] :=
  eq_nil_iff_forall_not_mem.mpr fun _ =>
    mem_sublistsLen.not.mpr fun ⟨hs, hl⟩ => (h.trans_eq hl.symm).not_ge (Sublist.length_le hs)

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