Theory Pick

theory Pick imports Main
begin

definition "pick X ≡ SOME x. x ∈ X"

lemma pick[simp]: "x ∈ X ⟹ pick X ∈ X"
unfolding pick_def by (metis someI_ex)

lemma pick_NE[simp]: "X ≠ {} ⟹ pick X ∈ X" by auto


end