singleton Set to element

Stream: new members

[Simon Daniel]

HI, im searching for function that maps a singleton set to its only element (apparently refered to by iota in math).
Ive used LeanSearch and looked at the Mathlib docs but couldnt find it. something like

def singleton_to_elem (fs: Finset α) (is_singleton: fs.card = 1): fs := sorry

[Eric Wieser]

import Mathlib


def Multiset.singleElem (fs: Multiset α) : fs.card = 1 → {x // x ∈ fs} :=
  fs.recOn (fun h => by simp at h)
    (fun a m ih ha => ⟨a, by simp⟩)
    (fun a b m ih => Function.hfunext (by simp) (by simp))

def Finset.singleElem (fs: Finset α) : fs.card = 1 → fs :=
  fs.val.singleElem

[Eric Wieser]

docs#Sym2.equivSym is the version for when there are two elements

[Simon Daniel]

nice, that works. Im not quite sure what Sym2.equivSym does, retrieving more than 1 element in a tuple/list should be however imposible from a set, without relying on choice right?

[Eric Wieser]

It retrieves them in a way that obscures the order they were chosen in

[Eric Wieser]

In fact, the Multiset version of your question is docs#Sym.oneEquiv