Theorems · Inductive type · order theory
CountableSupClosed
{α : Type u_2} → [LE α] → Set α → PropA set s is closed under countable supremum if for every nonempty countable subset of s, any
least upper bound of that subset is in s.
- Defined in
- Mathlib.Order.CountableSupClosed
- Cited by
- 27 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- LE
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
Cited by30
Results whose statement or proof uses this declaration.
- countableSupClosureproof · cited by 21
- CountableSupClosed.isLUB_memstatement and proof · cited by 10
- countableSupClosed_countableSupClosurestatement · cited by 5
- CountableSupClosed.iSup_memstatement and proof · cited by 3
- CountableSupClosed.supClosedstatement and proof · cited by 3
- countableSupClosure_minstatement and proof · cited by 3
- countableInfClosed_preimage_ofDualstatement and proof · cited by 1
- CountableSupClosed.finsetSup'_memstatement and proof · cited by 1
- CountableSupClosed.of_iSup_memstatement · cited by 1
- CountableSupClosed.prodstatement and proof · cited by 1
- CountableSupClosed.sInterstatement and proof · cited by 1
- countableSupClosed_preimage_ofDualstatement and proof · cited by 1