Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-16 16:08 e11da6ec

View on Github →

feat(data/real): variants on archimedean property

Estimated changes

Modified data/real.lean

deleted theorem NEW.real.archimedean

added theorem NEW.real.exists_int_gt

added theorem NEW.real.exists_int_lt

added theorem NEW.real.exists_nat_gt

added theorem NEW.real.exists_rat_gt

added theorem NEW.real.exists_rat_lt