pairwise_sublists — Mathlib

English

If l has Pairwise R, then the list of all sublists, after mapping (Lex R) on reverse, is pairwise.

Русский

Если список l имеет пару (Pairwise) по R, то список подсписков после преобразования Lex R по обратному списку образует пары.

LaTeX

$$$\\forall {R} {l}: List(\\alpha),\\ Pairwise R\\ l \\rightarrow\\ Pairwise (Function.onFun (List.Lex R) List.reverse) (l.sublists)$$$

Lean4

theorem pairwise_sublists {R} {l : List α} (H : Pairwise R l) : Pairwise (Lex R on reverse) (sublists l) :=
  by
  have := (pairwise_reverse.2 H).sublists'
  rwa [sublists'_reverse, pairwise_map] at this

Похожие утверждения