instCommutativeDisjSups

Mathlib.Data.Finset.Sups

URI: https://scilib.ai/kg/mathlib#Finset.instCommutativeDisjSups

English

The disjoint-sum operation on Finset α is commutative; i.e., s ○ t = t ○ s for all Finsets s,t.

Русский

Дизъюнктивная сумма над Finset α тождественно коммутативна: для всех s,t верно s ○ t = t ○ s.

LaTeX

$$$ s \\circ t = t \\circ s $$$

Lean4

instance : @Std.Commutative (Finset α) (· ○ ·) :=
  ⟨disjSups_comm⟩

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

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

Разделы

Аффилиация

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