UpperTick

The least tick at or above x, in a type whose order has ticks.

UpperTick(x)The least tick at or above x, in a type whose order has ticks.

Typed signatures

Type	Package	Applies
(any) -> unknown	structures	always

Domain: Structures

Details

• The FloorOrder protocol's member, and what Ceil answers for such a type.
• Left adjoint of the ticks' inclusion: $x$ is at or below a tick $z$ exactly when $\mathrm{UpperTick}(x)$ is.
• FloorOrder is our extension below Mathlib's FloorRing, for ticks that aren't a ring's integers.

Examples

Basic #

The least integer tick at or above 2.5

live ↗

In$\mathrm{UpperTick}(2.5)$Out$3$

About

Examples	1

See also: LowerTick, Ceil, Midpoint