Commit 2021-02-26 10:06 aeda3fb7

feat(topology/instances/real, topology/metric_space/basic, algebra/floor): integers are a proper space (#6437) The metric space ℤ is a proper space. Also, under the coercion from ℤ to ℝ, inverse images of compact sets are finite. The key point for both facts is to express the inverse image of an ℝ-interval under the coercion as an appropriate ℤ-interval, using floor or ceiling of the endpoints -- I provide these facts as simp-lemmas. Indirectly related discussion: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Finiteness.20of.20balls.20in.20the.20integers