Theorems · Theorem · order theory
wellFounded_lt
∀ {α : Type u} [inst : LT α] [WellFoundedLT α], WellFounded fun x1 x2 => x1 < x2- Defined in
- Mathlib.Order.RelClasses
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
- Assumes
- LTWellFoundedLT
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- WellFoundedLTstatement and proof · cited by 491
- IsWellFounded.wfproof · cited by 43
Cited by22
Results whose statement or proof uses this declaration.
- StrictMono.id_leproof · cited by 14
- Polynomial.degree_lt_wfproof · cited by 7
- InnerProductSpace.gramSchmidt_orthogonalproof · cited by 6
- MvPowerSeries.coeff_eq_zero_of_lt_lexOrderproof · cited by 5
- not_strictAnti_of_wellFoundedLTproof · cited by 5
- Field.Emb.Cardinal.isLeast_leastExtproof · cited by 4
- Finset.exists_inf_leproof · cited by 3
- WellQuasiOrdered.wellFoundedproof · cited by 2
- exists_covBy_of_wellFoundedLTproof · cited by 2
- exists_covBy_seq_of_wellFoundedLT_wellFoundedGTproof · cited by 2
- TopologicalSpace.NoetherianSpace.exists_finite_set_closeds_irreducibleproof · cited by 2
- WellFoundedLT.finite_of_sSupIndepproof · cited by 2