rel_get_of_lt — Mathlib

English

Let e be a RelEmbedding ra rb. Then the map of any list preserves sortedness: (List.map e l).Sorted rb iff l.Sorted ra.

Русский

Пусть e — отображение вложения относительного порядка ra rb. Тогда отображение списка сохраняет упорядоченность: (List.map e l).Sorted rb эквивалично l.Sorted ra.

LaTeX

$$$$ (List.map\ e\ l).Sorted rb \iff l.Sorted ra. $$$$

Lean4

theorem rel_get_of_lt {l : List α} (h : l.Sorted r) {a b : Fin l.length} (hab : a < b) : r (l.get a) (l.get b) :=
  List.pairwise_iff_get.1 h _ _ hab

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