support_sym2Mul_subset

Mathlib.Data.Sym.Sym2.Finsupp

URI: https://scilib.ai/kg/mathlib#Finsupp.support_sym2Mul_subset

English

The sym2Mul-support is contained in the sym2-support of f.

Русский

Поддержка sym2Mul включена в поддержку sym2 от f.

LaTeX

$$$f.\mathrm{sym2Mul}.\mathrm{support} \subseteq f.\mathrm{support}.\mathrm{sym2}$$$

Lean4

theorem support_sym2Mul_subset : f.sym2Mul.support ⊆ f.support.sym2 :=
  support_onFinset_subset

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

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

Разделы

Аффилиация

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