Still trying to grasp how far I should take formalizations

Stream: maths

[Alexandre Soares]

Hi people, mathematician here trying to make sense of Lean by trying to formalise simple stuff. I'm currently trying to do the equivalence between the various formulations of the Axiom of Choice. Some of them I succeeded but I'm stuck in one of them which requires me to translate into Lean the following bit of mathematics:

If $S$ is a non-empty subset of $A \times Y$ such that for any $x \in A$ there exists exactly one $y \in Y$ such that $(x, y) \in S$, then there is a function $f : A \to Y$ such that for all $x \in A$, $(x, f(x)) \in S$.

In fact, set-theoretically speaking the function $f$ is the set $S$ itself. In the course of my proof in Lean, I managed to get to a context containing the following

X : Type
Y : Type
A : Set X
S :  Set (A × Y)
ha : Nonempty A
h1 : ∀ x ∈ A, ∃ p ∈ S, p.1 = x
h2 : ∀ p₁ ∈ S, ∀ p₂ ∈ S, p₁ ≠ p₂ → p₁.1 ≠ p₂.1

From this I haven't been able to deduce the existence of a Lean function f : X → Y satisfying the condition
∀ x ∈ A, (x, f x) ∈ S; but I'm not really sure I need to, because mathematically S as above is already the desired function. Is it possible to obtain an actual Lean function f as stated without an unreasonable amount of extra work?

[Edward van de Meent]

fun x => (h1 x).choose.2 should be such a function. proving that it is will likely be helped by (h1 x).choose_spec

[Edward van de Meent]

(note the use of the axiom of choice in order to move from h1 x : ∃ p ∈ S, p.1 = x to p : A × Y)

[Patrick Massot]

Welcome! Be careful that your choice of topic is maybe not the greatest idea. Things that are very close to the foundations are bound to expose foundational differences between Lean and what you are used to. This may be very distracting in your learning.

[Edward van de Meent]

perhaps it would be useful to work with the ZFSets in mathlib? (i don't know how user-friendly those are compared to the usual Set though...)

[Edward van de Meent]

also note that i merely know of their existence, i have no experience working with them.

[Ruben Van de Velde]

For a beginner, I would indeed avoid ZFSet

[Kevin Buzzard]

For a beginner, I would avoid set theory completely as Patrick said, because Lean's foundations are completely different. Even the meaning of "axiom of choice" is rather different in lean to set theory.

[Alexandre Soares]

Thank you all for your answers!

@Patrick Massot I started in Lean by playing with some Analysis stuff and found it very satisfying. I should probably go back to that for now until I am more familiar with the idiosyncrasies of the foundations.

Edward van de Meent said:

fun x => (h1 x).choose.2 should be such a function. proving that it is will likely be helped by (h1 x).choose_spec

My bad, I forgot to say that I wanted some construction that does not use Classical.choose. At some point I tricked myself into thinking I found a formalisation, as Lean wasn't complaining and the goal was cleared. But then I realized that I was using choose in the middle of it and it makes the whole argument invalid, since I am trying to prove the Axiom of Choice itself.

[Mario Carneiro]

you should probably give a complete #mwe statement then, to show what version of the axiom of choice you are assuming and proving

[Mario Carneiro]

if you are not assuming the axiom of choice, and you don't want to use Classical.choose, then it obviously can't be done: without some form of the axiom of choice or an equivalent you can't prove the axiom of choice. That's why it's an axiom in the first place

[Alexandre Soares]

@Mario Carneiro what I posted above is practically a #mwe, the only thing it needs is import Mathlib at the top and wrapping the judgements and desired conclusion in an example.

The conclusion I originally described can obviously be done in Set Theory without the Axiom of Choice -- it's a trivial matter of checking that the set $S$ satisfies the definition of a function.

[Mario Carneiro]

@Alexandre Soares That's not what a #mwe is, please read the link. You can use extract_goal to produce a complete example that can be copied, but it is very important when asking these kind of questions to give all the context in copy-pastable form

[Mario Carneiro]

What you posted above doesn't even say what the original hypotheses are, only some hypotheses in the middle, and it lacks a goal statement except in a rephrased form. As others have pointed out, for a question like this which is close to the foundations it is important to have the exact goal you are giving to lean because the details matter