lnay / metric-spaces-and-topology-game

MIT License
2 stars 1 forks source link

Create new proof: Topology world lvl 1 #8

Open lnay opened 5 months ago

lnay commented 5 months ago
Create a new lean file with the name specified below in Game/Levels/content_drafts which correctly compiles and defines and proves the theorem below. Break into intermediate theorems/lemmas if necessary (to go into separate levels, or provided as 'given' helpers, tbd later).
file name topology_wrld_L03.lean
proof unions of open sets are open in a metric space
extra info

Syllabus outline: #5