Theorems · Theorem · order theory
csSup_of_not_bddAbove
∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α}, ¬BddAbove s → sSup s = sSup ∅- Cited by
- 16 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses no axioms
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
- SupSet.sSupstatement · cited by 954
- BddAbovestatement and proof · cited by 620
- ConditionallyCompleteLinearOrderstatement and proof · cited by 542
- ConditionallyCompleteLinearOrder.csSup_of_not_bddAboveproof · cited by 2
Cited by16
Results whose statement or proof uses this declaration.
- Measurable.iSupproof · cited by 14
- Ordinal.log_of_left_le_oneproof · cited by 13
- ciSup_of_not_bddAboveproof · cited by 9
- Ordinal.div_zeroproof · cited by 7
- NNReal.coe_sSupproof · cited by 5
- SimpleGraph.exists_isNClique_cliqueNumproof · cited by 5
- csSup_mem_of_not_isSuccPrelimitproof · cited by 3
- Ordinal.IsPrincipal.sSupproof · cited by 2
- Cardinal.ciSup_mulproof · cited by 2
- Ordinal.sSup_le_sSup_add_oneproof · cited by 2
- Ordinal.sSup_ordproof · cited by 2
- Monotone.ciSup_comp_tendsto_atTop_of_linearOrderproof · cited by 2