sym2_eq_empty

Mathlib.Data.Finset.Sym

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

English

For any s, s.sym2 = ∅ if and only if s = ∅.

Русский

Для любого s: s.sym2 = ∅ тогда и только если s = ∅.

LaTeX

$$$s.sym2 = \emptyset \iff s = \emptyset$$$

Lean4

@[simp]
theorem sym2_eq_empty : s.sym2 = ∅ ↔ s = ∅ := by rw [← val_eq_zero, sym2_val, Multiset.sym2_eq_zero_iff, val_eq_zero]

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

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

Разделы

Аффилиация

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