Zulip Chat Archive

Stream: new members

Topic: Extracting a single element from a set

view this post on Zulip ROCKY KAMEN-RUBIO (Jun 17 2020 at 17:44):

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.

view this post on Zulip Bryan Gin-ge Chen (Jun 17 2020 at 17:51):

// 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.

Last updated: May 13 2021 at 21:12 UTC