RelClasses

📁 Source: Mathlib/Order/RelClasses.lean

Statistics

Metric	Count
Definitions `exactSubsetOfSSubset`, `IsNonstrictStrictOrder`, `IsOrderConnected`, `IsWellFounded`, `fix`, `toWellFoundedRelation`, `IsWellOrder`, `linearOrder`, `toHasWellFounded`, `Unbounded`, `WellFoundedGT`, `fix`, `toWellFoundedRelation`, `WellFoundedLT`, `fix`, `toWellFoundedRelation`, `linearOrderOfSTO`, `partialOrderOfSO`	18
Theorems `subset`, `subset'`, `superset`, `trans_ssubset`, `trans_subset`, `ssubset_imp_ssubset`, `ssuperset_imp_ssuperset`, `asymm`, `false`, `ne`, `ne'`, `not_subset`, `subset`, `trans`, `trans_eq`, `trans_subset`, `antisymm`, `antisymm'`, `eq_of_not_ssubset`, `eq_of_not_ssuperset`, `eq_or_ssubset`, `not_ssubset`, `ssubset_of_ne`, `ssubset_of_not_subset`, `ssubset_or_eq`, `trans`, `trans_ssubset`, `trans_eq`, `asymm`, `isTrichotomous`, `trichotomous`, `swap`, `right_iff_left_not_left`, `conn`, `neg_trans`, `swap`, `swap`, `swap`, `swap`, `swap`, `swap`, `swap`, `apply`, `fix_eq`, `induction`, `wf`, `toIsTrans`, `toIsWellFounded`, `toTrichotomous`, `total`, `total'`, `ssubset_of_subset`, `antisymm`, `instAsymm`, `instIrrefl`, `instIsEquiv`, `instIsPreorder`, `instIsStrictOrder`, `instIsStrictWeakOrder`, `instIsSymm`, `instIsTrans`, `instRefl`, `instTotal`, `isAntisymm`, `total_ge`, `total_le`, `instIsWellFounded`, `wellFoundedGT`, `wellFoundedGT'`, `wellFoundedLT`, `wellFoundedLT'`, `not_bounded_iff`, `not_unbounded_iff`, `unbounded_of_isEmpty`, `swap`, `swap`, `swap`, `swap`, `swap`, `swap`, `isWellFounded`, `isWellOrder`, `asymmetric`, `asymmetric₃`, `prod_lex`, `psigma_lex`, `psigma_revLex`, `psigma_skipLeft`, `apply`, `fix_eq`, `induction`, `apply`, `fix_eq`, `induction`, `asymmetric`, `asymmetric₃`, `isWellFounded`, `eq_empty_relation`, `eq_of_subset_of_not_ssubset`, `eq_of_superset_of_not_ssuperset`, `eq_or_ssubset_of_subset`, `instAntisymmGe`, `instAntisymmGt`, `instAntisymmLe`, `instAntisymmLt`, `instAsymmGt`, `instAsymmLt`, `instAsymmOfIsWellFounded`, `instIrreflGt`, `instIrreflLt`, `instIrreflOfIsNonstrictStrictOrder`, `instIsLinearOrderGe`, `instIsLinearOrderLe`, `instIsNonstrictStrictOrderGeGt`, `instIsNonstrictStrictOrderLeLt`, `instIsPartialOrderGe`, `instIsPartialOrderLe`, `instIsPreorderGe`, `instIsPreorderLe`, `instIsStrictOrderGt`, `instIsStrictOrderLt`, `instIsStrictTotalOrderGt`, `instIsStrictTotalOrderLt`, `instIsStrictTotalOrderOfIsWellOrder`, `instIsTransGe`, `instIsTransGt`, `instIsTransLe`, `instIsTransLt`, `instIsWellFoundedInvImage`, `instIsWellFoundedInvImageNatLt`, `instIsWellFoundedTransGen`, `instIsWellOrderEmptyRelationOfSubsingleton`, `instIsWellOrderOfIsEmpty`, `instIsWellOrderProdLex`, `instReflGe`, `instReflLe`, `instTrichotomousGe`, `instTrichotomousGt`, `instTrichotomousLe`, `instTrichotomousLt`, `instWellFoundedGTOrderDualOfWellFoundedLT`, `instWellFoundedLTNat`, `instWellFoundedLTOrderDualOfWellFoundedGT`, `isStrictOrderConnected_of_isStrictTotalOrder`, `isStrictWeakOrder_of_isOrderConnected`, `isWellFounded_iff`, `isWellOrder_gt`, `isWellOrder_lt`, `ne_of_not_subset`, `ne_of_not_superset`, `ne_of_ssubset`, `ne_of_ssuperset`, `not_ssubset_of_subset`, `not_subset_of_ssubset`, `right_iff_left_not_left`, `right_iff_left_not_left_of`, `ssubset_asymm`, `ssubset_iff_subset_ne`, `ssubset_iff_subset_not_subset`, `ssubset_irrefl`, `ssubset_irrfl`, `ssubset_of_eq_of_ssubset`, `ssubset_of_ne_of_subset`, `ssubset_of_ssubset_of_eq`, `ssubset_of_ssubset_of_subset`, `ssubset_of_subset_not_subset`, `ssubset_of_subset_of_ne`, `ssubset_of_subset_of_ssubset`, `ssubset_or_eq_of_subset`, `ssubset_trans`, `subset_antisymm`, `subset_antisymm_iff`, `subset_iff_ssubset_or_eq`, `subset_of_eq`, `subset_of_eq_of_subset`, `subset_of_ssubset`, `subset_of_subset_of_eq`, `subset_refl`, `subset_rfl`, `subset_trans`, `superset_antisymm`, `superset_antisymm_iff`, `superset_of_eq`, `transitive_ge`, `transitive_gt`, `transitive_le`, `transitive_lt`, `wellFoundedGT_dual_iff`, `wellFoundedLT_dual_iff`, `wellFounded_gt`, `wellFounded_lt`	191
Total	209

Eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subset` 📖	—	—	—	—	`subset_of_eq`
`subset'` 📖	—	—	—	—	`subset`
`superset` 📖	—	—	—	—	`superset_of_eq`
`trans_ssubset` 📖	—	—	—	—	`ssubset_of_eq_of_ssubset`
`trans_subset` 📖	—	—	—	—	`subset_of_eq_of_subset`

GCongr

Definitions

Name	Category	Theorems
`exactSubsetOfSSubset` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ssubset_imp_ssubset` 📖	—	—	—	—	`HasSSubset.SSubset.trans_subset` `HasSubset.Subset.trans_ssubset`
`ssuperset_imp_ssuperset` 📖	—	—	—	—	`ssubset_imp_ssubset`

HasSSubset.SSubset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`asymm` 📖	—	—	—	—	`ssubset_asymm`
`false` 📖	—	—	—	—	`ssubset_irrfl`
`ne` 📖	—	—	—	—	`ne_of_ssubset`
`ne'` 📖	—	—	—	—	`ne_of_ssuperset`
`not_subset` 📖	—	—	—	—	`not_subset_of_ssubset`
`subset` 📖	—	—	—	—	`subset_of_ssubset`
`trans` 📖	—	—	—	—	`ssubset_trans`
`trans_eq` 📖	—	—	—	—	`ssubset_of_ssubset_of_eq`
`trans_subset` 📖	—	—	—	—	`ssubset_of_ssubset_of_subset`

HasSubset.Subset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antisymm` 📖	—	—	—	—	`subset_antisymm`
`antisymm'` 📖	—	—	—	—	`superset_antisymm`
`eq_of_not_ssubset` 📖	—	—	—	—	`eq_of_subset_of_not_ssubset`
`eq_of_not_ssuperset` 📖	—	—	—	—	`eq_of_superset_of_not_ssuperset`
`eq_or_ssubset` 📖	—	—	—	—	`eq_or_ssubset_of_subset`
`not_ssubset` 📖	—	—	—	—	`not_ssubset_of_subset`
`ssubset_of_ne` 📖	—	—	—	—	`ssubset_of_subset_of_ne`
`ssubset_of_not_subset` 📖	—	—	—	—	`ssubset_of_subset_not_subset`
`ssubset_or_eq` 📖	—	—	—	—	`ssubset_or_eq_of_subset`
`trans` 📖	—	—	—	—	`subset_trans`
`trans_ssubset` 📖	—	—	—	—	`ssubset_of_subset_of_ssubset`

HasSubset.subset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trans_eq` 📖	—	—	—	—	`subset_of_subset_of_eq`

InvImage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`asymm` 📖	—	—	—	—	—
`isTrichotomous` 📖	—	—	—	—	`trichotomous`
`trichotomous` 📖	—	—	—	—	—

IsAsymm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`swap` 📖	mathematical	—	`Function.swap`	—	`Std.Asymm.swap`

IsNonstrictStrictOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`right_iff_left_not_left` 📖	—	—	—	—	—

IsOrderConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conn` 📖	—	—	—	—	—
`neg_trans` 📖	—	—	—	—	`conn`

IsPartialOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`swap` 📖	mathematical	—	`IsPartialOrder` `Function.swap`	—	`IsPreorder.swap` `toIsPreorder` `Std.Antisymm.swap` `toAntisymm`

IsPreorder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`swap` 📖	mathematical	—	`IsPreorder` `Function.swap`	—	`Std.Refl.swap` `toRefl` `IsTrans.swap` `toIsTrans`

IsRefl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`swap` 📖	mathematical	—	`Function.swap`	—	`Std.Refl.swap`

IsStrictOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`swap` 📖	mathematical	—	`IsStrictOrder` `Function.swap`	—	`Std.Irrefl.swap` `toIrrefl` `IsTrans.swap` `toIsTrans`

IsStrictTotalOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`swap` 📖	mathematical	—	`IsStrictTotalOrder` `Function.swap`	—	`Std.Trichotomous.swap` `toTrichotomous` `IsStrictOrder.swap` `toIsStrictOrder`

IsTrans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`swap` 📖	mathematical	—	`IsTrans` `Function.swap`	—	`trans_of`

IsTrichotomous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`swap` 📖	mathematical	—	`Function.swap`	—	`Std.Trichotomous.swap`

IsWellFounded

Definitions

Name	Category	Theorems
`fix` 📖	CompOp	1 math math: `fix_eq`
`toWellFoundedRelation` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply` 📖	—	—	—	—	`wf`
`fix_eq` 📖	mathematical	—	`fix`	—	`wf`
`induction` 📖	—	—	—	—	`wf`
`wf` 📖	—	—	—	—	—

IsWellOrder

Definitions

Name	Category	Theorems
`linearOrder` 📖	CompOp	—
`toHasWellFounded` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toIsTrans` 📖	mathematical	—	`IsTrans`	—	—
`toIsWellFounded` 📖	mathematical	—	`IsWellFounded`	—	—
`toTrichotomous` 📖	—	—	—	—	—

LE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`total` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`le_total`
`total'` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`le_total`

Ne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ssubset_of_subset` 📖	—	—	—	—	`ssubset_of_ne_of_subset`

Order.Preimage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antisymm` 📖	mathematical	—	`Order.Preimage`	—	`antisymm_of`
`instAsymm` 📖	mathematical	—	`Order.Preimage`	—	`asymm_of`
`instIrrefl` 📖	mathematical	—	`Order.Preimage`	—	`irrefl_of`
`instIsEquiv` 📖	mathematical	—	`IsEquiv` `Order.Preimage`	—	`instIsPreorder` `IsEquiv.toIsPreorder` `instIsSymm` `IsEquiv.toSymm`
`instIsPreorder` 📖	mathematical	—	`IsPreorder` `Order.Preimage`	—	`instRefl` `IsPreorder.toRefl` `instIsTrans` `IsPreorder.toIsTrans`
`instIsStrictOrder` 📖	mathematical	—	`IsStrictOrder` `Order.Preimage`	—	`instIrrefl` `IsStrictOrder.toIrrefl` `instIsTrans` `IsStrictOrder.toIsTrans`
`instIsStrictWeakOrder` 📖	mathematical	—	`IsStrictWeakOrder` `Order.Preimage`	—	`instIsStrictOrder` `IsStrictWeakOrder.toIsStrictOrder` `IsStrictWeakOrder.incomp_trans`
`instIsSymm` 📖	mathematical	—	`Order.Preimage`	—	`symm_of`
`instIsTrans` 📖	mathematical	—	`IsTrans` `Order.Preimage`	—	`trans_of`
`instRefl` 📖	mathematical	—	`Order.Preimage`	—	`refl_of`
`instTotal` 📖	mathematical	—	`Order.Preimage`	—	`total_of`
`isAntisymm` 📖	mathematical	—	`Order.Preimage`	—	`antisymm`

OrderDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`total_ge` 📖	mathematical	—	`OrderDual` `instLE`	—	`Std.Total.swap`
`total_le` 📖	mathematical	—	`OrderDual` `instLE`	—	`Std.Total.swap`

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`wellFoundedGT` 📖	mathematical	—	`WellFoundedGT` `Preorder.toLT` `instPreorder`	—	`WellFoundedGT.induction` `lt_iff` `LT.lt.trans_le'` `le_rfl` `LE.le.trans'`
`wellFoundedGT'` 📖	mathematical	—	`WellFoundedGT` `Preorder.toLT` `instPreorder`	—	`wellFoundedGT`
`wellFoundedLT` 📖	mathematical	—	`WellFoundedLT` `Preorder.toLT` `instPreorder`	—	`WellFoundedLT.induction` `lt_iff` `LT.lt.trans_le` `le_rfl` `LE.le.trans`
`wellFoundedLT'` 📖	mathematical	—	`WellFoundedLT` `Preorder.toLT` `instPreorder`	—	`wellFoundedLT`

Prod.Lex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsWellFounded` 📖	mathematical	—	`IsWellFounded`	—	`WellFounded.prod_lex` `IsWellFounded.wf`

Set

Definitions

Name	Category	Theorems
`Unbounded` 📖	MathDef	37 math math: `unbounded_ge_univ`, `unbounded_lt_iff_unbounded_le`, `unbounded_gt_univ`, `unbounded_gt_inter_gt`, `unbounded_le_inter_not_le`, `unbounded_le_inter_le`, `unbounded_lt_inter_le`, `unbounded_inter_not`, `unbounded_inter_ge`, `not_bounded_iff`, `unbounded_gt_inter_not_gt`, `Ordinal.unbounded_range_of_le_iSup`, `unbounded_le_Ioi`, `unbounded_ge_iff_unbounded_inter_ge`, `unbounded_of_isEmpty`, `unbounded_lt_iff`, `not_unbounded_iff`, `unbounded_gt_iff`, `unbounded_le_iff`, `Ordinal.ord_cof_eq`, `unbounded_ge_inter_gt`, `unbounded_ge_inter_not_ge`, `unbounded_gt_of_forall_exists_ge`, `unbounded_lt_inter_not_lt`, `unbounded_lt_univ`, `unbounded_le_of_forall_exists_lt`, `unbounded_le_inter_lt`, `unbounded_lt_Ici`, `unbounded_le_univ`, `unbounded_lt_of_forall_exists_le`, `Ordinal.cof_eq`, `unbounded_ge_of_forall_exists_gt`, `unbounded_ge_iff`, `unbounded_le_Ici`, `unbounded_gt_iff_unbounded_ge`, `unbounded_lt_inter_lt`, `unbounded_lt_Ioi`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_bounded_iff` 📖	mathematical	—	`Bounded` `Unbounded`	—	—
`not_unbounded_iff` 📖	mathematical	—	`Unbounded` `Bounded`	—	`not_iff_comm` `not_bounded_iff`
`unbounded_of_isEmpty` 📖	mathematical	—	`Unbounded`	—	—

Std.Antisymm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`swap` 📖	mathematical	—	`Function.swap`	—	`antisymm`

Std.Asymm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`swap` 📖	mathematical	—	`Function.swap`	—	`asymm_of`

Std.Irrefl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`swap` 📖	mathematical	—	`Function.swap`	—	`irrefl_of`

Std.Refl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`swap` 📖	mathematical	—	`Function.swap`	—	`refl_of`

Std.Total

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`swap` 📖	mathematical	—	`Function.swap`	—	`total_of`

Std.Trichotomous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`swap` 📖	mathematical	—	`Function.swap`	—	—

Subrelation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isWellFounded` 📖	mathematical	—	`IsWellFounded`	—	`IsWellFounded.wf`

Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isWellOrder` 📖	mathematical	—	`IsWellOrder`	—	`not_rel_of_subsingleton`

WellFounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`asymmetric` 📖	—	—	—	—	`WellFoundedRelation.asymmetric`
`asymmetric₃` 📖	—	—	—	—	`WellFoundedRelation.asymmetric₃`
`prod_lex` 📖	—	—	—	—	—
`psigma_lex` 📖	—	—	—	—	—
`psigma_revLex` 📖	—	—	—	—	—
`psigma_skipLeft` 📖	—	—	—	—	`psigma_revLex`

WellFoundedGT

Definitions

Name	Category	Theorems
`fix` 📖	CompOp	1 math math: `fix_eq`
`toWellFoundedRelation` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply` 📖	—	—	—	—	`IsWellFounded.apply`
`fix_eq` 📖	mathematical	—	`fix`	—	`IsWellFounded.fix_eq`
`induction` 📖	—	—	—	—	`IsWellFounded.induction`

WellFoundedLT

Definitions

Name	Category	Theorems
`fix` 📖	CompOp	1 math math: `fix_eq`
`toWellFoundedRelation` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply` 📖	—	—	—	—	`IsWellFounded.apply`
`fix_eq` 📖	mathematical	—	`fix`	—	`IsWellFounded.fix_eq`
`induction` 📖	—	—	—	—	`IsWellFounded.induction`

WellFoundedRelation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`asymmetric` 📖	—	—	—	—	—
`asymmetric₃` 📖	—	—	—	—	—
`isWellFounded` 📖	mathematical	—	`IsWellFounded`	—	—

(root)

Definitions

Name	Category	Theorems
`IsNonstrictStrictOrder` 📖	CompData	8 math math: `PSet.instIsNonstrictStrictOrderSubsetSSubset`, `instIsNonstrictStrictOrderGeGt`, `ZFSet.instIsNonstrictStrictOrderSubsetSSubset`, `Finset.instIsNonstrictStrictOrderSubsetSSubset`, `Set.instIsNonstrictStrictOrderSubsetSSubset`, `Multiset.instIsNonstrictStrictOrder`, `instIsNonstrictStrictOrderLeLt`, `instIsNonstrictStrictOrderWCovByCovBy`
`IsOrderConnected` 📖	CompData	2 math math: `isStrictOrderConnected_of_isStrictTotalOrder`, `List.Lex.isOrderConnected`
`IsWellFounded` 📖	CompData	22 math math: `instIsWellFoundedInvImage`, `PSet.instIsWellFoundedMem`, `IsWellFounded.wellOrderExtension.isWellFounded_lt`, `instIsWellFoundedInvImageNatLt`, `Multiset.isWellFounded_ssubset`, `Prod.Lex.instIsWellFounded`, `Finset.isWellFounded_ssubset`, `EuclideanDomain.isWellFounded`, `isWellFounded_iff`, `ZFSet.instIsWellFoundedMem`, `Subrel.instIsWellFoundedSubtype`, `IsWellOrder.toIsWellFounded`, `WellFoundedRelation.isWellFounded`, `instIsWellFoundedTransGen`, `RelEmbedding.isWellFounded`, `RelHomClass.isWellFounded`, `SSet.Subcomplex.Pairing.instIsWellFoundedElemNIIAncestralRel`, `UniqueFactorizationMonoid.toIsWellFounded`, `Class.instIsWellFoundedMem`, `Relation.instIsWellFoundedMultisetCutExpand`, `Subrelation.isWellFounded`, `instIsWellFoundedChainsLex_chains`
`IsWellOrder` 📖	CompData	37 math math: `OrderEmbedding.isWellOrder`, `RelEmbedding.isWellOrder`, `Ordinal.liftOnWellOrder_type`, `WithTop.IsWellOrder.gt`, `Ordinal.liftPrincipalSeg_top'`, `isWellOrder_lt`, `WithTop.IsWellOrder.lt`, `isWellOrder_gt`, `WithBot.IsWellOrder.lt`, `instIsWellOrderEmptyRelationOfSubsingleton`, `Fin.Lt.isWellOrder`, `InitialSeg.exists_sum_relIso`, `Subsingleton.isWellOrder`, `Cardinal.ord_eq_Inf`, `Ordinal.le_enum_succ`, `Subrel.instIsWellOrderSubtype`, `RelIso.IsWellOrder.preimage`, `WellOrderingRel.isWellOrder`, `Sum.instIsWellOrderLex`, `ZFSet.IsOrdinal.isWellOrder`, `Cardinal.type_cardinal`, `Ordinal.enum_succ_eq_top`, `instIsWellOrderProdLex`, `IsWellFounded.exists_well_order_ge`, `Ordinal.univ_id`, `Ordinal.type_nat_lt`, `ZFSet.isOrdinal_iff_isWellOrder`, `RelIso.IsWellOrder.ulift`, `Ordinal.enum_zero_le'`, `IsWellFounded.wellOrderExtension.isWellOrder_lt`, `Ordinal.familyOfBFamily_enum`, `instIsWellOrderOfIsEmpty`, `Ordinal.type_toType`, `IsWellOrder.subtype_nonempty`, `WithBot.IsWellOrder.gt`, `Ordinal.type_fin`, `WellOrder.wo`
`WellFoundedGT` 📖	MathDef	40 math math: `isNoetherian_iff'`, `WithTop.instWellFoundedGT`, `wellFoundedLT_dual_iff`, `CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact`, `StrictMono.wellFoundedGT`, `CategoryTheory.instWellFoundedGTSubobjectOfIsNoetherianObject`, `SemigroupIdeal.instWellFoundedGT`, `Prod.wellFoundedGT'`, `instWellFoundedGTAntisymmetrizationLe`, `isNoetherian_iff_fg_wellFounded`, `instWellFoundedGTTrivial`, `instWellFoundedGTOfGradeOrderOrderDualNat`, `CompleteLattice.isSupClosedCompact_iff_wellFoundedGT`, `IsNoetherian.wellFoundedGT`, `AddSemigroupIdeal.instWellFoundedGT`, `instWellFoundedGTOrderDualOfWellFoundedLT`, `CompleteLattice.IsSupClosedCompact.wellFoundedGT`, `Bool.instWellFoundedGT`, `wellFoundedGT_antisymmetrization_iff`, `Prod.wellFoundedGT`, `wellFoundedGT_iff_monotone_chain_condition`, `ULift.instWellFoundedGT`, `wellFoundedGT_dual_iff`, `LieSubmodule.wellFoundedGT_of_noetherian`, `StrictAnti.wellFoundedGT`, `CompleteLattice.IsSupFiniteCompact.wellFoundedGT`, `OrderEmbedding.wellFoundedGT`, `CompleteLattice.wellFoundedGT_characterisations`, `WithBot.instWellFoundedGT`, `instWellFoundedGTUnit`, `wellFoundedGT`, `Finite.to_wellFoundedGT`, `wellFounded_gt_exact_sequence`, `wellFoundedGT_iff_monotone_chain_condition'`, `LieSubalgebra.wellFoundedGT_of_noetherian`, `Subtype.wellFoundedGT`, `instWellFoundedGTShrink`, `GradeOrder.wellFoundedGT`, `Prop.instWellFoundedGT`, `instWellFoundedGTWithZeroMultiplicativeIntLeOne`
`WellFoundedLT` 📖	MathDef	58 math math: `WellOrderExtension.wellFoundedLT`, `wellFoundedLT_dual_iff`, `Bool.instWellFoundedLT`, `GradeOrder.wellFoundedLT`, `instWellFoundedLTSubtypeSetFinite`, `Subtype.wellFoundedLT`, `PartENat.instWellFoundedLT`, `Finsupp.Colex.wellFoundedLT`, `exists_wellOrder`, `Function.Lex.wellFoundedLT`, `Prod.wellFoundedLT`, `Finsupp.Colex.wellFoundedLT_of_finite`, `wellQuasiOrderedLE_iff_wellFoundedLT`, `StrictAnti.wellFoundedLT`, `Ordinal.wellFoundedLT`, `ULift.instWellFoundedLT`, `instWellFoundedLTAntisymmetrizationLe`, `Finsupp.wellFoundedLT'`, `WithBot.instWellFoundedLT`, `wellFoundedLT_antisymmetrization_iff`, `Nimber.instWellFoundedLT`, `Multiset.instWellFoundedLT`, `instWellFoundedLTShrink`, `Function.wellFoundedLT`, `Cardinal.instWellFoundedLT`, `instWellFoundedLTOrderDualOfWellFoundedGT`, `TopologicalSpace.noetherianSpace_TFAE`, `Finset.wellFoundedLT`, `Prop.instWellFoundedLT`, `MonomialOrder.wf`, `LieSubmodule.wellFoundedLT_of_isArtinian`, `instWellFoundedLTNat`, `wellFoundedGT_dual_iff`, `Finite.to_wellFoundedLT`, `OrderEmbedding.wellFoundedLT`, `PNat.instWellFoundedLT`, `TopologicalSpace.instWellFoundedLTClosedsOfNoetherianSpace`, `Finsupp.wellFoundedLT`, `Set.isWF_univ_iff`, `WithTop.instWellFoundedLT`, `CategoryTheory.instWellFoundedLTSubobjectOfIsArtinianObject`, `WfDvdMonoid.iff_wellFounded_associates`, `NatOrdinal.instWellFoundedLT`, `Prod.Lex.instWellFoundedLTLex`, `StrictMono.wellFoundedLT`, `Finsupp.DegLex.wellFoundedLT`, `Finsupp.Lex.wellFoundedLT`, `wellQuasiOrderedLE_iff`, `instWellFoundedLTOfGradeOrderNat`, `WfDvdMonoid.wellFoundedLT_associates`, `WellQuasiOrderedLE.to_wellFoundedLT`, `Finsupp.wellFoundedLT_of_finite`, `Prod.wellFoundedLT'`, `Profinite.NobelingProof.Products.instWellFoundedLT`, `wellFoundedLT_toType`, `Finsupp.Lex.wellFoundedLT_of_finite`, `wellFounded_lt_exact_sequence`, `NONote.instWellFoundedLT`
`linearOrderOfSTO` 📖	CompOp	—
`partialOrderOfSO` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_empty_relation` 📖	—	—	—	—	`not_rel_of_subsingleton`
`eq_of_subset_of_not_ssubset` 📖	—	—	—	—	`eq_or_ssubset_of_subset`
`eq_of_superset_of_not_ssuperset` 📖	—	—	—	—	`eq_or_ssubset_of_subset`
`eq_or_ssubset_of_subset` 📖	—	—	—	—	`HasSubset.Subset.antisymm` `HasSubset.Subset.ssubset_of_not_subset` `em`
`instAntisymmGe` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder`	—	`ge_antisymm`
`instAntisymmGt` 📖	mathematical	—	`Preorder.toLT`	—	`Std.Asymm.antisymm` `instAsymmGt`
`instAntisymmLe` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder`	—	`le_antisymm`
`instAntisymmLt` 📖	mathematical	—	`Preorder.toLT`	—	`Std.Asymm.antisymm` `instAsymmLt`
`instAsymmGt` 📖	mathematical	—	`Preorder.toLT`	—	`lt_asymm`
`instAsymmLt` 📖	mathematical	—	`Preorder.toLT`	—	`lt_asymm`
`instAsymmOfIsWellFounded` 📖	—	—	—	—	`WellFounded.asymmetric` `IsWellFounded.wf`
`instIrreflGt` 📖	mathematical	—	`Preorder.toLT`	—	`lt_irrefl`
`instIrreflLt` 📖	mathematical	—	`Preorder.toLT`	—	`lt_irrefl`
`instIrreflOfIsNonstrictStrictOrder` 📖	—	—	—	—	`right_iff_left_not_left_of`
`instIsLinearOrderGe` 📖	mathematical	—	`IsLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`instIsPartialOrderGe` `LE.total'`
`instIsLinearOrderLe` 📖	mathematical	—	`IsLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`instIsPartialOrderLe` `LE.total`
`instIsNonstrictStrictOrderGeGt` 📖	mathematical	—	`IsNonstrictStrictOrder` `Preorder.toLE` `Preorder.toLT`	—	`lt_iff_le_not_ge`
`instIsNonstrictStrictOrderLeLt` 📖	mathematical	—	`IsNonstrictStrictOrder` `Preorder.toLE` `Preorder.toLT`	—	`lt_iff_le_not_ge`
`instIsPartialOrderGe` 📖	mathematical	—	`IsPartialOrder` `Preorder.toLE` `PartialOrder.toPreorder`	—	`instIsPreorderGe` `instAntisymmGe`
`instIsPartialOrderLe` 📖	mathematical	—	`IsPartialOrder` `Preorder.toLE` `PartialOrder.toPreorder`	—	`instIsPreorderLe` `instAntisymmLe`
`instIsPreorderGe` 📖	mathematical	—	`IsPreorder` `Preorder.toLE`	—	`instReflGe` `instIsTransGe`
`instIsPreorderLe` 📖	mathematical	—	`IsPreorder` `Preorder.toLE`	—	`instReflLe` `instIsTransLe`
`instIsStrictOrderGt` 📖	mathematical	—	`IsStrictOrder` `Preorder.toLT`	—	`instIrreflGt` `instIsTransGt`
`instIsStrictOrderLt` 📖	mathematical	—	`IsStrictOrder` `Preorder.toLT`	—	`instIrreflLt` `instIsTransLt`
`instIsStrictTotalOrderGt` 📖	mathematical	—	`IsStrictTotalOrder` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`instTrichotomousGt` `instIsStrictOrderGt`
`instIsStrictTotalOrderLt` 📖	mathematical	—	`IsStrictTotalOrder` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`instTrichotomousLt` `instIsStrictOrderLt`
`instIsStrictTotalOrderOfIsWellOrder` 📖	mathematical	—	`IsStrictTotalOrder`	—	`IsWellOrder.toTrichotomous` `instAsymmOfIsWellFounded` `IsWellOrder.toIsWellFounded` `IsWellOrder.toIsTrans`
`instIsTransGe` 📖	mathematical	—	`IsTrans` `Preorder.toLE`	—	`ge_trans`
`instIsTransGt` 📖	mathematical	—	`IsTrans` `Preorder.toLT`	—	`gt_trans`
`instIsTransLe` 📖	mathematical	—	`IsTrans` `Preorder.toLE`	—	`le_trans`
`instIsTransLt` 📖	mathematical	—	`IsTrans` `Preorder.toLT`	—	`lt_trans`
`instIsWellFoundedInvImage` 📖	mathematical	—	`IsWellFounded`	—	`IsWellFounded.wf`
`instIsWellFoundedInvImageNatLt` 📖	mathematical	—	`IsWellFounded`	—	—
`instIsWellFoundedTransGen` 📖	mathematical	—	`IsWellFounded`	—	`IsWellFounded.wf`
`instIsWellOrderEmptyRelationOfSubsingleton` 📖	mathematical	—	`IsWellOrder`	—	`Subsingleton.isWellOrder` `instIrreflEmptyRelation_mathlib`
`instIsWellOrderOfIsEmpty` 📖	mathematical	—	`IsWellOrder`	—	`wellFounded_of_isEmpty`
`instIsWellOrderProdLex` 📖	mathematical	—	`IsWellOrder`	—	`IsWellOrder.toTrichotomous` `trans` `IsWellOrder.toIsTrans` `Prod.Lex.instIsWellFounded` `IsWellOrder.toIsWellFounded`
`instReflGe` 📖	mathematical	—	`Preorder.toLE`	—	`le_refl`
`instReflLe` 📖	mathematical	—	`Preorder.toLE`	—	`le_refl`
`instTrichotomousGe` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`LE.total'`
`instTrichotomousGt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	—
`instTrichotomousLe` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`LE.total`
`instTrichotomousLt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	—
`instWellFoundedGTOrderDualOfWellFoundedLT` 📖	mathematical	—	`WellFoundedGT` `OrderDual` `OrderDual.instLT`	—	—
`instWellFoundedLTNat` 📖	mathematical	—	`WellFoundedLT`	—	—
`instWellFoundedLTOrderDualOfWellFoundedGT` 📖	mathematical	—	`WellFoundedLT` `OrderDual` `OrderDual.instLT`	—	—
`isStrictOrderConnected_of_isStrictTotalOrder` 📖	mathematical	—	`IsOrderConnected`	—	`trans` `IsStrictOrder.toIsTrans` `IsStrictTotalOrder.toIsStrictOrder` `trichotomous` `IsStrictTotalOrder.toTrichotomous`
`isStrictWeakOrder_of_isOrderConnected` 📖	mathematical	—	`IsStrictWeakOrder`	—	`Std.Asymm.irrefl` `IsOrderConnected.conn` `asymm` `IsOrderConnected.neg_trans`
`isWellFounded_iff` 📖	mathematical	—	`IsWellFounded`	—	—
`isWellOrder_gt` 📖	mathematical	—	`IsWellOrder` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`instTrichotomousGt` `instIsTransGt`
`isWellOrder_lt` 📖	mathematical	—	`IsWellOrder` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`instTrichotomousLt` `instIsTransLt`
`ne_of_not_subset` 📖	—	—	—	—	`subset_of_eq`
`ne_of_not_superset` 📖	—	—	—	—	`superset_of_eq`
`ne_of_ssubset` 📖	—	—	—	—	`ne_of_irrefl`
`ne_of_ssuperset` 📖	—	—	—	—	`ne_of_irrefl'`
`not_ssubset_of_subset` 📖	—	—	—	—	`not_subset_of_ssubset`
`not_subset_of_ssubset` 📖	—	—	—	—	`ssubset_iff_subset_not_subset`
`right_iff_left_not_left` 📖	—	—	—	—	`IsNonstrictStrictOrder.right_iff_left_not_left`
`right_iff_left_not_left_of` 📖	—	—	—	—	`right_iff_left_not_left`
`ssubset_asymm` 📖	—	—	—	—	`asymm`
`ssubset_iff_subset_ne` 📖	—	—	—	—	`HasSSubset.SSubset.subset` `HasSSubset.SSubset.ne` `instIrreflOfIsNonstrictStrictOrder` `HasSubset.Subset.ssubset_of_ne`
`ssubset_iff_subset_not_subset` 📖	—	—	—	—	`right_iff_left_not_left`
`ssubset_irrefl` 📖	—	—	—	—	`irrefl`
`ssubset_irrfl` 📖	—	—	—	—	`irrefl`
`ssubset_of_eq_of_ssubset` 📖	—	—	—	—	—
`ssubset_of_ne_of_subset` 📖	—	—	—	—	`ssubset_of_subset_of_ne`
`ssubset_of_ssubset_of_eq` 📖	—	—	—	—	—
`ssubset_of_ssubset_of_subset` 📖	—	—	—	—	`HasSubset.Subset.ssubset_of_not_subset` `HasSubset.Subset.trans` `HasSSubset.SSubset.subset` `HasSSubset.SSubset.not_subset`
`ssubset_of_subset_not_subset` 📖	—	—	—	—	`ssubset_iff_subset_not_subset`
`ssubset_of_subset_of_ne` 📖	—	—	—	—	`HasSubset.Subset.ssubset_of_not_subset` `HasSubset.Subset.antisymm`
`ssubset_of_subset_of_ssubset` 📖	—	—	—	—	`HasSubset.Subset.ssubset_of_not_subset` `HasSubset.Subset.trans` `HasSSubset.SSubset.subset` `HasSSubset.SSubset.not_subset`
`ssubset_or_eq_of_subset` 📖	—	—	—	—	`eq_or_ssubset_of_subset`
`ssubset_trans` 📖	—	—	—	—	`trans`
`subset_antisymm` 📖	—	—	—	—	`antisymm`
`subset_antisymm_iff` 📖	—	—	—	—	`Eq.subset` `Eq.superset` `HasSubset.Subset.antisymm`
`subset_iff_ssubset_or_eq` 📖	—	—	—	—	`HasSubset.Subset.ssubset_or_eq` `subset_of_ssubset` `subset_of_eq`
`subset_of_eq` 📖	—	—	—	—	`subset_rfl`
`subset_of_eq_of_subset` 📖	—	—	—	—	—
`subset_of_ssubset` 📖	—	—	—	—	`ssubset_iff_subset_not_subset`
`subset_of_subset_of_eq` 📖	—	—	—	—	—
`subset_refl` 📖	—	—	—	—	`refl`
`subset_rfl` 📖	—	—	—	—	`refl`
`subset_trans` 📖	—	—	—	—	`trans`
`superset_antisymm` 📖	—	—	—	—	`antisymm'`
`superset_antisymm_iff` 📖	—	—	—	—	`Eq.superset` `Eq.subset` `HasSubset.Subset.antisymm'`
`superset_of_eq` 📖	—	—	—	—	`subset_rfl`
`transitive_ge` 📖	mathematical	—	`Transitive` `Preorder.toLE`	—	`transitive_of_trans` `instIsTransGe`
`transitive_gt` 📖	mathematical	—	`Transitive` `Preorder.toLT`	—	`transitive_of_trans` `instIsTransGt`
`transitive_le` 📖	mathematical	—	`Transitive` `Preorder.toLE`	—	`transitive_of_trans` `instIsTransLe`
`transitive_lt` 📖	mathematical	—	`Transitive` `Preorder.toLT`	—	`transitive_of_trans` `instIsTransLt`
`wellFoundedGT_dual_iff` 📖	mathematical	—	`WellFoundedGT` `OrderDual` `OrderDual.instLT` `WellFoundedLT`	—	`IsWellFounded.wf`
`wellFoundedLT_dual_iff` 📖	mathematical	—	`WellFoundedLT` `OrderDual` `OrderDual.instLT` `WellFoundedGT`	—	`IsWellFounded.wf`
`wellFounded_gt` 📖	—	—	—	—	`IsWellFounded.wf`
`wellFounded_lt` 📖	—	—	—	—	`IsWellFounded.wf`

---

← Back to Index