English
Let α be a type and r a relation on α with IsAntisymm. For any lists l1, l2 of α, if l1 is a subpermutation of l2 and both l1 and l2 are sorted by r, then l1 is a sublist of l2.
Русский
Пусть α — множество, r — отношение на α, удовлетворяющее свойству антисимметрии. Для любых списков l1, l2 из α, если l1 является подпermutой к l2 и оба списка упорядочены по r, то l1 является подподсписком l2.
LaTeX
$$$$ \forall l_1,l_2:\ \text{List }\alpha\,\Big[IsAntisymm\ \alpha\ r\Big],\ (l_1 <+~ l_2) \Rightarrow (l_1.Sorted r) \Rightarrow (l_2.Sorted r) \Rightarrow l_1 <+ l_2. $$$$
Lean4
theorem sublist_of_subperm_of_sorted [IsAntisymm α r] {l₁ l₂ : List α} (hp : l₁ <+~ l₂) (hs₁ : l₁.Sorted r)
(hs₂ : l₂.Sorted r) : l₁ <+ l₂ := by
let ⟨_, h, h'⟩ := hp
rwa [← eq_of_perm_of_sorted h (hs₂.sublist h') hs₁]
