Documentation Verification Report

WellQuasiOrder

📁 Source: Mathlib/Order/WellQuasiOrder.lean

Statistics

Metric	Count
Definitions `WellQuasiOrdered`, `WellQuasiOrderedLE`	2
Theorems `to_wellQuasiOrderedLE`, `wellQuasiOrdered`, `finite_of_wellQuasiOrdered`, `wellQuasiOrderedLE_iff`, `wellQuasiOrderedLE`, `wellQuasiOrdered_iff`, `exists_monotone_subseq`, `pi`, `prod`, `wellFounded`, `finite_of_isAntichain`, `to_wellFoundedLT`, `wqo`, `instWellQuasiOrderedLEOfWellFoundedLT`, `instWellQuasiOrderedLEProd`, `wellQuasiOrderedLE_def`, `wellQuasiOrderedLE_iff`, `wellQuasiOrderedLE_iff_wellFoundedLT`, `wellQuasiOrdered_iff_exists_monotone_subseq`, `wellQuasiOrdered_le`, `wellQuasiOrdered_of_isEmpty`	21
Total	23

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to_wellQuasiOrderedLE` 📖	mathematical	—	`WellQuasiOrderedLE` `Preorder.toLE`	—	`wellQuasiOrdered` `instReflLe`
`wellQuasiOrdered` 📖	mathematical	—	`WellQuasiOrdered`	—	`Set.Finite.exists_lt_map_eq_of_forall_mem` `instInfiniteNat` `Set.mem_univ` `Set.finite_univ` `refl`

IsAntichain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_of_wellQuasiOrdered` 📖	mathematical	`IsAntichain` `WellQuasiOrdered`	`Set.Finite`	—	`LT.lt.ne` `Function.Embedding.injective` `Subtype.val_injective` `eq`

OrderIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`wellQuasiOrderedLE_iff` 📖	mathematical	—	`WellQuasiOrderedLE`	—	`RelIso.wellQuasiOrdered_iff`

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`wellQuasiOrderedLE` 📖	mathematical	`WellQuasiOrderedLE` `Preorder.toLE`	`hasLe`	—	`WellQuasiOrdered.pi` `instIsPreorderLe` `WellQuasiOrderedLE.wqo`

RelIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`wellQuasiOrdered_iff` 📖	mathematical	—	`WellQuasiOrdered`	—	`Equiv.forall_congr` `map_rel_iff`

WellQuasiOrdered

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_monotone_subseq` 📖	mathematical	`WellQuasiOrdered`	`DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding`	—	`exists_increasing_or_nonincreasing_subseq` `IsPreorder.toIsTrans` `LE.le.lt_or_eq` `refl_of` `IsPreorder.toRefl`
`pi` 📖	—	`IsPreorder` `WellQuasiOrdered`	—	—	`Finset.cons_induction` `instIsEmptyFalse` `exists_monotone_subseq` `Finset.forall_mem_cons` `OrderHomClass.mono` `RelEmbedding.instRelHomClass` `wellQuasiOrdered_iff_exists_monotone_subseq` `refl` `IsPreorder.toRefl` `trans` `IsPreorder.toIsTrans`
`prod` 📖	—	`WellQuasiOrdered`	—	—	`exists_monotone_subseq` `OrderEmbedding.strictMono` `LT.lt.le`
`wellFounded` 📖	—	`WellQuasiOrdered`	—	—	`refl_of` `IsPreorder.toRefl` `trans_of` `IsPreorder.toIsTrans` `wellFounded_lt` `WellQuasiOrderedLE.to_wellFoundedLT`

WellQuasiOrderedLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_of_isAntichain` 📖	mathematical	`IsAntichain` `Preorder.toLE`	`Set.Finite`	—	`IsAntichain.finite_of_wellQuasiOrdered` `wellQuasiOrdered_le`
`to_wellFoundedLT` 📖	mathematical	—	`WellFoundedLT` `Preorder.toLT`	—	`WellFoundedLT.eq_1` `isWellFounded_iff` `RelEmbedding.wellFounded_iff_isEmpty` `instIsStrictOrderLt` `wellQuasiOrdered_le` `LT.lt.not_ge` `RelEmbedding.map_rel_iff`
`wqo` 📖	mathematical	—	`WellQuasiOrdered`	—	—

(root)

Definitions

Name	Category	Theorems
`WellQuasiOrdered` 📖	MathDef	8 math math: `wellQuasiOrdered_of_isEmpty`, `wellQuasiOrderedLE_def`, `Finite.wellQuasiOrdered`, `WellQuasiOrderedLE.wqo`, `wellQuasiOrdered_iff_exists_monotone_subseq`, `RelIso.wellQuasiOrdered_iff`, `Set.partiallyWellOrderedOn_univ_iff`, `wellQuasiOrdered_le`
`WellQuasiOrderedLE` 📖	CompData	9 math math: `instWellQuasiOrderedLEOfWellFoundedLT`, `Set.isPWO_univ_iff`, `Finite.to_wellQuasiOrderedLE`, `OrderIso.wellQuasiOrderedLE_iff`, `wellQuasiOrderedLE_def`, `wellQuasiOrderedLE_iff_wellFoundedLT`, `Finsupp.wellQuasiOrderedLE`, `wellQuasiOrderedLE_iff`, `instWellQuasiOrderedLEProd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instWellQuasiOrderedLEOfWellFoundedLT` 📖	mathematical	—	`WellQuasiOrderedLE` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`wellQuasiOrderedLE_iff_wellFoundedLT`
`instWellQuasiOrderedLEProd` 📖	mathematical	—	`WellQuasiOrderedLE` `Prod.instLE_mathlib` `Preorder.toLE`	—	`WellQuasiOrdered.prod` `instIsPreorderLe` `wellQuasiOrdered_le`
`wellQuasiOrderedLE_def` 📖	mathematical	—	`WellQuasiOrderedLE` `WellQuasiOrdered`	—	—
`wellQuasiOrderedLE_iff` 📖	mathematical	—	`WellQuasiOrderedLE` `Preorder.toLE` `WellFoundedLT` `Preorder.toLT` `Set.Finite`	—	`WellQuasiOrderedLE.to_wellFoundedLT` `WellQuasiOrderedLE.finite_of_isAntichain` `exists_increasing_or_nonincreasing_subseq` `instIsTransGt` `RelEmbedding.not_wellFounded` `instIsStrictOrderLt` `instAsymmGt` `IsWellFounded.wf` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_and_eq` `Mathlib.Tactic.Push.not_forall_eq` `lt_trichotomy` `OrderEmbedding.strictMono` `lt_of_le_not_ge` `Set.infinite_range_of_injective` `instInfiniteNat` `le_rfl`
`wellQuasiOrderedLE_iff_wellFoundedLT` 📖	mathematical	—	`WellQuasiOrderedLE` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `WellFoundedLT` `Preorder.toLT`	—	`wellQuasiOrderedLE_iff` `Set.Subsingleton.finite` `IsAntichain.subsingleton` `instTrichotomousLe`
`wellQuasiOrdered_iff_exists_monotone_subseq` 📖	mathematical	—	`WellQuasiOrdered` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding`	—	`WellQuasiOrdered.exists_monotone_subseq` `OrderEmbedding.strictMono`
`wellQuasiOrdered_le` 📖	mathematical	—	`WellQuasiOrdered`	—	`WellQuasiOrderedLE.wqo`
`wellQuasiOrdered_of_isEmpty` 📖	mathematical	—	`WellQuasiOrdered`	—	—

---

← Back to Index