Mathlib Map

Theorems · Theorem · order theory

IsWellFounded.wf

∀ {α : Type u} {r : α → α → Prop} [self : IsWellFounded α r], WellFounded r

The relation is WellFounded, as a proposition.

Defined in
Mathlib.Order.RelClasses
Cited by
43 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Assumes
IsWellFounded
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

wellFounded_lt · cited by 22wellFounded_ltwellFounded_dvdNotUnit · cited by 7wellFounded_dvdNotUnitisArtinian_of_tower · cited by 6isArtinian_of_towerIsWellFounded.apply · cited by 5IsWellFounded.applyIsWellFounded.induction · cited by 5IsWellFounded.inductionwellFounded_gt · cited by 5wellFounded_gtSubrelation.isWellFounded · cited by 4Subrelation.isWellFoundedOrderEmbedding.wellFoundedLT · cited by 3OrderEmbedding.wellFounde…Pi.toLex_strictMono · cited by 3Pi.toLex_strictMonowellFoundedGT_iff_monotone_chain_condition' · cited by 3wellFoundedGT_iff_monoton…isArtinian_of_injective · cited by 2isArtinian_of_injectiveisArtinian_of_surjective · cited by 2isArtinian_of_surjectiveexists_covBy_of_wellFoundedLT · cited by 2exists_covBy_of_wellFound…exists_covBy_seq_of_wellFoundedLT_wellFoundedGT · cited by 2exists_covBy_seq_of_wellF…IsWellFounded.fix_eq · cited by 2IsWellFounded.fix_eqIsWellFounded · cited by 18IsWellFoundedIsWellFounded.wfCITED BYCITES

Cites1

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

Cited by45

Results whose statement or proof uses this declaration.