Theorems · Definition · order theory

Set.uIcc

{α : Type u_1} → [Lattice α] → α → α → Set α

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 Set.Icc (a ⊓ b) (a ⊔ b). In a product type, uIcc corresponds to the bounding box of the two elements.

Defined in

Mathlib.Order.Interval.Set.UnorderedInterval

Cited by

393 results in Mathlib

Foundations

Depth 4 from the axioms, rests on 27 definitions · uses no axioms

Assumes

Lattice