mem_insertionSort

Mathlib.Data.List.Sort

URI: https://scilib.ai/kg/mathlib#List.mem_insertionSort

English

An element is in the insertionSort of a list if and only if it is in the original list.

Русский

Элемент принадлежит списку insertionSort, если и только если он принадлежит исходному списку.

LaTeX

$$$$ x \in \mathrm{insertionSort}(r,l) \iff x \in l. $$$$

Lean4

@[simp]
theorem mem_insertionSort {l : List α} {x : α} : x ∈ l.insertionSort r ↔ x ∈ l :=
  (perm_insertionSort r l).mem_iff

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

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

Разделы

Аффилиация

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