sym2 — Mathlib

English

Same as Range SublistsLen Perm, with small lemmas used for simplification.

Русский

То же самое, что и Range SublistsLen Perm, с использованием вспомогательных лемм для упрощения.

LaTeX

$$$$ \\text{(see Range SublistsLen Perm for the main statement)} $$$$

Lean4

/-- `xs.sym2` is a list of all unordered pairs of elements from `xs`.
If `xs` has no duplicates then neither does `xs.sym2`. -/
protected def sym2 : List α → List (Sym2 α)
  | [] => []
  | x :: xs => (x :: xs).map (fun y => s(x, y)) ++ xs.sym2

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