Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-23 16:42 963bcad8

View on Github →

rat is order-dense in real; cleanup continuity proof for inv

Estimated changes

Modified topology/real.lean

deleted theorem closure_of_rat_image_eq

added theorem closure_of_rat_image_le_eq

added theorem closure_of_rat_image_le_le_eq

added theorem exists_pos_of_rat

added theorem ge_mem_nhds

added theorem le_mem_nhds

added theorem mem_zero_nhd_le

modified theorem tendsto_mul_bnd_rat