Contribute images and inverse images.

[kvanvels]

I would like to make a point-set topology lean game and I think that contributing images and inverse images to the set-theory game would be a good place to start. Is that something you might be interested in?

Thank you,

Kent Van Vels

[djvelleman]

Hi Ken, When I wrote the set theory game, my intention was to use set theory as a vehicle to introduce the rules for dealing with all of the concepts of logic in Lean: and, or, not, if-then, iff, for all, and there exists. Subset world shows how to work with if-then, complement world is for not (but it also introduces iff), intersection world for and, union world for or, and the family worlds are for the quantifiers for all and there exists. So I think that the game, as it stands, accomplishes a well-defined purpose, with every world making a contribution to that purpose. The ideas you are proposing sound like good ideas for a game, but I'm reluctant to add them to the set theory game, because I'm not sure they fit with my overall vision for the game. But perhaps they should be the first world in your point-set topology game? I assume you found the source code for the game here: https://github.com/djvelleman/STG4 <https://github.com/djvelleman/STG4> Feel free to take any ideas from the game that you find useful for creating your game. -Dan

…

On Jan 25, 2025, at 6:38 PM, kvanvels ***@***.***> wrote: I would like to make a point-set topology lean game and I think that contributing images and inverse images to the set-theory game would be a good place to start. Is that something you might be interested in? Thank you, Kent Van Vels — Reply to this email directly, view it on GitHub <#15>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/A2MRYYTRSLE46HNRMOO4YKT2MQOADAVCNFSM6AAAAABV3Z5BZ2VHI2DSMVQWIX3LMV43ASLTON2WKOZSHAYTCMRSGQ4TGNI>. You are receiving this because you are subscribed to this thread.

[kvanvels]

Hello Dan, That makes sense. And I appreciate the detailed and quick response. I think I will use your game as a prerequisite for the topology game. If you have any ideas that will make a good topology game, please let me know. Feel free to ignore this: I am thinking of starting with a prelude where I do topology in the context of a metric space and introduce concepts of closed-open sets/arbitrary unions/ finite intersections/maybe compactness/bases/etc. in that context, before doing things in a general topological space. Again thank you for your response. I appreciate it. Kent VanVels

…

On Sunday, January 26th, 2025 at 11:39 AM, Dan Velleman ***@***.***> wrote: Hi Ken, When I wrote the set theory game, my intention was to use set theory as a vehicle to introduce the rules for dealing with all of the concepts of logic in Lean: and, or, not, if-then, iff, for all, and there exists. Subset world shows how to work with if-then, complement world is for not (but it also introduces iff), intersection world for and, union world for or, and the family worlds are for the quantifiers for all and there exists. So I think that the game, as it stands, accomplishes a well-defined purpose, with every world making a contribution to that purpose. The ideas you are proposing sound like good ideas for a game, but I'm reluctant to add them to the set theory game, because I'm not sure they fit with my overall vision for the game. But perhaps they should be the first world in your point-set topology game? I assume you found the source code for the game here: https://github.com/djvelleman/STG4 <https://github.com/djvelleman/STG4> Feel free to take any ideas from the game that you find useful for creating your game. -Dan > On Jan 25, 2025, at 6:38 PM, kvanvels ***@***.***> wrote: > > > I would like to make a point-set topology lean game and I think that contributing images and inverse images to the set-theory game would be a good place to start. Is that something you might be interested in? > > Thank you, > > Kent Van Vels > > — > Reply to this email directly, view it on GitHub <#15>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/A2MRYYTRSLE46HNRMOO4YKT2MQOADAVCNFSM6AAAAABV3Z5BZ2VHI2DSMVQWIX3LMV43ASLTON2WKOZSHAYTCMRSGQ4TGNI>. > You are receiving this because you are subscribed to this thread. > — Reply to this email directly, [view it on GitHub](#15 (comment)), or [unsubscribe](https://github.com/notifications/unsubscribe-auth/AYG544R2WN5YTYABDKJ6GA32MUFUFAVCNFSM6AAAAABV3Z5BZ2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDMMJUGQ4TQMBZGU). You are receiving this because you authored the thread.Message ID: ***@***.***>

[djvelleman]

Hi Kent,

Good luck with your project. I'll be interested to see what you come up with.

-Dan