Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-19 19:04 ee398b66

View on Github →

feat(algebra/floor): prove ⌈x⌉ ≤ ⌊x⌋ + 1 (#1568)

Estimated changes

added theorem ceil_le_floor_add_one