Structures · Order
IsWellFounded
A well-founded relation. Not to be confused with IsWellOrder.
- Defined in
- Mathlib.Order.RelClasses
- Shape
- 2 explicit arguments · adds wf
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Forgetful instances
Every IsWellFounded is also a
Concrete types that are instances9
- Class
- ZFSet
- PSet
- List.chains
- Subtype
- Prod
- Set.Elem
- Multiset
- Finset
How is a type an instance?
Loading the hierarchy index…
Assumed by31
- IsWellFounded.wf
- IsWellFounded.rank
- IsWellFounded.apply
- IsWellFounded.induction
- Subrelation.isWellFounded
- IsWellFounded.rank_lt_of_rel
- IsWellFounded.fix_eq
- IsWellFounded.rank_eq
- isCofinal_setOfPred_imp_lt
- IsWellFounded.mem_range_rank_of_le
- RelHomClass.isWellFounded
- IsWellFounded.fix
- isCofinal_setOf_imp_lt
- InitialSeg.subsingleton_of_trichotomous_of_irrefl
- WellFounded.instIsWellFoundedOnFun
- IsWellFounded.toWellFoundedRelation
- instIsWellFoundedTransGen
- IsWellFounded.wellOrderExtension.isWellOrder_lt
- WellFounded.not_rel_apply_succ
- Prod.Lex.instIsWellFounded
- Relation.instIsWellFoundedMultisetCutExpand
- instAsymmOfIsWellFounded
- instIsWellFoundedInvImage
- Cycle.Chain.eq_nil_of_well_founded
- IsWellFounded.exists_well_order_ge
- IsWellFounded.rank.congr_simp
- IsWellFounded.wellOrderExtension.isWellFounded_lt
- Subrel.instIsWellFoundedSubtype
- instIsWellFoundedChainsLex_chains
- IsWellFounded.wellOrderExtension
- RelEmbedding.isWellFounded