strictMono_sym2

Mathlib.Data.Finset.Sym

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

English

The map S ↦ S.sym2 is strictly monotone with respect to inclusion: if S ⊆ T and S ≠ T, then S.sym2 ⊊ T.sym2.

Русский

Отображение S ↦ S.sym2 точно монотонно: если S ⊆ T и S ≠ T, то S.sym2 ⊊ T.sym2.

LaTeX

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

Lean4

theorem strictMono_sym2 : StrictMono (Finset.sym2 : Finset α → _) :=
  monotone_sym2.strictMono_of_injective injective_sym2

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

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

Разделы

Аффилиация

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