Theorems · Theorem · combinatorics

List.sublist_iff_exists_fin_orderEmbedding_get_eq

∀ {α : Type u_1} {l l' : List α}, l.Sublist l' ↔ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)

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'.

Defined in

Mathlib.Data.List.NodupEquivFin

Cited by

1 results in Mathlib

Foundations

Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound