monotone_sym2

Mathlib.Data.Finset.Sym

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

English

Let S and T be finite subsets of α with S ⊆ T. Then S.sym2 ⊆ T.sym2.

Русский

Пусть S и T — конечные подмножества множества α и S ⊆ T. Тогда S.sym2 ⊆ T.sym2.

LaTeX

$$$S \subseteq T \Rightarrow S^{(2)} \subseteq T^{(2)}$$$

Lean4

theorem monotone_sym2 : Monotone (Finset.sym2 : Finset α → _) := fun _ _ => sym2_mono

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

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

Разделы

Аффилиация

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