mem_sublists — Mathlib

English

For any s, t, s is a member of sublists t if and only if s is a sublist of t.

Русский

Для любых s, t: s является элементом sublists t тогда и только тогда, когда s является подпоследовательностью t.

LaTeX

$$$\\forall {s,t:\\mathrm{List}(\\alpha)},\\; s \\in \\text{sublists}(t) \\iff s \\subseteq t$$$

Lean4

@[simp]
theorem mem_sublists {s t : List α} : s ∈ sublists t ↔ s <+ t := by
  rw [← reverse_sublist, ← mem_sublists', sublists'_reverse, mem_map_of_injective reverse_injective]

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