mem_sym2_iff

Mathlib.Data.Finset.Sym

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

English

Same content as mem_sym2_iff but expressed via simp-friendly form.

Русский

Та же мысль, выраженная в упрощенной форме.

LaTeX

$$Eq (s.sym2 m) (∀ a ∈ m, a ∈ s)$$

Lean4

@[simp]
theorem mem_sym2_iff {m : Sym2 α} : m ∈ s.sym2 ↔ ∀ a ∈ m, a ∈ s :=
  by
  rw [mem_mk, sym2_val, Multiset.mem_sym2_iff]
  simp only [mem_val]

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

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

Разделы

Аффилиация

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