well-defined function

Stream: maths

[Calle Sönne]

In "informal" maths when you want to define a function you often make a bunch of choices and then show that this is well-defined and then move on with your life. How do you do this in lean? I have defined a function using classical.some and it turns out that this choice is unique. Where (and how) do you show that this is "well defined". I just dont want to have to prove my choice makes sense everytime I prove something about this function. Essentially what I am looking for is some lemma like function_is_well_def that I can prove about my function which makes dealing with it a lot easier.

[Eric Wieser]

If the properties you want the function to have are part of the existential, then docs#classical.some_spec gives you those properties

[Kevin Buzzard]

If you have defined a function then you've made a definition and immediately afterwards you should make an API for your definition. You might want to take a look at the example I showed Jason on the Discord when he was defining projections from direct sums using classical.some . The idea is that immediately after the definition you prove theorems about your function saying all the convenient things you want to say about it, eg if some_spec is P \and Q and R then you almost certainly want three theorems saying that P and Q and R are all true for your function, and then you prove these with some_spec and then you never have to touch some_spec again