sorted_listMap

Mathlib.Data.List.Sort

URI: https://scilib.ai/kg/mathlib#RelIso.sorted_listMap

English

For a RelIso e: ra ≃r rb and any list l, (l.map e).Sorted rb ↔ l.Sorted ra.

Русский

Для изоморфизма отношения e: ra ≃r rb и любого списка l, (l.map e).Sorted rb эквивалентно l.Sorted ra.

LaTeX

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

Lean4

@[simp]
theorem sorted_listMap (e : ra ≃r rb) {l : List α} : (l.map e).Sorted rb ↔ l.Sorted ra :=
  e.toRelEmbedding.sorted_listMap

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

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

Разделы

Аффилиация

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