sym_empty

Mathlib.Data.Finset.Sym

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

English

The sym power of the empty set is empty for all positive n.

Русский

Симметрическая степень пустого множества равна пустому множеству для всех положительных n.

LaTeX

$$\text{For all } n, (\varnothing : \mathrm{Finset} \alpha).\mathrm{sym} (n+1) = \varnothing$$

Lean4

theorem sym_empty (n : ℕ) : (∅ : Finset α).sym (n + 1) = ∅ :=
  rfl

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

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

Разделы

Аффилиация

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