cons_swap

Mathlib.Data.Sym.Basic

URI: https://scilib.ai/kg/mathlib#Sym.cons_swap

English

Inserting a then b equals inserting b then a: a ::ₛ b ::ₛ s = b ::ₛ a ::ₛ s.

Русский

Вставка a затем b равна вставке b затем a: a ::ₛ b ::ₛ s = b ::ₛ a ::ₛ s.

LaTeX

$$$ a ::_s (b ::_s s) = b ::_s (a ::_s s) $$$

Lean4

theorem cons_swap (a b : α) (s : Sym α n) : a ::ₛ b ::ₛ s = b ::ₛ a ::ₛ s :=
  Subtype.ext <| Multiset.cons_swap a b s.1

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

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

Разделы

Аффилиация

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