DISCUSSION: Game syllabus

[lnay]

Provisional outline for the lean levels and worlds to target

Metric Space world

proof	unlock
Tri inequality related equivalence	Distance function axioms (incl Tri ineq)
Sequence converges => any tail converges (or some other simple exercise with raw definition of convergence)	Convergence of sequence definition
Uniqueness of a sequence limit
Open ball is open (with raw definitions)	Open set definition	Prove some examples is continuous?	Continuous function definition
Something about closures/interiors/boundaries?
Cauchy sequences
Completeness
Boundedness
Bolzano-Weierstrass Theorem

Topology World

Proof	unlock
Union of open sets are open (in metric space)	Corresponding topology axiom	Finite intersection of open is open (metric space)	Corresponding topology axiom	If a sequence converges to a point in an open set, then some tail is entirely in that open set	Convergence definition
Preimage of open is open (metric spaces)	Continuous definition (topology)	Prove continuity of some function between non-metrisable
Metric space is Hausdorff (raw definition)	Hausdorff definition
Sequence can have at most one limit in Hausdorff space
Prove counterexample is not Hausdorff (opens={cofinite} works I think)
Something about closures/interiors/boundaries?
bijection from compact to haussdorff has a continuous inverse

Other potential things to pursue:

• induced topologies (maybe each in their own optional world?):
  • subspace
  • quotient
  • product
• transition to filter framework for topology
• other metric space stuff?

[lnay]

I can't find a definition for sequence limit in metric spaces. It's possible that it's just not necessary for developing theory. But is probably still useful for the pedagogical side of the game. Defining the limit of a sequence is not very long though:

def sequenceLimit (sequence: ℕ → X) (limit: X) :=
  ∀ε:ℝ, ε > 0 → (∃N:ℕ, ∀n:ℕ, n>N → (dist (sequence n) limit) < ε)