Theorems · Definition · order theory

Finset.Iic

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

The finset $(-∞, b]$ of elements x such that x ≤ b. Basically Set.Iic b as a finset.

Defined in

Mathlib.Order.Interval.Finset.Defs

Cited by

280 results in Mathlib

Foundations

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

Assumes

PreorderLocallyFiniteOrderBot