English
For any relation R, if l has Pairwise R, then the transformed list l.sublists' is Pairwise with Lex (swap R) relation.
Русский
Для любой relation R, если список l является Pairwise по R, то l.sublists' является Pairwise по Lex (swap R) с отношением к подспискам.
LaTeX
$$$\\forall {R}\\ {l}: List(\\alpha),\\ Pairwise R\\ l \\rightarrow\\ Pairwise (\\\\operatorname{Lex} (\\\\text{swap} R))\\ (l.sublists')$$$
Lean4
theorem sublists' {R} : ∀ {l : List α}, Pairwise R l → Pairwise (Lex (swap R)) (sublists' l)
| _, Pairwise.nil => pairwise_singleton _ _
| _, @Pairwise.cons _ _ a l H₁ H₂ =>
by
simp only [sublists'_cons, pairwise_append, pairwise_map, mem_sublists', mem_map, exists_imp, and_imp]
refine ⟨H₂.sublists', H₂.sublists'.imp fun l₁ => Lex.cons l₁, ?_⟩
rintro l₁ sl₁ x l₂ _ rfl
rcases l₁ with - | ⟨b, l₁⟩; · constructor
exact Lex.rel (H₁ _ <| sl₁.subset mem_cons_self)
