mk_mem_sym2_iff

Mathlib.Data.Finset.Sym

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

English

For a Sym2 element m, m ∈ s.sym2 if and only if every element of m belongs to s.

Русский

Для элемента m типа Sym2: m ∈ s.sym2 тогда и только тогда, когда каждый элемент пары m принадлежит s.

LaTeX

$$m ∈ s.sym2 \iff \forall a \in m, a ∈ s$$

Lean4

theorem mk_mem_sym2_iff : s(a, b) ∈ s.sym2 ↔ a ∈ s ∧ b ∈ s := by
  rw [mem_mk, sym2_val, Multiset.mk_mem_sym2_iff, mem_mk, mem_mk]

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

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

Разделы

Аффилиация

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