Theorems · Definition · combinatorics

Sym2.lift

{α : Type u_1} → {β : Type u_2} → { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ } ≃ (Sym2 α → β)

The universal property of Sym2; symmetric functions of two arguments are equivalent to functions from Sym2. Note that when β is Prop, it can sometimes be more convenient to use Sym2.fromRel instead.

Defined in

Mathlib.Data.Sym.Sym2

Cited by

6 results in Mathlib

Foundations

Depth 10 from the axioms · uses Quot.sound