Theorems · Inductive type · order theory

LocallyFiniteOrder

(α : Type u_1) → [Preorder α] → Type u_1

This is a mixin class describing a locally finite order, that is, is an order where bounded intervals are finite. When you don't care too much about definitional equality, you can use LocallyFiniteOrder.ofIcc or LocallyFiniteOrder.ofFiniteIcc to build a locally finite order from just Finset.Icc.

Defined in

Mathlib.Order.Interval.Finset.Defs

Cited by

658 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

Preorder