English
A list l is a sublist of l' iff there exists an order-preserving embedding f: ℕ ↪o ℕ such that for all indices, l[i] = l'[f(i)].
Русский
Список l является подсписком l' тогда и только тогда, когда существует отображение-встраивание по порядку f: ℕ ↪o ℕ такое, что для каждого индекса l[i] = l'[f(i)].
LaTeX
$$$ l <+ l' \\iff \\exists f:\\, \\mathbb{N} \\hookrightarrow_o \\mathbb{N},\\forall i, l[i] = l'[f(i)]. $$$
Lean4
/-- A `l : List α` is `Sublist l l'` for `l' : List α` iff
there is `f`, an order-preserving embedding of `ℕ` into `ℕ` such that
any element of `l` found at index `ix` can be found at index `f ix` in `l'`.
-/
theorem sublist_iff_exists_orderEmbedding_getElem?_eq {l l' : List α} :
l <+ l' ↔ ∃ f : ℕ ↪o ℕ, ∀ ix : ℕ, l[ix]? = l'[f ix]? :=
by
constructor
· intro H
induction H with
| slnil => simp
| cons _ _ IH =>
obtain ⟨f, hf⟩ := IH
refine ⟨f.trans (OrderEmbedding.ofStrictMono (· + 1) fun _ => by simp), ?_⟩
simpa using hf
| cons₂ _ _ IH =>
obtain ⟨f, hf⟩ := IH
refine ⟨OrderEmbedding.ofMapLEIff (fun ix : ℕ => if ix = 0 then 0 else (f ix.pred).succ) ?_, ?_⟩
· rintro ⟨_ | a⟩ ⟨_ | b⟩ <;> simp [Nat.succ_le_succ_iff]
· rintro ⟨_ | i⟩
· simp
· simpa using hf _
· rintro ⟨f, hf⟩
exact sublist_of_orderEmbedding_getElem?_eq f hf
