Extracting a single element from a set

Stream: new members

[ROCKY KAMEN-RUBIO]

I want to extract an arbitrary element of a set that is unequal to a given element.

variable P : Type
def elt_of_set_ne_given (points : set P) (p1 : P) : {p : P // p ∈ points ∧ p ≠ p1} := sorry

1. Where can I find the documentation for //? I'm having trouble finding it
2. Is there an easy way to tell Lean that my set has at least two elements? I know finset can do this, but my set might be infinite. I know I could just state that there are two unequal elements in the set, but I'd like to be able to generalize this to larger cases, and that approach gets inconvenient. I know set.card is a thing but looking through the documentation I'm not seeing an easy way to do this.

[Bryan Gin-ge Chen]

// is notation for subtypes. There's also a very brief discussion in TPiL.

In general, if you suspect some symbols may be notation, you can tell the pretty-printer to turn off printing notation by using set_option pp.notation false. Then you can #print the declaration and see what the full name is.