def Sym2.liftLe {α : Type u_1} {β : Type u_2} [ha : LinearOrder α] (p : Sym2 α) (f : α → α → β) : β

Equations

• p.liftLe f = Sym2.lift ⟨fun (a b : α) => f (min a b) (max a b), ⋯⟩ p

def Sym2.univ {α : Type u_1} [ha₁ : DecidableEq α] [ha₂ : Fintype α] : Finset (Sym2 α)

Equations

• Sym2.univ = Finset.image (fun (x : α × α) => match x with | (a, b) => s(a, b)) Finset.univ

@[simp]

theorem Sym2.mem_univ {α : Type u_1} [ha₁ : DecidableEq α] [ha₂ : Fintype α] {p : Sym2 α} : p ∈ univ

@[instance_reducible]

instance Sym2.instFintypeOfDecidableEq_projects {α : Type u_1} [ha₁ : DecidableEq α] [ha₂ : Fintype α] : Fintype (Sym2 α)

Equations

• Sym2.instFintypeOfDecidableEq_projects = { elems := Sym2.univ, complete := ⋯ }