Theorems · Theorem · order theory
StrictMono.not_bddAbove_range_of_isSuccArchimedean
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [Nonempty α] [inst_2 : Preorder β] {f : α → β} [NoMaxOrder α]
[inst_4 : SuccOrder β] [IsSuccArchimedean β], StrictMono f → ¬BddAbove (Set.range f)- Defined in
- Mathlib.Order.SuccPred.Archimedean
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement and proof · cited by 7,952
- Set.rangestatement and proof · cited by 4,705
- LE.le.trans_ltproof · cited by 795
- StrictMonostatement and proof · cited by 706
- BddAbovestatement and proof · cited by 620
- SuccOrderstatement and proof · cited by 574
- NoMaxOrderstatement and proof · cited by 340
- Set.mem_range_selfproof · cited by 328
- LT.lt.not_geproof · cited by 305
- upperBoundsproof · cited by 263
- IsSuccArchimedeanstatement and proof · cited by 88
- NoMaxOrder.exists_gtproof · cited by 62
Cited by2
Results whose statement or proof uses this declaration.
- StrictAnti.not_bddBelow_range_of_isPredArchimedeanproof · cited by 0
- StrictMono.not_bddBelow_range_of_isSuccArchimedeanproof · cited by 0