Theorems · Inductive type · order theory
CountableInfClosed
{α : Type u_2} → [LE α] → Set α → PropA set s is closed under countable infimum if for every nonempty countable subset of s, any
greatest lower 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.
- countableInfClosureproof · cited by 21
- CountableInfClosed.isGLB_memstatement and proof · cited by 10
- countableInfClosed_countableInfClosurestatement · cited by 5
- countableInfClosure_eq_selfstatement · cited by 4
- countableInfClosure_minstatement and proof · cited by 3
- CountableInfClosed.iInf_memstatement and proof · cited by 3
- CountableInfClosed.infClosedstatement and proof · cited by 3
- countableInfClosed_preimage_ofDualstatement and proof · cited by 1
- countableSupClosed_preimage_ofDualstatement and proof · cited by 1
- mem_countableInfClosure_iff_iInfproof · cited by 1
- CountableInfClosed.emptystatement · cited by 1
- CountableInfClosed.finsetInf'_memstatement and proof · cited by 1