LowerTick

The greatest tick at or below x, in a type whose order has ticks.

LowerTick(x)The greatest tick at or below 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 Floor answers for such a type.
• Right adjoint of the ticks' inclusion: a tick $z$ is at or below $x$ exactly when it is at or below $\mathrm{LowerTick}(x)$.
• FloorOrder is our extension below Mathlib's FloorRing, for ticks that aren't a ring's integers.

Examples

Basic #

The greatest integer tick at or below 2.5

live ↗

In$\mathrm{LowerTick}(2.5)$Out$2$

About

Examples	1

See also: UpperTick, Floor, Midpoint