Theorems · Definition · order theory

Finset.Ioo

{α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrder α] → α → α → Finset α

The finset $(a, b)$ of elements x such that a < x and x < b. Basically Set.Ioo a b as a finset.

Defined in

Mathlib.Order.Interval.Finset.Defs

Cited by

185 results in Mathlib

Foundations

Depth 3 from the axioms, rests on 5 definitions · uses no axioms

Assumes

PreorderLocallyFiniteOrder