Theorems · Definition · order theory
IsCompactElement
{α : Type u_1} → [PartialOrder α] → α → PropAn element k is compact if any directed set with LUB (least upper bound) above
k has already got above k at some point in the set.
Such an element is also called "finite" or "S-compact".
- Defined in
- Mathlib.Order.CompactlyGenerated.Basic
- Cited by
- 34 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
- Assumes
- PartialOrder
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.
- Setproof · cited by 53,352
- PartialOrderstatement and proof · cited by 6,410
- Set.Nonemptyproof · cited by 2,627
- IsLUBproof · cited by 280
- DirectedOnproof · cited by 271
Cited by38
Results whose statement or proof uses this declaration.
- CompleteLattice.isCompactElement_iff_le_of_directed_sSup_lestatement and proof · cited by 6
- isNoetherian_iff'proof · cited by 6
- CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSupstatement · cited by 4
- Submodule.singleton_span_isCompactElementstatement · cited by 4
- inf_sSup_eq_iSup_inf_sup_finsetproof · cited by 4
- CompleteLattice.wellFoundedGT_characterisationsstatement and proof · cited by 4
- IsCompactlyGenerated.BooleanGenerators.atomisticproof · cited by 4
- CompleteLattice.isCompactElement_finsetSupstatement and proof · cited by 3
- CompleteLattice.isSupFiniteCompact_iff_all_elements_compactstatement · cited by 3
- CompleteLattice.wellFoundedGT_iff_isSupFiniteCompactproof · cited by 3
- DirectedOn.inf_sSup_eqproof · cited by 3
- IsCompactlyGenerated.exists_sSup_eqstatement · cited by 2