Commit 2023-03-04 08:08 34972770

View on Github →

feat: port Topology.Instances.Int (#2612)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Instances/Int.lean

added theorem Int.ball_eq_Ioo

added theorem Int.closedBall_eq_Icc

added theorem Int.closedEmbedding_coe_real

added theorem Int.cocompact_eq

added theorem Int.cofinite_eq

added theorem Int.dist_cast_real

added theorem Int.dist_eq'

added theorem Int.dist_eq

added theorem Int.pairwise_one_le_dist

added theorem Int.preimage_ball

added theorem Int.preimage_closedBall

added theorem Int.uniformEmbedding_coe_real