English
A list l is a sublist of l' iff there exists f: Fin(length l) ↪o Fin(length l') such that for all indices i, l.get i = l'.get (f(i)).
Русский
Список l является подсписком l' тогда и только тогда, когда существует встраивание f: Fin(|l|) ↪o Fin(|l'|) такое, что для каждого i выполняется l.get i = l'.get (f(i)).
LaTeX
$$$ l <+ l' \\iff \\exists f:\\, Fin(l.length) \\hookrightarrow_o Fin(l'.length),\\forall i: Fin(l.length), l.get i = l'.get (f(i)). $$$
Lean4
/-- A `l : List α` is `Sublist l l'` for `l' : List α` iff
there is `f`, an order-preserving embedding of `Fin l.length` into `Fin l'.length` such that
any element of `l` found at index `ix` can be found at index `f ix` in `l'`.
-/
theorem sublist_iff_exists_fin_orderEmbedding_get_eq {l l' : List α} :
l <+ l' ↔ ∃ f : Fin l.length ↪o Fin l'.length, ∀ ix : Fin l.length, l.get ix = l'.get (f ix) :=
by
rw [sublist_iff_exists_orderEmbedding_getElem?_eq]
constructor
· rintro ⟨f, hf⟩
have h : ∀ {i : ℕ}, i < l.length → f i < l'.length :=
by
intro i hi
specialize hf i
rw [getElem?_eq_getElem hi, eq_comm, getElem?_eq_some_iff] at hf
obtain ⟨h, -⟩ := hf
exact h
refine ⟨OrderEmbedding.ofMapLEIff (fun ix => ⟨f ix, h ix.is_lt⟩) ?_, ?_⟩
· simp
· intro i
apply Option.some_injective
simpa [getElem?_eq_getElem i.2, getElem?_eq_getElem (h i.2)] using hf i
· rintro ⟨f, hf⟩
refine ⟨OrderEmbedding.ofStrictMono (fun i => if hi : i < l.length then f ⟨i, hi⟩ else i + l'.length) ?_, ?_⟩
· intro i j h
dsimp only
split_ifs with hi hj hj
· rwa [Fin.val_fin_lt, f.lt_iff_lt]
· cutsat
· exact absurd (h.trans hj) hi
· simpa using h
· intro i
simp only [OrderEmbedding.coe_ofStrictMono]
split_ifs with hi
· specialize hf ⟨i, hi⟩
simp_all
· rw [getElem?_eq_none_iff.mpr, getElem?_eq_none_iff.mpr]
· simp
· simpa using hi
