mem_toFinset — Mathlib

English

The members of the unordered pair are members of the corresponding finite set.

Русский

Члены неупорядоченной пары являются элементами соответствующего конечного множества.

LaTeX

$$$$ x \in z.toFinset \iff x \in z. $$$$

Lean4

/-- The members of an unordered pair are members of the corresponding finite set. -/
@[simp]
theorem mem_toFinset {x : α} {z : Sym2 α} : x ∈ z.toFinset ↔ x ∈ z := by
  rw [← Sym2.mem_toMultiset, Sym2.toFinset, Multiset.mem_toFinset]

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