Structures · Order
IsWellOrder
A well order is a well-founded linear order.
- Defined in
- Mathlib.Order.RelClasses
- Shape
- 2 explicit arguments
Extends2
Extended by1
Forgetful instances
Concrete types that are instances8
- WellOrder.α
- Subtype
- Prod
- ULift
- Fin
- WithTop
- WithBot
- Sum
How is a type an instance?
Loading the hierarchy index…
Assumed by126
- Ordinal.type
- Ordinal.typein
- Ordinal.enum
- Ordinal.typein_lt_type
- Ordinal.typein_enum
- Ordinal.bfamilyOfFamily'
- Ordinal.familyOfBFamily'
- Ordinal.enum_typein
- Ordinal.card_type
- RelIso.ordinalType_congr
- InitialSeg.eq
- Ordinal.type_ne_zero_iff_nonempty
- RelEmbedding.isWellOrder
- Ordinal.type_fintype
- Ordinal.enum_lt_enum
- Ordinal.blsub_eq_lsub'
- Ordinal.typein_lt_typein
- Ordinal.type_eq
- Ordinal.enum_le_enum
- Ordinal.bsup'_eq_iSup
- Ordinal.type_eq_zero_of_empty
- Ordinal.type_le_iff'
- Ordinal.bfamilyOfFamily'_typein
- Ordinal.iSup'_eq_bsup
- RelIso.ordinal_lift_type_eq
- Cardinal.ord_le_type
- IsWellOrder.linearOrder
- Ordinal.typein_le_typein
- RelEmbedding.ordinal_type_le
- Ordinal.range_familyOfBFamily'
- InitialSeg.antisymm
- RelEmbedding.collapse
- Ordinal.lsub_eq_blsub'
- Ordinal.typein_inj
- Ordinal.familyOfBFamily'_enum
- Ordinal.type_eq_one_of_unique
- Ordinal.enum_type
- InitialSeg.principalSumRelIso
- Cardinal.card_typein_lt
- InitialSeg.transPrincipal
- InitialSeg.toPrincipalSeg
- InitialSeg.eq_principalSeg
- Ordinal.type_eq_zero_iff_isEmpty
- Ordinal.card_typein_min_le_mk
- Cardinal.mk_bounded_subset
- Ordinal.typein_surj
- Ordinal.relIso_enum'
- PrincipalSeg.eq
- Ordinal.lift_type_le
- Ordinal.bounded_singleton