WellFoundedSet

📁 Source: Mathlib/Order/WellFoundedSet.lean

Statistics

Metric	Count
Definitions `IsPWO`, `IsWF`, `min`, `PartiallyWellOrderedOn`, `IsBadSeq`, `IsMinBadSeq`, `minBadSeqOfBadSeq`, `WellFoundedOn`	8
Theorems `wellFoundedOn_gt`, `isWF`, `wellFoundedOn_lt`, `isPWO`, `isPWO_bUnion`, `isPWO_sup`, `isWF`, `isWF_bUnion`, `isWF_sup`, `partiallyWellOrderedOn`, `partiallyWellOrderedOn_bUnion`, `partiallyWellOrderedOn_sup`, `wellFoundedOn`, `wellFoundedOn_bUnion`, `wellFoundedOn_sup`, `finite_of_partiallyWellOrderedOn`, `partiallyWellOrderedOn_iff`, `isPWO`, `isPWO`, `isWF`, `partiallyWellOrderedOn`, `wellFoundedOn`, `exists_le_minimal`, `exists_minimal`, `exists_minimalFor`, `exists_monotone_subseq`, `image_of_monotone`, `image_of_monotoneOn`, `insert`, `isWF`, `mono`, `of_linearOrder`, `pi`, `prod`, `union`, `subset`, `insert`, `isPWO`, `le_min_iff`, `min_eq_of_le`, `min_eq_of_lt`, `min_le`, `min_le_min_of_subset`, `min_mem`, `min_of_subset_not_lt_min`, `min_union`, `mono`, `not_lt_min`, `of_wellFoundedLT`, `union`, `ProdLex_iff`, `bddAbove_preimage`, `exists_lt`, `exists_min_bad_of_exists_bad`, `exists_monotone_subseq`, `exists_notMem_of_gt`, `fiberProdLex`, `iff_forall_not_isBadSeq`, `iff_not_exists_isMinBadSeq`, `imageProdLex`, `image_of_monotone_on`, `insert`, `mono`, `partiallyWellOrderedOn_sublistForall₂`, `pi`, `prod`, `subsetProdLex`, `union`, `wellFoundedOn`, `isPWO`, `isWF`, `partiallyWellOrderedOn`, `wellFoundedOn`, `acc_iff_wellFoundedOn`, `induction`, `insert`, `mapsTo`, `mono`, `mono'`, `prod_lex_of_wellFoundedOn_fiber`, `sdiff_singleton`, `sigma_lex_of_wellFoundedOn_fiber`, `subset`, `union`, `isPWO_empty`, `isPWO_iff_exists_monotone_subseq`, `isPWO_iff_isWF`, `isPWO_insert`, `isPWO_of_finite`, `isPWO_of_wellQuasiOrderedLE`, `isPWO_singleton`, `isPWO_union`, `isPWO_univ_iff`, `isWF_empty`, `isWF_iff_no_descending_seq`, `isWF_insert`, `isWF_min_singleton`, `isWF_singleton`, `isWF_union`, `isWF_univ_iff`, `partiallyWellOrderedOn_empty`, `partiallyWellOrderedOn_iff_exists_lt`, `partiallyWellOrderedOn_iff_exists_monotone_subseq`, `partiallyWellOrderedOn_iff_finite_antichains`, `partiallyWellOrderedOn_insert`, `partiallyWellOrderedOn_of_wellQuasiOrdered`, `partiallyWellOrderedOn_singleton`, `partiallyWellOrderedOn_union`, `partiallyWellOrderedOn_univ_iff`, `wellFoundedOn_empty`, `wellFoundedOn_iff`, `wellFoundedOn_iff_no_descending_seq`, `wellFoundedOn_image`, `wellFoundedOn_insert`, `wellFoundedOn_range`, `wellFoundedOn_sdiff_singleton`, `wellFoundedOn_singleton`, `wellFoundedOn_union`, `wellFoundedOn_univ`, `prod_lex_of_wellFoundedOn_fiber`, `sigma_lex_of_wellFoundedOn_fiber`, `wellFoundedOn`	122
Total	130

BddAbove

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`wellFoundedOn_gt` 📖	mathematical	`BddAbove` `Preorder.toLE`	`Set.WellFoundedOn` `Preorder.toLT`	—	`BddBelow.wellFoundedOn_lt` `dual`

BddBelow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isWF` 📖	mathematical	`BddBelow` `Preorder.toLE`	`Set.IsWF` `Preorder.toLT`	—	`wellFoundedOn_lt`
`wellFoundedOn_lt` 📖	mathematical	`BddBelow` `Preorder.toLE`	`Set.WellFoundedOn` `Preorder.toLT`	—	`Set.wellFoundedOn_iff_no_descending_seq` `instIsStrictOrderLt` `Set.infinite_range_of_injective` `instInfiniteNat` `RelEmbedding.injective` `Set.Finite.subset` `Set.finite_Icc` `Set.range_subset_iff` `antitone_iff_forall_lt` `LT.lt.le` `RelEmbedding.map_rel_iff`

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPWO` 📖	mathematical	—	`Set.IsPWO` `SetLike.coe` `Finset` `instSetLike`	—	`partiallyWellOrderedOn` `instReflLe`
`isPWO_bUnion` 📖	mathematical	—	`Set.IsPWO` `Set.iUnion` `Finset` `instMembership`	—	`partiallyWellOrderedOn_bUnion`
`isPWO_sup` 📖	mathematical	—	`Set.IsPWO` `sup` `Set` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`partiallyWellOrderedOn_sup`
`isWF` 📖	mathematical	—	`Set.IsWF` `Preorder.toLT` `SetLike.coe` `Finset` `instSetLike`	—	`Set.Finite.isWF` `finite_toSet`
`isWF_bUnion` 📖	mathematical	—	`Set.IsWF` `Preorder.toLT` `Set.iUnion` `Finset` `instMembership`	—	`wellFoundedOn_bUnion` `instIsStrictOrderLt`
`isWF_sup` 📖	mathematical	—	`Set.IsWF` `Preorder.toLT` `sup` `Set` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`wellFoundedOn_sup` `instIsStrictOrderLt`
`partiallyWellOrderedOn` 📖	mathematical	—	`Set.PartiallyWellOrderedOn` `SetLike.coe` `Finset` `instSetLike`	—	`Set.Finite.partiallyWellOrderedOn` `finite_toSet`
`partiallyWellOrderedOn_bUnion` 📖	mathematical	—	`Set.PartiallyWellOrderedOn` `Set.iUnion` `Finset` `instMembership`	—	`sup_eq_iSup` `partiallyWellOrderedOn_sup`
`partiallyWellOrderedOn_sup` 📖	mathematical	—	`Set.PartiallyWellOrderedOn` `sup` `Set` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`cons_induction_on` `sup_empty` `instIsEmptyFalse` `sup_cons`
`wellFoundedOn` 📖	mathematical	—	`Set.WellFoundedOn` `SetLike.coe` `Finset` `instSetLike`	—	`isWF`
`wellFoundedOn_bUnion` 📖	mathematical	—	`Set.WellFoundedOn` `Set.iUnion` `Finset` `instMembership`	—	`sup_eq_iSup` `wellFoundedOn_sup`
`wellFoundedOn_sup` 📖	mathematical	—	`Set.WellFoundedOn` `sup` `Set` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`cons_induction_on` `sup_empty` `instIsEmptyFalse` `sup_cons`

IsAntichain

Theorems

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

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPWO` 📖	mathematical	`WellQuasiOrderedLE` `Preorder.toLE`	`Set.IsPWO` `preorder`	—	`Set.isPWO_of_wellQuasiOrderedLE` `wellQuasiOrderedLE`

Set

Definitions

Name	Category	Theorems
`IsPWO` 📖	MathDef	26 math math: `HahnSeries.SummableFamily.isPWO_iUnion_support'`, `HahnSeries.isPWO_support`, `HVertexOperator.coeff_isPWOsupport`, `Pi.isPWO`, `isPWO_univ_iff`, `HahnSeries.SummableFamily.isPWO_iUnion_support`, `isPWO_insert`, `isPWO_union`, `HahnSeries.isPWO_support'`, `isPWO_iff_exists_monotone_subseq`, `Finsupp.isPWO`, `Finite.isPWO`, `Subsingleton.isPWO`, `HahnSeries.SummableFamily.isPWO_iUnion_support_powers`, `Finset.isPWO_sup`, `HahnSeries.suppBddBelow_supp_PWO`, `isPWO_singleton`, `IsWF.isPWO`, `isPWO_empty`, `Finset.isPWO_bUnion`, `Finset.isPWO`, `isPWO_of_wellQuasiOrderedLE`, `isPWO_iff_isWF`, `isPWO_of_finite`, `IsPWO.of_linearOrder`, `PartiallyWellOrderedOn.ProdLex_iff`
`IsWF` 📖	MathDef	17 math math: `isWF_insert`, `Finset.isWF_sup`, `HahnEmbedding.Partial.isWF_support_evalCoeff`, `isWF_union`, `isWF_empty`, `IsPWO.isWF`, `Finset.isWF_bUnion`, `isWF_singleton`, `BddBelow.isWF`, `isWF_univ_iff`, `isPWO_iff_isWF`, `Finite.isWF`, `Subsingleton.isWF`, `isWF_iff_no_descending_seq`, `IsWF.of_wellFoundedLT`, `HahnSeries.isWF_support`, `Finset.isWF`
`PartiallyWellOrderedOn` 📖	MathDef	17 math math: `partiallyWellOrderedOn_insert`, `partiallyWellOrderedOn_iff_exists_lt`, `Finite.partiallyWellOrderedOn`, `Finset.partiallyWellOrderedOn`, `Subsingleton.partiallyWellOrderedOn`, `partiallyWellOrderedOn_singleton`, `partiallyWellOrderedOn_of_wellQuasiOrdered`, `Finset.partiallyWellOrderedOn_sup`, `partiallyWellOrderedOn_empty`, `PartiallyWellOrderedOn.iff_not_exists_isMinBadSeq`, `partiallyWellOrderedOn_iff_finite_antichains`, `partiallyWellOrderedOn_union`, `partiallyWellOrderedOn_univ_iff`, `partiallyWellOrderedOn_iff_exists_monotone_subseq`, `Finset.partiallyWellOrderedOn_bUnion`, `IsAntichain.partiallyWellOrderedOn_iff`, `PartiallyWellOrderedOn.iff_forall_not_isBadSeq`
`WellFoundedOn` 📖	MathDef	27 math math: `LinearOrderedAddCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete`, `wellFoundedOn_empty`, `Finite.wellFoundedOn`, `WellFounded.wellFoundedOn`, `Finset.wellFoundedOn_bUnion`, `BddBelow.wellFoundedOn_lt`, `PartiallyWellOrderedOn.wellFoundedOn`, `BddAbove.wellFoundedOn_gt`, `wellFoundedOn_iff`, `LinearOrderedCommGroup.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete`, `wellFoundedOn_insert`, `Subsingleton.wellFoundedOn`, `WellFoundedOn.acc_iff_wellFoundedOn`, `wellFoundedOn_univ`, `wellFoundedOn_image`, `wellFoundedOn_iff_no_descending_seq`, `Ideal.setOf_isPrincipal_wellFoundedOn_gt`, `LinearOrderedCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete`, `LinearOrderedAddCommGroup.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete`, `wellFoundedOn_range`, `LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero`, `wellFoundedOn_sdiff_singleton`, `Finset.wellFoundedOn_sup`, `wellFoundedOn_union`, `Finset.wellFoundedOn`, `wellFoundedOn_singleton`, `LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPWO_empty` 📖	mathematical	—	`IsPWO` `Set` `instEmptyCollection`	—	`Finite.isPWO` `finite_empty`
`isPWO_iff_exists_monotone_subseq` 📖	mathematical	—	`IsPWO` `Monotone` `Nat.instPreorder` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding`	—	`partiallyWellOrderedOn_iff_exists_monotone_subseq` `instIsPreorderLe`
`isPWO_iff_isWF` 📖	mathematical	—	`IsPWO` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsWF` `Preorder.toLT`	—	`wellQuasiOrderedLE_def` `isWellFounded_iff` `wellQuasiOrderedLE_iff_wellFoundedLT`
`isPWO_insert` 📖	mathematical	—	`IsPWO` `Set` `instInsert`	—	—
`isPWO_of_finite` 📖	mathematical	—	`IsPWO`	—	`Finite.isPWO` `toFinite` `Subtype.finite`
`isPWO_of_wellQuasiOrderedLE` 📖	mathematical	—	`IsPWO`	—	`partiallyWellOrderedOn_of_wellQuasiOrdered` `WellQuasiOrderedLE.wqo`
`isPWO_singleton` 📖	mathematical	—	`IsPWO` `Set` `instSingletonSet`	—	`Finite.isPWO` `finite_singleton`
`isPWO_union` 📖	mathematical	—	`IsPWO` `Set` `instUnion`	—	`partiallyWellOrderedOn_union`
`isPWO_univ_iff` 📖	mathematical	—	`IsPWO` `univ` `WellQuasiOrderedLE` `Preorder.toLE`	—	`partiallyWellOrderedOn_univ_iff` `wellQuasiOrderedLE_def`
`isWF_empty` 📖	mathematical	—	`IsWF` `Set` `instEmptyCollection`	—	`wellFounded_of_isEmpty` `instIsEmptyElemEmptyCollection`
`isWF_iff_no_descending_seq` 📖	mathematical	—	`IsWF` `Preorder.toLT` `Set` `instMembership`	—	`wellFoundedOn_iff_no_descending_seq` `instIsStrictOrderLt` `StrictAnti.injective` `StrictAnti.lt_iff_gt` `RelEmbedding.map_rel_iff`
`isWF_insert` 📖	mathematical	—	`IsWF` `Preorder.toLT` `Set` `instInsert`	—	—
`isWF_min_singleton` 📖	mathematical	`IsWF` `Preorder.toLT` `Set` `instSingletonSet` `Nonempty`	`IsWF.min`	—	`eq_of_mem_singleton` `IsWF.min_mem`
`isWF_singleton` 📖	mathematical	—	`IsWF` `Preorder.toLT` `Set` `instSingletonSet`	—	`Finite.isWF` `finite_singleton`
`isWF_union` 📖	mathematical	—	`IsWF` `Preorder.toLT` `Set` `instUnion`	—	`wellFoundedOn_union` `instIsStrictOrderLt`
`isWF_univ_iff` 📖	mathematical	—	`IsWF` `univ` `WellFoundedLT`	—	—
`partiallyWellOrderedOn_empty` 📖	mathematical	—	`PartiallyWellOrderedOn` `Set` `instEmptyCollection`	—	`wellQuasiOrdered_of_isEmpty` `instIsEmptyElemEmptyCollection`
`partiallyWellOrderedOn_iff_exists_lt` 📖	mathematical	—	`PartiallyWellOrderedOn`	—	`PartiallyWellOrderedOn.exists_lt`
`partiallyWellOrderedOn_iff_exists_monotone_subseq` 📖	mathematical	—	`PartiallyWellOrderedOn` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding`	—	`PartiallyWellOrderedOn.exists_monotone_subseq` `PartiallyWellOrderedOn.eq_1` `wellQuasiOrdered_iff_exists_monotone_subseq` `Subrel.instIsPreorderSubtype`
`partiallyWellOrderedOn_iff_finite_antichains` 📖	mathematical	—	`PartiallyWellOrderedOn` `Finite`	—	`IsAntichain.finite_of_partiallyWellOrderedOn` `PartiallyWellOrderedOn.mono` `partiallyWellOrderedOn_iff_exists_lt` `infinite_range_of_injective` `instInfiniteNat` `lt_trichotomy` `Mathlib.Tactic.Push.not_and_eq` `refl` `range_subset_iff` `Ne.lt_or_gt` `symm`
`partiallyWellOrderedOn_insert` 📖	mathematical	—	`PartiallyWellOrderedOn` `Set` `instInsert`	—	—
`partiallyWellOrderedOn_of_wellQuasiOrdered` 📖	mathematical	`WellQuasiOrdered`	`PartiallyWellOrderedOn`	—	`PartiallyWellOrderedOn.mono` `partiallyWellOrderedOn_univ_iff` `subset_univ`
`partiallyWellOrderedOn_singleton` 📖	mathematical	—	`PartiallyWellOrderedOn` `Set` `instSingletonSet`	—	`Finite.partiallyWellOrderedOn` `finite_singleton`
`partiallyWellOrderedOn_union` 📖	mathematical	—	`PartiallyWellOrderedOn` `Set` `instUnion`	—	`PartiallyWellOrderedOn.mono` `subset_union_left` `subset_union_right` `PartiallyWellOrderedOn.union`
`partiallyWellOrderedOn_univ_iff` 📖	mathematical	—	`PartiallyWellOrderedOn` `univ` `WellQuasiOrdered`	—	`RelIso.wellQuasiOrdered_iff`
`wellFoundedOn_empty` 📖	mathematical	—	`WellFoundedOn` `Set` `instEmptyCollection`	—	`wellFounded_of_isEmpty` `instIsEmptyElemEmptyCollection`
`wellFoundedOn_iff` 📖	mathematical	—	`WellFoundedOn` `Set` `instMembership`	—	`Subtype.coe_injective` `WellFounded.wellFounded_iff_has_min` `WellFounded.has_min` `Subtype.preimage_coe_nonempty` `RelEmbedding.wellFounded`
`wellFoundedOn_iff_no_descending_seq` 📖	mathematical	—	`WellFoundedOn` `Set` `instMembership` `DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike`	—	`IsStrictOrder.subset`
`wellFoundedOn_image` 📖	mathematical	—	`WellFoundedOn` `image` `Function.onFun`	—	`image_eq_range` `wellFoundedOn_range`
`wellFoundedOn_insert` 📖	mathematical	—	`WellFoundedOn` `Set` `instInsert`	—	—
`wellFoundedOn_range` 📖	mathematical	—	`WellFoundedOn` `range` `Function.onFun`	—	`WellFounded.mono` `Acc.of_downward_closed`
`wellFoundedOn_sdiff_singleton` 📖	mathematical	—	`WellFoundedOn` `Set` `instSDiff` `instSingletonSet`	—	`wellFoundedOn_insert` `insert_diff_singleton` `insert_eq_of_mem`
`wellFoundedOn_singleton` 📖	mathematical	—	`WellFoundedOn` `Set` `instSingletonSet`	—	`Finite.wellFoundedOn` `finite_singleton`
`wellFoundedOn_union` 📖	mathematical	—	`WellFoundedOn` `Set` `instUnion`	—	`WellFoundedOn.subset` `subset_union_left` `subset_union_right` `WellFoundedOn.union`
`wellFoundedOn_univ` 📖	mathematical	—	`WellFoundedOn` `univ`	—	—

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPWO` 📖	mathematical	—	`Set.IsPWO`	—	`partiallyWellOrderedOn` `instReflLe`
`isWF` 📖	mathematical	—	`Set.IsWF` `Preorder.toLT`	—	`Set.IsPWO.isWF` `isPWO`
`partiallyWellOrderedOn` 📖	mathematical	—	`Set.PartiallyWellOrderedOn`	—	`Finite.wellQuasiOrdered` `to_subtype` `Subrel.instReflSubtype`
`wellFoundedOn` 📖	mathematical	—	`Set.WellFoundedOn`	—	`isWF`

Set.IsPWO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_le_minimal` 📖	mathematical	`Set.IsPWO` `Set` `Set.instMembership`	`Preorder.toLE` `Minimal`	—	`le_rfl` `WellQuasiOrdered.wellFounded` `Subrel.instIsPreorderSubtype` `instIsPreorderLe` `WellFounded.min_mem` `WellFounded.not_lt_min` `LE.le.trans`
`exists_minimal` 📖	mathematical	`Set.IsPWO` `Set.Nonempty`	`Minimal` `Preorder.toLE` `Set` `Set.instMembership`	—	`exists_le_minimal`
`exists_minimalFor` 📖	mathematical	`Set.IsPWO` `Set.image` `Set.Nonempty`	`MinimalFor` `Preorder.toLE` `Set` `Set.instMembership`	—	`exists_minimal` `Set.Nonempty.image` `Set.mem_image_of_mem`
`exists_monotone_subseq` 📖	mathematical	`Set.IsPWO` `Set` `Set.instMembership`	`Monotone` `Nat.instPreorder` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding`	—	`Set.PartiallyWellOrderedOn.exists_monotone_subseq` `instIsPreorderLe`
`image_of_monotone` 📖	mathematical	`Set.IsPWO` `Monotone`	`Set.image`	—	`Set.PartiallyWellOrderedOn.image_of_monotone_on` `Monotone.monotoneOn`
`image_of_monotoneOn` 📖	mathematical	`Set.IsPWO` `MonotoneOn`	`Set.image`	—	`Set.PartiallyWellOrderedOn.image_of_monotone_on`
`insert` 📖	mathematical	`Set.IsPWO`	`Set` `Set.instInsert`	—	`Set.isPWO_insert`
`isWF` 📖	mathematical	`Set.IsPWO`	`Set.IsWF` `Preorder.toLT`	—	`Set.PartiallyWellOrderedOn.wellFoundedOn` `instIsPreorderLe`
`mono` 📖	—	`Set.IsPWO` `Set` `Set.instHasSubset`	—	—	`Set.PartiallyWellOrderedOn.mono`
`of_linearOrder` 📖	mathematical	—	`Set.IsPWO` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Set.IsWF.isPWO` `Set.IsWF.of_wellFoundedLT`
`pi` 📖	mathematical	`Set.IsPWO`	`Pi.preorder` `Set.pi` `Set.univ`	—	`Set.PartiallyWellOrderedOn.pi` `instIsPreorderLe`
`prod` 📖	mathematical	`Set.IsPWO`	`Prod.instPreorder` `SProd.sprod` `Set` `Set.instSProd`	—	`Set.PartiallyWellOrderedOn.prod` `instIsPreorderLe`
`union` 📖	mathematical	`Set.IsPWO`	`Set` `Set.instUnion`	—	`Set.PartiallyWellOrderedOn.union`

Set.IsStrictOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subset` 📖	mathematical	—	`IsStrictOrder` `Set` `Set.instMembership`	—	`irrefl_of` `IsStrictOrder.toIrrefl` `trans_of` `IsStrictOrder.toIsTrans`

Set.IsWF

Definitions

Name	Category	Theorems
`min` 📖	CompOp	23 math math: `HahnSeries.untop_orderTop_of_ne_zero`, `min_union`, `not_lt_min`, `Finset.smulAntidiagonal_min_smul_min`, `min_mem`, `HahnSeries.orderTop_of_ne`, `Finset.addAntidiagonal_min_add_min`, `min_smul`, `min_of_subset_not_lt_min`, `min_eq_of_lt`, `HahnSeries.orderTop_of_ne_zero`, `HahnSeries.order_of_ne`, `Set.isWF_min_singleton`, `min_eq_of_le`, `le_min_iff`, `min_add`, `min_mul`, `min_le_min_of_subset`, `Finset.mulAntidiagonal_min_mul_min`, `min_le`, `HahnSeries.min_le_min_add`, `min_vadd`, `Finset.vaddAntidiagonal_min_vadd_min`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`insert` 📖	mathematical	`Set.IsWF` `Preorder.toLT`	`Set` `Set.instInsert`	—	`Set.isWF_insert`
`isPWO` 📖	mathematical	`Set.IsWF` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set.IsPWO`	—	`Set.isPWO_iff_isWF`
`le_min_iff` 📖	mathematical	`Set.IsWF` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Nonempty`	`Preorder.toLE` `min`	—	`le_trans` `min_le` `min_mem`
`min_eq_of_le` 📖	mathematical	`Set.IsWF` `Preorder.toLT` `PartialOrder.toPreorder` `Set` `Set.instMembership` `Preorder.toLE`	`min` `Set.nonempty_of_mem`	—	`Set.nonempty_of_mem` `eq_of_le_of_not_lt` `min_mem` `not_lt_min`
`min_eq_of_lt` 📖	mathematical	`Set.IsWF` `Preorder.toLT` `Set` `Set.instMembership`	`min` `Set.nonempty_of_mem`	—	`Set.nonempty_of_mem` `not_lt_min` `min_mem`
`min_le` 📖	mathematical	`Set.IsWF` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Nonempty` `Set` `Set.instMembership`	`Preorder.toLE` `min`	—	`le_of_not_gt` `not_lt_min`
`min_le_min_of_subset` 📖	mathematical	`Set.IsWF` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Nonempty` `Set` `Set.instHasSubset`	`Preorder.toLE` `min`	—	`le_min_iff` `min_le`
`min_mem` 📖	mathematical	`Set.IsWF` `Preorder.toLT` `Set.Nonempty`	`Set` `Set.instMembership` `min`	—	`Set.nonempty_iff_univ_nonempty` `Set.Nonempty.to_subtype`
`min_of_subset_not_lt_min` 📖	mathematical	`Set.IsWF` `Preorder.toLT` `Set.Nonempty` `Set` `Set.instHasSubset`	`min`	—	`not_lt_min` `min_mem`
`min_union` 📖	mathematical	`Set.IsWF` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Nonempty`	`min` `Set` `Set.instUnion` `union` `Set.union_nonempty` `SemilatticeInf.toMin`	—	`le_antisymm` `union` `Set.union_nonempty` `le_min` `min_le_min_of_subset` `Set.subset_union_left` `Set.subset_union_right` `min_le_iff` `min_le` `Set.mem_union` `min_mem`
`mono` 📖	—	`Set.IsWF` `Set` `Set.instHasSubset`	—	—	`Set.WellFoundedOn.subset`
`not_lt_min` 📖	mathematical	`Set.IsWF` `Preorder.toLT` `Set.Nonempty` `Set` `Set.instMembership`	`min`	—	`WellFounded.not_lt_min` `Set.nonempty_iff_univ_nonempty` `Set.Nonempty.to_subtype` `Set.mem_univ`
`of_wellFoundedLT` 📖	mathematical	—	`Set.IsWF`	—	`mono` `Set.isWF_univ_iff` `Set.subset_univ`
`union` 📖	mathematical	`Set.IsWF` `Preorder.toLT`	`Set` `Set.instUnion`	—	`Set.WellFoundedOn.union` `instIsStrictOrderLt`

Set.PartiallyWellOrderedOn

Definitions

Name	Category	Theorems
`IsBadSeq` 📖	MathDef	2 math math: `iff_not_exists_isMinBadSeq`, `iff_forall_not_isBadSeq`
`IsMinBadSeq` 📖	MathDef	2 math math: `exists_min_bad_of_exists_bad`, `iff_not_exists_isMinBadSeq`
`minBadSeqOfBadSeq` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ProdLex_iff` 📖	mathematical	—	`Set.IsPWO` `Lex` `Prod.Lex.instPreorder` `PartialOrder.toPreorder` `Set.image` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `setOf` `Set` `Set.instMembership` `toLex`	—	`imageProdLex` `fiberProdLex` `subsetProdLex`
`bddAbove_preimage` 📖	mathematical	`Set.PartiallyWellOrderedOn`	`BddAbove` `Set.preimage`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `Nat.exists_strictMono_subsequence` `not_bddAbove_iff` `Set.partiallyWellOrderedOn_iff_exists_lt`
`exists_lt` 📖	—	`Set.PartiallyWellOrderedOn` `Set` `Set.instMembership`	—	—	—
`exists_min_bad_of_exists_bad` 📖	mathematical	`IsBadSeq`	`IsMinBadSeq`	—	`LT.lt.le`
`exists_monotone_subseq` 📖	mathematical	`Set.PartiallyWellOrderedOn` `Set` `Set.instMembership`	`DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding`	—	`WellQuasiOrdered.exists_monotone_subseq` `Subrel.instIsPreorderSubtype`
`exists_notMem_of_gt` 📖	mathematical	`Set.PartiallyWellOrderedOn`	`Set` `Set.instMembership`	—	`bddAbove_preimage` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq`
`fiberProdLex` 📖	mathematical	`Set.IsPWO` `Lex` `Prod.Lex.instPreorder`	`setOf` `Set` `Set.instMembership` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`Set.ext` `Set.image_congr` `Set.IsPWO.image_of_monotoneOn` `Set.IsPWO.mono` `Set.inter_subset_left` `Prod.Lex.toLex_le_toLex`
`iff_forall_not_isBadSeq` 📖	mathematical	—	`Set.PartiallyWellOrderedOn` `IsBadSeq`	—	`Set.partiallyWellOrderedOn_iff_exists_lt`
`iff_not_exists_isMinBadSeq` 📖	mathematical	—	`Set.PartiallyWellOrderedOn` `IsBadSeq` `IsMinBadSeq`	—	`iff_forall_not_isBadSeq` `exists_min_bad_of_exists_bad`
`imageProdLex` 📖	mathematical	`Set.IsPWO` `Lex` `Prod.Lex.instPreorder`	`Set.image` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	`Set.IsPWO.image_of_monotone` `Prod.Lex.monotone_fst`
`image_of_monotone_on` 📖	mathematical	`Set.PartiallyWellOrderedOn`	`Set.image`	—	`Set.partiallyWellOrderedOn_iff_exists_lt`
`insert` 📖	mathematical	`Set.PartiallyWellOrderedOn`	`Set` `Set.instInsert`	—	`Set.partiallyWellOrderedOn_insert`
`mono` 📖	—	`Set.PartiallyWellOrderedOn` `Set` `Set.instHasSubset`	—	—	—
`partiallyWellOrderedOn_sublistForall₂` 📖	mathematical	`Set.PartiallyWellOrderedOn`	`setOf` `List.SublistForall₂`	—	`isEmpty_or_nonempty` `Set.Subsingleton.partiallyWellOrderedOn` `List.SublistForall₂.is_refl` `IsPreorder.toRefl` `Set.subsingleton_of_subsingleton` `Unique.instSubsingleton` `iff_not_exists_isMinBadSeq` `exists_monotone_subseq` `List.head!_mem_self` `lt_irrefl` `Mathlib.Tactic.Push.not_and_eq` `Mathlib.Tactic.Push.not_forall_eq` `IsBadSeq.eq_1` `List.tail_subset` `LT.lt.trans` `not_lt` `lt_of_lt_of_le` `OrderEmbedding.monotone` `trans` `List.SublistForall₂.is_trans` `IsPreorder.toIsTrans` `add_comm` `List.tail_sublistForall₂_self` `OrderEmbedding.lt_iff_lt` `le_of_not_gt` `List.cons_head!_tail` `le_of_lt`
`pi` 📖	mathematical	`IsPreorder` `Set.PartiallyWellOrderedOn`	`Set.pi` `Set.univ`	—	`Finset.cons_induction` `instIsEmptyFalse` `exists_monotone_subseq` `Finset.forall_mem_cons` `OrderHomClass.mono` `RelEmbedding.instRelHomClass` `Set.partiallyWellOrderedOn_iff_exists_monotone_subseq` `refl` `IsPreorder.toRefl` `trans` `IsPreorder.toIsTrans`
`prod` 📖	mathematical	`Set.PartiallyWellOrderedOn`	`SProd.sprod` `Set` `Set.instSProd`	—	`Set.partiallyWellOrderedOn_iff_exists_lt` `exists_monotone_subseq` `exists_lt` `OrderEmbedding.strictMono` `LT.lt.le`
`subsetProdLex` 📖	mathematical	`Set.IsPWO` `PartialOrder.toPreorder` `Set.image` `Lex` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `setOf` `Set` `Set.instMembership` `toLex`	`Prod.Lex.instPreorder`	—	`Set.IsPWO.eq_1` `Set.partiallyWellOrderedOn_iff_exists_lt` `Set.isPWO_iff_exists_monotone_subseq` `Set.mem_image_of_mem` `Prod.Lex.toLex_le_toLex` `LE.le.eq_of_not_lt`
`union` 📖	mathematical	`Set.PartiallyWellOrderedOn`	`Set` `Set.instUnion`	—	`Nat.exists_subseq_of_forall_mem_union` `exists_lt` `OrderEmbedding.strictMono`
`wellFoundedOn` 📖	mathematical	`Set.PartiallyWellOrderedOn`	`Set.WellFoundedOn`	—	`WellQuasiOrdered.wellFounded` `Subrel.instIsPreorderSubtype`

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPWO` 📖	mathematical	`Set.Subsingleton`	`Set.IsPWO`	—	`Set.Finite.isPWO` `finite`
`isWF` 📖	mathematical	`Set.Subsingleton`	`Set.IsWF` `Preorder.toLT`	—	`Set.IsPWO.isWF` `isPWO`
`partiallyWellOrderedOn` 📖	mathematical	`Set.Subsingleton`	`Set.PartiallyWellOrderedOn`	—	`Set.Finite.partiallyWellOrderedOn` `finite`
`wellFoundedOn` 📖	mathematical	`Set.Subsingleton`	`Set.WellFoundedOn`	—	`Set.Finite.wellFoundedOn` `finite`

Set.WellFoundedOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`acc_iff_wellFoundedOn` 📖	mathematical	—	`List.TFAE` `Set.WellFoundedOn` `setOf` `Relation.ReflTransGen`	—	`Relation.reflTransGen_iff_eq_or_transGen` `subset` `Relation.TransGen.to_reflTransGen` `Acc.of_fibration` `Relation.TransGen.head` `List.tfae_of_cycle`
`induction` 📖	—	`Set.WellFoundedOn` `Set` `Set.instMembership`	—	—	—
`insert` 📖	mathematical	`Set.WellFoundedOn`	`Set` `Set.instInsert`	—	`Set.wellFoundedOn_insert`
`mapsTo` 📖	mathematical	`Set.MapsTo` `Set.WellFoundedOn`	`Function.onFun`	—	`Subtype.prop`
`mono` 📖	—	`Set.WellFoundedOn` `Pi.hasLe` `Prop.le` `Set` `Set.instHasSubset`	—	—	`Set.wellFoundedOn_iff`
`mono'` 📖	—	`Set.WellFoundedOn`	—	—	—
`prod_lex_of_wellFoundedOn_fiber` 📖	—	`Set.WellFoundedOn` `Function.onFun` `Set` `Set.instInter` `Set.preimage` `Set.instSingletonSet`	—	—	`WellFounded.prod_lex_of_wellFoundedOn_fiber` `WellFounded.mono` `WellFounded.onFun`
`sdiff_singleton` 📖	mathematical	`Set.WellFoundedOn`	`Set` `Set.instSDiff` `Set.instSingletonSet`	—	`Set.wellFoundedOn_sdiff_singleton`
`sigma_lex_of_wellFoundedOn_fiber` 📖	mathematical	`Set.WellFoundedOn` `Function.onFun` `Set` `Set.instInter` `Set.preimage` `Set.instSingletonSet`	`Sigma.Lex`	—	`WellFounded.sigma_lex_of_wellFoundedOn_fiber` `WellFounded.mono` `WellFounded.onFun`
`subset` 📖	—	`Set.WellFoundedOn` `Set` `Set.instHasSubset`	—	—	`mono` `le_rfl`
`union` 📖	mathematical	`Set.WellFoundedOn`	`Set` `Set.instUnion`	—	`Set.wellFoundedOn_iff_no_descending_seq` `Nat.exists_subseq_of_forall_mem_union`

WellFounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_lex_of_wellFoundedOn_fiber` 📖	—	`Function.onFun` `Set.WellFoundedOn` `Set.preimage` `Set` `Set.instSingletonSet`	—	—	`mono` `onFun` `psigma_lex` `Set.wellFoundedOn_range` `Prod.lex_iff` `PSigma.subtype_ext`
`sigma_lex_of_wellFoundedOn_fiber` 📖	mathematical	`Function.onFun` `Set.WellFoundedOn` `Set.preimage` `Set` `Set.instSingletonSet`	`Sigma.Lex`	—	`mono` `onFun` `psigma_lex` `Set.wellFoundedOn_range` `Sigma.lex_iff` `PSigma.subtype_ext`
`wellFoundedOn` 📖	mathematical	—	`Set.WellFoundedOn`	—	—

---

← Back to Index