mathlib3

aeda3fb7 - feat(topology/instances/real, topology/metric_space/basic, algebra/floor): integers are a proper space (#6437)

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