sym — Mathlib

English

The sym2 of a set equals the image of the pairing function on its square.

Русский

Sym2 множества равен изображению пары на квадрате множества.

LaTeX

$$s^{(2)} = (s \times s).image Sym2.mk$$

Lean4

/-- Lifts a finset to `Sym α n`. `s.sym n` is the finset of all unordered tuples of cardinality `n`
with elements in `s`. -/
protected def sym (s : Finset α) : ∀ n, Finset (Sym α n)
  | 0 => {∅}
  | n + 1 => s.sup fun a ↦ Finset.image (Sym.cons a) (s.sym n)

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