search

lnay / metric-spaces-and-topology-game

MIT License
2 stars 1 forks source link

Create new proof: metric world - lvl 3 #7

Closed lnay closed 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 metric_wrld_L03.lean
proof uniqueness of sequence limit in a metric space
extra info Use definition for limit provided in mathlib

Syllabus outline: #5

lnay commented 5 months ago

Completed in commit 011a772

There's a decent variety of lean and a non-trivial calc-block. Curious about how this will play out in the browser. This might have to be split into several levels.