Theorems · Definition · order theory
Set.IsWF
{α : Type u_2} → [LT α] → Set α → Props.IsWF indicates that < is well-founded when restricted to s.
- Defined in
- Mathlib.Order.WellFoundedSet
- Cited by
- 47 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- LT
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.
- Setstatement and proof · cited by 53,352
- Set.WellFoundedOnproof · cited by 53
Cited by48
Results whose statement or proof uses this declaration.
- Set.IsWF.minstatement and proof · cited by 47
- HahnSeries.isWF_supportstatement · cited by 33
- Set.IsWF.min_memstatement and proof · cited by 20
- Set.IsWF.min_lestatement and proof · cited by 14
- Set.IsWF.isPWOstatement · cited by 13
- Set.IsPWO.isWFstatement · cited by 9
- Set.IsWF.min_le_min_of_subsetstatement and proof · cited by 7
- Set.IsWF.not_lt_minstatement and proof · cited by 7
- Set.IsWF.le_min_iffstatement and proof · cited by 5
- Set.Finite.isWFstatement · cited by 4
- Set.IsWF.min_addstatement and proof · cited by 3
- Set.IsWF.min.congr_simpstatement and proof · cited by 3