Mathlib Map

Theorems · Theorem · order theory

Finite.wellQuasiOrdered

∀ {α : Type u_1} (r : α → α → Prop) [Finite α] [Std.Refl r], WellQuasiOrdered r
Defined in
Mathlib.Order.WellQuasiOrder
Cited by
2 results in Mathlib
Foundations
Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FiniteStd.Refl
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.Finite.partiallyWellOrderedOn · cited by 5Finite.partiallyWellOrder…Finite.to_wellQuasiOrderedLE · cited by 0Finite.to_wellQuasiOrdere…Finite · cited by 3029FiniteSet.mem_univ · cited by 416Set.mem_univrefl · cited by 80reflSet.finite_univ · cited by 52Set.finite_univWellQuasiOrdered · cited by 15WellQuasiOrderedSet.Finite.exists_lt_map_eq_of_forall_mem · cited by 6Finite.exists_lt_map_eq_o…Finite.wellQuasiOrderedCITED BYCITES

Cites6

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

Cited by2

Results whose statement or proof uses this declaration.