Bourbaki's tau

Stream: maths

[Hamza Maimoune]

Hello, I am now reading Bourbaki and I'm wondering how would the tau be represented in Lean? Thank you!

[Reid Barton]

probably classical.some or classical.epsilon, though this question may be too low-level to be meaningful

[Patrick Massot]

I think reading that part of Bourbaki is a bad idea. My understanding is that Bourbaki messed up foundations. They had no expert in this topic and, contrary to what they sort of claim, they didn't really care about foundations.

[Patrick Massot]

Maybe I should expand a bit on Reid's answer too: he says those $\tau$ or $\varepsilon$ things are too close to the logical foundations that it makes sense to compare them across very different foundational systems.

[Reid Barton]

At least, don't take it too seriously. Lean is not based on set theory anyways.

[Hamza Maimoune]

Yes, I was warned I'm just trying to traduce it into Lean as an exercise.

[Reid Barton]

I think this will probably make you frustrated with both Bourbaki and Lean, but up to you.

[Reid Barton]

(I've also never read this part of Bourbaki, so I don't really know what I am talking about.)

[Hamza Maimoune]

I really think that I should stop. But do you know what Bourbaki volume are interesting to read? Because I would not want to learn non standard things!

[Reid Barton]

Patrick could give you a better answer, but approximately: the other ones.

[Kevin Buzzard]

Lie algebras and Lie groups

[Kevin Buzzard]

We have very little on them. I bet Lie algebras would be an interesting way to learn Lean

[Patrick Massot]

The stuff in general topology is slightly non-standard, but excellent. Basically it's non-standard only because people usually don't bother to provide proofs. It's 100% standard in proof assistants.

[Hamza Maimoune]

Thank you!