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_L02.lean
proof
if a sequence converges, so does any tail
extra info
Use raw definition of convergence in formal statement (not mathlib definition). Alternatively prove a different elementary theorem about a converging sequenc.
Game/Levels/content_draftswhich 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).metric_wrld_L02.leanSyllabus outline: #5