Theorems · Theorem · order theory
Order.krullDim_eq_bot_iff
∀ {α : Type u_1} [inst : Preorder α], Order.krullDim α = ⊥ ↔ IsEmpty α- Defined in
- Mathlib.Order.KrullDimension
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 34 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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
- ENatstatement and proof · cited by 4,985
- Bot.botstatement and proof · cited by 4,720
- WithBotstatement and proof · cited by 1,498
- IsEmptystatement and proof · cited by 759
- RelSeries.lengthproof · cited by 195
- eq_bot_iffproof · cited by 159
- RelSeries.toFunproof · cited by 114
- LTSeriesproof · cited by 87
- Order.krullDimstatement · cited by 82
- iSup_le_iffproof · cited by 45
Cited by4
Results whose statement or proof uses this declaration.
- Order.krullDim_eq_botproof · cited by 5
- Order.finiteDimensionalOrder_iff_krullDim_ne_bot_and_topproof · cited by 3
- Order.krullDim_ne_bot_iffproof · cited by 1
- Order.krullDim_nonneg_iffproof · cited by 1