Mathlib v3 is deprecated. Go to Mathlib v4

Theorem NEW.real.exists_rat_lt

Modification history

2018-01-19 16:18
data/real.lean
feat(data/real,*): supporting material for metric spaces
Deleted NEW.real.exists_rat_ltView on Github →
2018-01-16 16:08
data/real.lean
feat(data/real): variants on archimedean property
Added NEW.real.exists_rat_ltView on Github →