Mathlib Map

Theorems · Definition · order theory

WellFoundedLT.toOrderBot

(α : Type u_4) → [inst : LinearOrder α] → [Nonempty α] → [h : WellFoundedLT α] → OrderBot α

A nonempty linear order with well-founded < has a bottom element.

Defined in
Mathlib.Order.WellFounded
Cited by
8 results in Mathlib
Foundations
Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
LinearOrderNonemptyWellFoundedLT
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Order.IsNormal.dirSupClosed_range · cited by 2IsNormal.dirSupClosed_ran…Cardinal.orderBotAleph0OrdToType · cited by 1Cardinal.orderBotAleph0Or…Order.IsNormal.exists_map_le_lt_map_succ_of_exists_ge · cited by 1IsNormal.exists_map_le_lt…ciInf_eq_iff · cited by 1ciInf_eq_iffCategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_ordinal · cited by 1generatingMonomorphisms.e…CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_transfiniteCompositionOfShape · cited by 1generatingMonomorphisms.e…CategoryTheory.MorphismProperty.isRightAdjoint_ι_isLocal · cited by 1MorphismProperty.isRightA…csInf_eq_iff · cited by 0csInf_eq_iffOrder.isNormal_enum_iff_dirSupClosed · cited by 0Order.isNormal_enum_iff_d…LinearOrder · cited by 8572LinearOrderOrderBot · cited by 1055OrderBotWellFoundedLT · cited by 491WellFoundedLTWellFoundedLT.toOrderBotCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by9

Results whose statement or proof uses this declaration.