Theorems · Definition · order theory
Set.Ici
{α : Type u_1} → [Preorder α] → α → Set αIci a is the left-closed right-infinite interval $[a, ∞)$.
- Defined in
- Mathlib.Order.Interval.Set.Defs
- Cited by
- 1,070 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 7 definitions · uses no axioms
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Preorderstatement and proof · cited by 7,952
- Set.ofPredproof · cited by 6,101
Cited by1,106
Results whose statement or proof uses this declaration.
- Filter.atTopproof · cited by 2,405
- Filter.atTop_basisstatement · cited by 42
- isClosed_Icistatement · cited by 40
- UpperSet.Iciproof · cited by 38
- Set.mem_Icistatement · cited by 37
- Filter.Ici_mem_atTopstatement · cited by 37
- Set.Ioi_subset_Ici_selfstatement · cited by 34
- Set.self_mem_Icistatement · cited by 30
- convex_Icistatement · cited by 29
- Finset.coe_Icistatement · cited by 27
- measurableSet_Icistatement · cited by 26
- Filter.mem_atTop_setsproof · cited by 21
Showing the 200 most cited of 1,106.