Theorems · Definition · order theory

Finset.uIcc

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

Finset.uIcc a b is the set of elements lying between a and b, with a and b included. Note that we define it more generally in a lattice as Finset.Icc (a ⊓ b) (a ⊔ b). In a product type, Finset.uIcc corresponds to the bounding box of the two elements.

Defined in

Mathlib.Order.Interval.Finset.Defs

Cited by

84 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

LatticeLocallyFiniteOrder