Commit 2023-03-04 17:31 94a6006b

View on Github →

feat: port Topology.Instances.Nat (#2616)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Instances/Nat.lean

added theorem Nat.closedBall_eq_Icc

added theorem Nat.closedEmbedding_coe_real

added theorem Nat.dist_cast_real

added theorem Nat.dist_coe_int

added theorem Nat.dist_eq

added theorem Nat.pairwise_one_le_dist

added theorem Nat.preimage_ball

added theorem Nat.preimage_closedBall

added theorem Nat.uniformEmbedding_coe_real