Theorems · Theorem · order theory
not_bddAbove_iff
∀ {α : Type u_4} [inst : LinearOrder α] {s : Set α}, ¬BddAbove s ↔ ∀ (x : α), ∃ y ∈ s, x < yA set s is not bounded above if and only if for each x there exists y ∈ s that is greater
than x. A version for preorders is called not_bddAbove_iff'.
- Defined in
- Mathlib.Order.Bounds.Basic
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- LinearOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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
- LinearOrderstatement and proof · cited by 8,572
- BddAbovestatement · cited by 620
Cited by15
Results whose statement or proof uses this declaration.
- Set.Infinite.exists_gtproof · cited by 5
- Filter.tendsto_atTop_atTop_of_monotone'proof · cited by 5
- WithTop.iSup_coe_eq_topproof · cited by 3
- IsPreconnected.Ioi_csInf_subsetproof · cited by 2
- Nat.decreasing_induction_of_not_bddAboveproof · cited by 2
- Ordinal.not_bddAbove_fp_familyproof · cited by 2
- Nat.not_bddAbove_setOfPred_primeproof · cited by 2
- tendsto_add_one_pow_atTop_atTop_of_posproof · cited by 1
- lowerClosure_eq_topproof · cited by 1
- IsPreconnected.eq_univ_of_unboundedproof · cited by 1
- Set.PartiallyWellOrderedOn.bddAbove_preimageproof · cited by 1
- MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurableproof · cited by 1