Theorems · Theorem · order theory
StrictMono.not_bddAbove_range_of_wellFoundedLT
∀ {β : Type u_2} [inst : LinearOrder β] {f : β → β} [WellFoundedLT β] [NoMaxOrder β],
StrictMono f → ¬BddAbove (Set.range f)- Defined in
- Mathlib.Order.WellFounded
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LinearOrderstatement and proof · cited by 8,572
- Set.rangestatement and proof · cited by 4,705
- LE.le.trans_ltproof · cited by 795
- StrictMonostatement and proof · cited by 706
- LT.lt.trans_leproof · cited by 678
- BddAbovestatement and proof · cited by 620
- WellFoundedLTstatement and proof · cited by 491
- NoMaxOrderstatement and proof · cited by 340
- Set.mem_range_selfproof · cited by 328
- upperBoundsproof · cited by 263
- LT.lt.falseproof · cited by 66
- NoMaxOrder.exists_gtproof · cited by 62
Cited by2
Results whose statement or proof uses this declaration.
- Ordinal.enumOrd_rangeproof · cited by 1
- StrictMono.not_bddBelow_range_of_wellFoundedGTproof · cited by 0