filter — Mathlib

English

If a list is sorted, then any subsequence obtained by filtering with a predicate preserves sorting.

Русский

Если список отсортирован, то подсписок, полученный фильтром по предикату, сохраняет сортировку.

LaTeX

$$$\\forall f:\\alpha\\to\\text{Bool},\\; l.\\text{Sorted } r\\Rightarrow \\text{Sorted } r(\\text{filter } f\_\\star l) $$$

Lean4

protected theorem filter {l : List α} (f : α → Bool) (h : Sorted r l) : Sorted r (filter f l) :=
  h.sublist filter_sublist

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