Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-12 07:11 60d32337

View on Github →

feat(topology/instances/real): metric space structure on nat (#11963) Mostly copied from the already existing int version.

Estimated changes

added theorem nat.preimage_Icc
added theorem nat.preimage_Ici
added theorem nat.preimage_Ico
added theorem nat.preimage_Iic
added theorem nat.preimage_Iio
added theorem nat.preimage_Ioc
added theorem nat.preimage_Ioi
added theorem nat.preimage_Ioo
added theorem nat.closed_ball_eq_Icc
added theorem nat.dist_cast_rat
added theorem nat.dist_cast_real
added theorem nat.dist_coe_int
added theorem nat.dist_eq
added theorem nat.preimage_ball