sorted_gt_listMap

Mathlib.Data.List.Sort

URI: https://scilib.ai/kg/mathlib#OrderIso.sorted_gt_listMap

English

For an OrderIso e: α ≃o β and any list l, (l.map e).Sorted (GT.gt) ↔ l.Sorted (GT.gt).

Русский

Для OrderIso e: α ≃o β и любого списка l, (l.map e).Sorted (GT) эквивалентно l.Sorted (GT).

LaTeX

$$$$ (l.map e).Sorted (\GT.gt) \iff l.Sorted (\GT.gt). $$$$

Lean4

@[simp]
theorem sorted_gt_listMap (e : α ≃o β) {l : List α} : (l.map e).Sorted (· > ·) ↔ l.Sorted (· > ·) :=
  e.toOrderEmbedding.sorted_gt_listMap

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

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

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru