Theorems · Definition · order theory
DirSupClosedOn
{α : Type u_1} → [Preorder α] → Set (Set α) → Set α → PropA predicate for a set which is closed under directed suprema of nonempty sets.
This is the complement of a DirSupInaccOn set.
- Defined in
- Mathlib.Order.DirSupClosed
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Preorderstatement and proof · cited by 7,952
- Set.Nonemptyproof · cited by 2,627
- IsLUBproof · cited by 280
- DirectedOnproof · cited by 271
Cited by26
Results whose statement or proof uses this declaration.
- dirSupClosedOn_complstatement · cited by 7
- DirSupClosed.dirSupClosedOnstatement · cited by 6
- DirSupClosedOn.sInterstatement and proof · cited by 4
- dirSupInaccOn_complstatement and proof · cited by 3
- DirSupInaccOn.complstatement · cited by 3
- dirSupClosedOn_univstatement · cited by 2
- IsUpperSet.dirSupClosedOnstatement · cited by 2
- DirSupClosedOn.interstatement and proof · cited by 2
- DirSupClosedOn.unionstatement and proof · cited by 2
- Topology.IsScottHausdorff.isClosed_iff_dirSupClosedOnstatement and proof · cited by 2
- DirSupInaccOn.sUnionproof · cited by 2
- DirSupClosedOn.of_complstatement · cited by 1