feat: prove T218, discrete implies locally finite

[kisonecat]

Adds T218: a discrete space is locally finite, which fixes #473

In a discrete space {x} is open, hence a neighbourhood of x, and it is finite:

⟨fun x ↦ ⟨{x}, by simp, finite_singleton x⟩⟩

Closes #473.