Mathlib v3 is deprecated. Go to Mathlib v4

Theorem NEW.real.sub_one_lt_floor

Modification history

2018-01-19 16:18
data/real.lean
feat(data/real,*): supporting material for metric spaces
Deleted NEW.real.sub_one_lt_floorView on Github →
2018-01-16 05:29
data/real.lean
feat(data/real): completeness of the (new) real numbers
Added NEW.real.sub_one_lt_floorView on Github →