Re: [isabelle] I can't understand types in set-membership expressions
> I always wanted to learn mathematics in the way, that I
> understand every tiny bit.
The set theory you might be familiar with is the Zermelo - Fraenkel set theory. This is different than the typed set theory implemented in Isabelle/HOL.
A Tjark Weber mentions in a separate post, Isabelle implements the ZF set theory as well. For what you want to do I believe Isabelle's ZF logic is a better place to look at. There is some documentation on the logic in
For Isabelle/ZF based formalizations farther away from the foundations you can look at http://formalmath.tiddlyspot.com/ . (dislaimer: I am the author of that site).
And if you really want "every tiny bit", check out the Metamath project at http://us.metamath.org/mpegif/mmset.html
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)
This archive was generated by a fusion of
Pipermail (Mailman edition) and