sym2 — Mathlib

English

The symmetric square is equivalent to multisets of cardinality two.

Русский

Симметрическая пара эквивалентна мультисетам размером два.

LaTeX

$$$\\mathrm{Sym}^2(\\alpha) \\simeq { s : \\mathrm{Multiset}(\\alpha) \\;\\middle|\\; \\mathrm{Multiset.card}\\, s = 2 }$$$

Lean4

/-- For a set `s : Set α`, `s.sym2` is the set of all unordered pairs of elements from `s`.
-/
def sym2 (s : Set α) : Set (Sym2 α) :=
  fromRel (r := fun x y ↦ x ∈ s ∧ y ∈ s) (fun _ _ => .symm)

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