Creating definitions in Lean

Stream: new members

[Abhimanyu Pallavi Sudhir]

I am trying to define an equivalence class in Lean, where I already have a binary relation, defined as a variable variable (r : S → S → Prop) -- how would I insert the requirement of binary_relation satisfying equivalence while defining an equivalence class?

[Abhimanyu Pallavi Sudhir]

I.e. surely just def class (a : S) : set S := { x | r x a } is not enough. Do I need some squiggly brackets here to impose the requirement equivalence binary_relation?

[Kenny Lau]

the philosophy is that we create the definition as general as possible, and only insert the hypothesis in the proofs

[Abhimanyu Pallavi Sudhir]

Perhaps, but I just want to learn how definitions work. Can we make them specific in this way?

[Kenny Lau]

def equivalence_class (h : is_equivalence r) (a : S) : set S := { x | r x a }

[Abhimanyu Pallavi Sudhir]

Right, and then when using the definition we'd need to provide a proof of is_equivalence r as a parameter, right?

[Kenny Lau]

yes

[Bryan Gin-ge Chen]

Note that if you use that definition, the variable r becomes something lean can very easily infer. Thus it's convenient to make it implicit (by writing variable {r} immediately beforehand), so that when you use equivalence_class, you won't need to write equivalence_class r h a but only equivalence_class h a.

[Kevin Buzzard]

@Abhimanyu Pallavi Sudhir just to note that class is already a keyword in Lean so you might want to stick to Kenny's suggestion of equivalence_class in any experiments you try.