How To Prove It with Lean

Stream: general

[Mykhailo Kilianovski]

Thank you for augmenting your book with this great Lean plotline! I am not sure if I would gone through exercises on paper, but with a modern tool, it is much more fun!

Exercise_3_6_6b was a challenging one. First, it differs a little bit from the one in the book and does not have Like_ prefix to indicate this (the book version is formulated in terms of powersets).

Also, as I suppose, the answer here is the Universal set of U. But it is hard to find documentation on the universal set in Lean 4. Are there any neat examples of how universal sets are manipulated? Because I suspect that my proof is a dirty one :upside_down:

[Notification Bot]

A message was moved here from #announce > How To Prove It with Lean by Scott Morrison.

[Dan Velleman]

Yes, the solution is to use the universal set of U. One way to define it would be { x : U | x = x }. (Another possibility, using an idea that is not introduced until later in How To Prove It With Lean, would be { x : U | True }.) You don't need any special facts about universal sets to solve the exercise--just use the definition of this set theory notation.

[Dan Velleman]

You're right that the problem statement is slightly different from the statement in the print version of How To Prove It. The type Set U in this problem plays the same role as the power set of U in the print version. But they both mean essentially the same thing: the collection of all sets whose elements come from U.