Theorems · Inductive type · order theory
UpperSet
(α : Type u_1) → [LE α] → Type u_1
An upper set in an order α is a set such that any element greater than one of its members is
also a member. Also called up-set, upward-closed set.
- Defined in
- Mathlib.Order.Defs.Unbundled
- Cited by
- 245 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- LE
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by280
Results whose statement or proof uses this declaration.
- upperClosurestatement · cited by 84
- UpperSet.Icistatement · cited by 38
- UpperSet.extstatement and proof · cited by 29
- LowerSet.complstatement · cited by 17
- UpperSet.complstatement and proof · cited by 17
- UpperSet.Ioistatement · cited by 15
- UpperSet.mapstatement and proof · cited by 12
- UpperSet.upperstatement and proof · cited by 11
- subset_upperClosurestatement · cited by 11
- UpperSet.erasestatement and proof · cited by 9
- UpperSet.sdiffstatement and proof · cited by 8
- upperClosure_singletonstatement · cited by 8
Showing the 200 most cited of 280.