instIsSymmPerm

Mathlib.Data.List.Perm.Basic

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

English

The permutation relation on lists is symmetric: if l ~ l', then l' ~ l.

Русский

Отношение перестановок на списках симметрично: если l ~ l', то l' ~ l.

LaTeX

$$$\\forall l,l':\\ l \\sim l' \\Rightarrow l' \\sim l.$$$

Lean4

instance : IsSymm (List α) Perm :=
  ⟨fun _ _ ↦ .symm⟩

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

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

Разделы

Аффилиация

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