mem_sublistsLen_self — Mathlib

English

If l' is a sublist of l, then l' appears as a member of sublistsLen (length l') l.

Русский

Если l' является подсписком l, то l' встречается как элемент в sublistsLen(|l'|) l.

LaTeX

$$$\\forall {l}{l'}:\\ l' \\sublist l \\Rightarrow l' \\in \\operatorname{sublistsLen}(\\operatorname{length}(l'), l)$$$

Lean4

theorem mem_sublistsLen_self {l l' : List α} (h : l' <+ l) : l' ∈ sublistsLen (length l') l := by
  induction h with
  | slnil => simp
  | @cons l₁ l₂ a s IH =>
    rcases l₁ with - | ⟨b, l₁⟩
    · simp
    · rw [length, sublistsLen_succ_cons]
      exact mem_append_left _ IH
  | cons₂ a s IH =>
    rw [length, sublistsLen_succ_cons]
    exact mem_append_right _ (mem_map.2 ⟨_, IH, rfl⟩)

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