mem_sublistsLen — Mathlib

English

An element l' belongs to sublistsLen n l exactly when l' is a sublist of l and has length n.

Русский

Элемент l' принадлежит sublistsLen n l тогда и только тогда, когда l' является подсписком l и имеет длину n.

LaTeX

$$$\\forall {n}{l}{l'}:\\ l' \\in \\operatorname{sublistsLen}(n, l) \\leftrightarrow (l' \\lt+ l) \\land \\operatorname{length}(l') = n$$$

Lean4

@[simp]
theorem mem_sublistsLen {n} {l l' : List α} : l' ∈ sublistsLen n l ↔ l' <+ l ∧ length l' = n :=
  ⟨fun h => ⟨mem_sublists'.1 ((sublistsLen_sublist_sublists' _ _).subset h), length_of_sublistsLen h⟩, fun ⟨h₁, h₂⟩ =>
    h₂ ▸ mem_sublistsLen_self h₁⟩

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