Max

Statistics

Metric	Count
Definitions `IsBot`, `IsMax`, `IsMin`, `IsTop`, `NoBotOrder`, `NoMaxOrder`, `NoMinOrder`, `NoTopOrder`	8
Theorems `fst`, `isMin`, `isMin_iff`, `lt_of_ne`, `lt_of_ne'`, `mono`, `not_isMax`, `not_isTop`, `ofDual`, `prodMk`, `snd`, `toDual`, `toNoMaxOrder`, `toNoMinOrder`, `eq_of_ge`, `eq_of_le`, `fst`, `mono`, `not_lt`, `ofDual`, `prodMk`, `snd`, `toDual`, `eq_of_ge`, `eq_of_le`, `fst`, `mono`, `not_lt`, `ofDual`, `prodMk`, `snd`, `toDual`, `fst`, `isMax`, `isMax_iff`, `lt_of_ne`, `lt_of_ne'`, `mono`, `not_isBot`, `not_isMin`, `ofDual`, `prodMk`, `snd`, `toDual`, `not_isMax`, `not_isMin`, `exists_not_ge`, `to_noMinOrder`, `exists_gt`, `not_acc`, `exists_lt`, `not_acc`, `exists_not_le`, `to_noMaxOrder`, `noBotOrder`, `noMaxOrder`, `noMinOrder`, `noTopOrder`, `isBot_iff`, `isMax_iff`, `isMin_iff`, `isTop_iff`, `isBot`, `isMax`, `isMin`, `isTop`, `instNoBotOrderOfNoMinOrder`, `instNoMaxOrderForallOfNonempty`, `instNoMinOrderForallOfNonempty`, `instNoTopOrderOfNoMaxOrder`, `isBot_ofDual_iff`, `isBot_toDual_iff`, `isMax_iff_forall_not_lt`, `isMax_ofDual_iff`, `isMax_toDual_iff`, `isMin_iff_forall_not_lt`, `isMin_ofDual_iff`, `isMin_toDual_iff`, `isTop_ofDual_iff`, `isTop_toDual_iff`, `noBotOrder_iff_noMinOrder`, `noMaxOrder_of_left`, `noMaxOrder_of_right`, `noMinOrder_of_left`, `noMinOrder_of_right`, `noTopOrder_iff_noMaxOrder`, `nonempty_gt`, `nonempty_lt`, `not_isBot`, `not_isMax`, `not_isMax_iff`, `not_isMax_of_lt`, `not_isMin`, `not_isMin_iff`, `not_isMin_of_lt`, `not_isTop`	96
Total	104

IsBot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fst` 📖	—	`IsBot` `Prod.instLE_mathlib` `Preorder.toLE`	—	—	—
`isMin` 📖	mathematical	`IsBot`	`IsMin`	—	—
`isMin_iff` 📖	mathematical	`IsBot` `Preorder.toLE` `PartialOrder.toPreorder`	`IsMin`	—	`le_trans`
`lt_of_ne` 📖	mathematical	`IsBot` `Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLT`	—	`LE.le.lt_of_ne`
`lt_of_ne'` 📖	mathematical	`IsBot` `Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLT`	—	`LE.le.lt_of_ne'`
`mono` 📖	—	`IsBot` `Preorder.toLE`	—	—	`LE.le.trans`
`not_isMax` 📖	mathematical	`IsBot` `Preorder.toLE` `PartialOrder.toPreorder`	`IsMax`	—	`exists_ne` `IsMax.eq_of_ge` `LT.lt.le` `lt_of_ne`
`not_isTop` 📖	mathematical	`IsBot` `Preorder.toLE` `PartialOrder.toPreorder`	`IsTop`	—	`IsTop.isMax` `not_isMax`
`ofDual` 📖	mathematical	`IsBot` `OrderDual` `OrderDual.instLE`	`IsTop` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	`isTop_ofDual_iff`
`prodMk` 📖	mathematical	`IsBot` `Preorder.toLE`	`Prod.instLE_mathlib`	—	—
`snd` 📖	—	`IsBot` `Prod.instLE_mathlib` `Preorder.toLE`	—	—	—
`toDual` 📖	mathematical	`IsBot`	`IsTop` `OrderDual` `OrderDual.instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`isTop_toDual_iff`

IsEmpty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toNoMaxOrder` 📖	mathematical	—	`NoMaxOrder`	—	—
`toNoMinOrder` 📖	mathematical	—	`NoMinOrder`	—	—

IsMax

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_ge` 📖	—	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`LE.le.antisymm'`
`eq_of_le` 📖	—	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`LE.le.antisymm`
`fst` 📖	—	`IsMax` `Prod.instLE_mathlib` `Preorder.toLE`	—	—	`le_rfl`
`mono` 📖	—	`IsMax` `Preorder.toLE`	—	—	`LE.le.trans'`
`not_lt` 📖	mathematical	`IsMax` `Preorder.toLE`	`Preorder.toLT`	—	`LT.lt.not_ge` `LT.lt.le`
`ofDual` 📖	mathematical	`IsMax` `OrderDual` `OrderDual.instLE`	`IsMin` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	`isMin_ofDual_iff`
`prodMk` 📖	mathematical	`IsMax` `Preorder.toLE`	`Prod.instLE_mathlib`	—	—
`snd` 📖	—	`IsMax` `Prod.instLE_mathlib` `Preorder.toLE`	—	—	`le_rfl`
`toDual` 📖	mathematical	`IsMax`	`IsMin` `OrderDual` `OrderDual.instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`isMin_toDual_iff`

IsMin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_ge` 📖	—	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`LE.le.antisymm'`
`eq_of_le` 📖	—	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`LE.le.antisymm`
`fst` 📖	—	`IsMin` `Prod.instLE_mathlib` `Preorder.toLE`	—	—	`le_rfl`
`mono` 📖	—	`IsMin` `Preorder.toLE`	—	—	`LE.le.trans`
`not_lt` 📖	mathematical	`IsMin` `Preorder.toLE`	`Preorder.toLT`	—	`LT.lt.not_ge` `LT.lt.le`
`ofDual` 📖	mathematical	`IsMin` `OrderDual` `OrderDual.instLE`	`IsMax` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	`isMax_ofDual_iff`
`prodMk` 📖	mathematical	`IsMin` `Preorder.toLE`	`Prod.instLE_mathlib`	—	—
`snd` 📖	—	`IsMin` `Prod.instLE_mathlib` `Preorder.toLE`	—	—	`le_rfl`
`toDual` 📖	mathematical	`IsMin`	`IsMax` `OrderDual` `OrderDual.instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`isMax_toDual_iff`

IsTop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fst` 📖	—	`IsTop` `Prod.instLE_mathlib` `Preorder.toLE`	—	—	—
`isMax` 📖	mathematical	`IsTop`	`IsMax`	—	—
`isMax_iff` 📖	mathematical	`IsTop` `Preorder.toLE` `PartialOrder.toPreorder`	`IsMax`	—	`ge_antisymm_iff` `ge_trans`
`lt_of_ne` 📖	mathematical	`IsTop` `Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLT`	—	`LE.le.lt_of_ne`
`lt_of_ne'` 📖	mathematical	`IsTop` `Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLT`	—	`LE.le.lt_of_ne'`
`mono` 📖	—	`IsTop` `Preorder.toLE`	—	—	`LE.le.trans'`
`not_isBot` 📖	mathematical	`IsTop` `Preorder.toLE` `PartialOrder.toPreorder`	`IsBot`	—	`IsBot.isMin` `not_isMin`
`not_isMin` 📖	mathematical	`IsTop` `Preorder.toLE` `PartialOrder.toPreorder`	`IsMin`	—	`exists_ne` `IsMin.eq_of_le` `LT.lt.le` `lt_of_ne'`
`ofDual` 📖	mathematical	`IsTop` `OrderDual` `OrderDual.instLE`	`IsBot` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	`isBot_ofDual_iff`
`prodMk` 📖	mathematical	`IsTop` `Preorder.toLE`	`Prod.instLE_mathlib`	—	—
`snd` 📖	—	`IsTop` `Prod.instLE_mathlib` `Preorder.toLE`	—	—	—
`toDual` 📖	mathematical	`IsTop`	`IsBot` `OrderDual` `OrderDual.instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`isBot_toDual_iff`

LT.lt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_isMax` 📖	mathematical	`Preorder.toLT`	`IsMax` `Preorder.toLE`	—	`not_isMax_of_lt`
`not_isMin` 📖	mathematical	`Preorder.toLT`	`IsMin` `Preorder.toLE`	—	`not_isMin_of_lt`

NoBotOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_not_ge` 📖	—	—	—	—	—
`to_noMinOrder` 📖	mathematical	—	`NoMinOrder` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`exists_not_ge`

NoMaxOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_gt` 📖	—	—	—	—	—
`not_acc` 📖	—	—	—	—	`exists_gt`

NoMinOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_lt` 📖	—	—	—	—	—
`not_acc` 📖	—	—	—	—	`exists_lt`

NoTopOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_not_le` 📖	—	—	—	—	—
`to_noMaxOrder` 📖	mathematical	—	`NoMaxOrder` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`not_le` `exists_not_le`

OrderDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`noBotOrder` 📖	mathematical	—	`NoBotOrder` `OrderDual` `instLE`	—	`NoTopOrder.exists_not_le`
`noMaxOrder` 📖	mathematical	—	`NoMaxOrder` `OrderDual` `instLT`	—	`NoMinOrder.exists_lt`
`noMinOrder` 📖	mathematical	—	`NoMinOrder` `OrderDual` `instLT`	—	`NoMaxOrder.exists_gt`
`noTopOrder` 📖	mathematical	—	`NoTopOrder` `OrderDual` `instLE`	—	`NoBotOrder.exists_not_ge`

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBot_iff` 📖	mathematical	—	`IsBot` `instLE_mathlib` `Preorder.toLE`	—	`IsBot.fst` `IsBot.snd` `IsBot.prodMk`
`isMax_iff` 📖	mathematical	—	`IsMax` `instLE_mathlib` `Preorder.toLE`	—	`IsMax.fst` `IsMax.snd` `IsMax.prodMk`
`isMin_iff` 📖	mathematical	—	`IsMin` `instLE_mathlib` `Preorder.toLE`	—	`IsMin.fst` `IsMin.snd` `IsMin.prodMk`
`isTop_iff` 📖	mathematical	—	`IsTop` `instLE_mathlib` `Preorder.toLE`	—	`IsTop.fst` `IsTop.snd` `IsTop.prodMk`

Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBot` 📖	mathematical	—	`IsBot` `Preorder.toLE`	—	`Eq.le`
`isMax` 📖	mathematical	—	`IsMax` `Preorder.toLE`	—	`IsTop.isMax` `isTop`
`isMin` 📖	mathematical	—	`IsMin` `Preorder.toLE`	—	`IsBot.isMin` `isBot`
`isTop` 📖	mathematical	—	`IsTop` `Preorder.toLE`	—	`Eq.ge`

(root)

Definitions

Name	Category	Theorems
`IsBot` 📖	MathDef	26 math math: `isBot_ofDual_iff`, `isTop_toDual_iff`, `isBot_iff_eq_bot`, `IsMin.isBot`, `isBot_iff_isMin`, `Prod.isBot_iff`, `IsTop.ofDual`, `disjoint_nhds_atBot_iff`, `not_isBot`, `isBot_one`, `Set.finite_isBot`, `isBot_toDual_iff`, `Subsingleton.isBot`, `nhdsLT_eq_bot_iff`, `isLUB_empty_iff`, `isBot_or_exists_lt`, `isBot_bot`, `isBot_zero`, `isLeast_univ_iff`, `Set.countable_isBot`, `isTop_ofDual_iff`, `not_isBot_iff_ne_bot`, `IsTop.toDual`, `Set.subsingleton_isBot`, `LieAlgebra.engel_isBot_of_isMin`, `IsTop.not_isBot`
`IsMax` 📖	MathDef	84 math math: `isMax_iff_eq_top`, `Order.isMax_or_mem_range_pred_or_isPredLimit`, `isMin_toDual_iff`, `Flag.isMax_coe`, `IsMax.of_succ_le`, `exists_covBy_seq_of_wellFoundedLT_wellFoundedGT`, `infPrime_iff_not_isMax`, `Order.krullDim_le_one_iff`, `IsMin.not_isMax`, `LocalSubring.isMax_iff`, `isMax_top`, `isTop_iff_isMax`, `ValuationSubring.isMax_toLocalSubring`, `not_isMax`, `Order.krullDim_nonpos_iff_forall_isMax`, `Order.IsSuccLimit.isMax`, `Order.IsPredPrelimit.isMax`, `PrimeSpectrum.isMax_iff`, `not_infIrred`, `maximal_gt_iff`, `PartENat.not_isMax_natCast`, `Order.max_of_succ_le`, `Order.isPredPrelimit_iff`, `zorn_le`, `isMax_ofDual_iff`, `Finset.Ioi_nonempty`, `WithTop.coe_covBy_top`, `isMax_of_succ_notMem`, `Order.succ_eq_iff_isMax`, `isMax_grade_iff`, `Order.succ_le_iff_isMax`, `Order.IsPredPrelimit.isMax_of_noMin`, `IsTop.isMax_iff`, `not_isMax_of_lt`, `Order.isPredPrelimit_iff_of_noMin`, `IsBot.not_isMax`, `Order.not_isMax_zero`, `Finset.Ioi_eq_empty`, `isMax_toDual_iff`, `Order.isMax_iterate_succ_of_eq_of_lt`, `Prod.isMax_iff`, `Prod.Lex.covBy_iff`, `not_infPrime`, `maximal_ge_iff`, `IsMin.ofDual`, `CategoryTheory.Functor.WellOrderInductionData.Extension.map_succ`, `WithTop.coe_wcovBy_top`, `Order.isMax_iterate_succ_of_eq_of_ne`, `Order.coheight_eq_zero`, `infIrred_iff_not_isMax`, `Order.lt_succ_iff_not_isMax`, `maximal_true`, `isMax_iff_forall_not_lt`, `succ_notMem_iff_isMax`, `Order.IsSuccPrelimit.isMax`, `IsTop.isMax`, `Order.krullDim_le_one_iff_forall_isMax`, `zorn_le_nonempty_Ici₀`, `Set.Ioi_eq_empty_iff`, `Prod.Lex.toLex_covBy_toLex_iff`, `OrderIso.isMax_apply`, `not_isMax_iff`, `Order.not_isPredLimit_iff`, `HomotopicalAlgebra.RelativeCellComplex.Cells.hj`, `Finset.nonempty_Ioi`, `isMin_ofDual_iff`, `LT.lt.not_isMax`, `Order.not_isMax_pred`, `Order.coheight_pos`, `Set.Ioi_nonempty`, `IsMin.toDual`, `not_isMax_bot`, `SuccOrder.max_of_succ_le`, `Order.coheight_ne_zero`, `zorn_le_nonempty`, `HahnEmbedding.Partial.exists_isMax`, `IsMin.not_isMax'`, `Subsingleton.isMax`, `Order.IsPredLimit.not_isMax`, `Order.not_isSuccPrelimit_iff`, `not_isMax_iff_ne_top`, `StrictAnti.isMax_of_apply`, `maximal_iff_isMax`, `LinearLocallyFiniteOrder.isMax_of_succFn_le`
`IsMin` 📖	MathDef	78 math math: `not_isMin_iff`, `OrderIso.isMin_apply`, `isMin_toDual_iff`, `not_isMin`, `PrincipalSeg.isMin_apply_iff`, `Order.IsSuccPrelimit.isMin`, `not_supPrime`, `isMin_of_pred_notMem`, `Order.height_ne_zero`, `Order.not_isPredPrelimit_iff`, `Order.IsSuccPrelimit.isMin_of_noMax`, `IsBot.isMin`, `exists_covBy_seq_of_wellFoundedLT_wellFoundedGT`, `Order.krullDim_le_one_iff`, `minimal_le_iff`, `Set.Iio_eq_empty_iff`, `Order.height_pos`, `Order.min_of_le_pred`, `Order.krullDim_nonpos_iff_forall_isMin`, `Order.IsPredLimit.isMin`, `Order.isMin_or_mem_range_succ_or_isSuccLimit`, `Subsingleton.isMin`, `isMax_ofDual_iff`, `PrimeSpectrum.isMin_iff`, `Order.isSuccPrelimit_iff`, `SupPrime.not_isMin`, `supPrime_iff_not_isMin`, `IsMax.toDual`, `Flag.isMin_coe`, `isBot_iff_isMin`, `Order.pred_lt_iff_not_isMin`, `Finset.Iio_nonempty`, `supIrred_iff_not_isMin`, `not_isMin_iff_ne_bot`, `IsMax.not_isMin'`, `Order.height_eq_zero`, `IsMin.of_le_pred`, `isMax_toDual_iff`, `Order.not_isMin_succ`, `Prod.Lex.covBy_iff`, `WithBot.bot_covBy_coe`, `pred_notMem_iff_isMin`, `Order.isMin_iterate_pred_of_eq_of_lt`, `Order.IsSuccLimit.not_isMin`, `Set.Iio_nonempty`, `Finset.nonempty_Iio`, `IsBot.isMin_iff`, `PrimeSpectrum.finite_setOf_isMin`, `not_isMin_of_lt`, `Order.IsPredPrelimit.isMin`, `IsTop.not_isMin`, `LT.lt.not_isMin`, `Order.not_isSuccLimit_iff`, `not_isMin_top`, `Order.pred_eq_iff_isMin`, `SupIrred.not_isMin`, `StrictAnti.isMin_of_apply`, `isMin_iff_eq_bot`, `Order.isMin_iterate_pred_of_eq_of_ne`, `minimal_lt_iff`, `isMin_iff_forall_not_lt`, `Order.le_pred_iff_isMin`, `Prod.Lex.toLex_covBy_toLex_iff`, `not_supIrred`, `PredOrder.min_of_le_pred`, `IsMax.not_isMin`, `minimal_true`, `Prod.isMin_iff`, `isMin_ofDual_iff`, `Order.krullDim_le_one_iff_forall_isMin`, `isMin_bot`, `IsMax.ofDual`, `Order.isSuccPrelimit_iff_of_noMax`, `WithBot.bot_wcovBy_coe`, `isMin_grade_iff`, `minimal_iff_isMin`, `InitialSeg.isMin_apply_iff`, `Finset.Iio_eq_empty`
`IsTop` 📖	MathDef	24 math math: `isGLB_empty_iff`, `isBot_ofDual_iff`, `IsMax.isTop`, `isTop_toDual_iff`, `Subsingleton.isTop`, `IsBot.toDual`, `isTop_or_exists_gt`, `isTop_iff_isMax`, `Set.subsingleton_isTop`, `IsBot.ofDual`, `Prod.isTop_iff`, `Set.finite_isTop`, `not_isTop_iff_ne_top`, `isBot_toDual_iff`, `IsBot.not_isTop`, `Set.countable_isTop`, `not_isTop`, `isTop_iff_eq_top`, `nhdsGT_eq_bot_iff`, `isGreatest_univ_iff`, `isTop_ofDual_iff`, `disjoint_nhds_atTop_iff`, `Set.Ici_eq_singleton_iff_isTop`, `isTop_top`
`NoBotOrder` 📖	CompData	6 math math: `instNoBotOrderOfNoMinOrder`, `FirstOrder.Language.realize_noBotOrder_iff`, `WithTop.noBotOrder`, `noBotOrder_iff_noMinOrder`, `OrderDual.noBotOrder`, `FirstOrder.Language.noBotOrder_of_dlo`
`NoMaxOrder` 📖	CompData	36 math math: `Irrational.instNoMaxOrderSubtypeReal`, `IsEmpty.toNoMaxOrder`, `Set.instNoMaxOrderElemIoi`, `Sum.Lex.noMaxOrder`, `noTopOrder_iff_noMaxOrder`, `instNoMaxOrderOfNontrivial`, `Sum.Lex.noMaxOrder_of_nonempty`, `PSigma.Lex.noMaxOrder_of_nonempty`, `Cardinal.noMaxOrder`, `Nonneg.noMaxOrder`, `Pi.Colex.noMaxOrder'`, `Field.Emb.Cardinal.noMaxOrder_rank_toType`, `Cardinal.instNoMaxOrder`, `Ordinal.toType_noMax_of_succ_lt`, `Sigma.Lex.noMaxOrder_of_nonempty`, `Prod.Lex.noMaxOrder_of_left`, `Nat.instNoMaxOrder`, `noMaxOrder_of_right`, `instNoMaxOrderElemIco`, `IsStrictOrderedRing.toNoMaxOrder`, `WithBot.noMaxOrder`, `Sum.noMaxOrder`, `Nimber.instNoMaxOrder`, `Ordinal.instNoMaxOrder`, `Prod.Lex.noMaxOrder_of_right`, `noMaxOrder_of_left`, `Sum.noMaxOrder_iff`, `OrderDual.noMaxOrder`, `instNoMaxOrderElemIoo`, `PNat.instNoMaxOrder`, `LinearOrderedAddCommGroup.to_noMaxOrder`, `NoTopOrder.to_noMaxOrder`, `LinearOrderedCommGroup.to_noMaxOrder`, `Set.instNoMaxOrderElemIci`, `Pi.Lex.noMaxOrder'`, `instNoMaxOrderElemIio`
`NoMinOrder` 📖	CompData	24 math math: `Sum.noMinOrder`, `Set.instNoMinOrderElemIic`, `IsEmpty.toNoMinOrder`, `Prod.Lex.noMinOrder_of_left`, `noMinOrder_of_left`, `PSigma.Lex.noMinOrder_of_nonempty`, `instNoMinOrderElemIoo`, `instNoMinOrderOfNontrivial`, `Set.instNoMinOrderElemIio`, `Sum.noMinOrder_iff`, `Prod.Lex.noMinOrder_of_right`, `NoBotOrder.to_noMinOrder`, `Irrational.instNoMinOrderSubtypeReal`, `OrderDual.noMinOrder`, `instNoMinOrderElemIoi`, `instNoMinOrderElemIoc`, `noBotOrder_iff_noMinOrder`, `LinearOrderedCommGroup.to_noMinOrder`, `WithTop.noMinOrder`, `noMinOrder_of_right`, `Sigma.Lex.noMinOrder_of_nonempty`, `Sum.Lex.noMinOrder`, `Sum.Lex.noMinOrder_of_nonempty`, `LinearOrderedAddCommGroup.to_noMinOrder`
`NoTopOrder` 📖	CompData	6 math math: `WithBot.noTopOrder`, `noTopOrder_iff_noMaxOrder`, `FirstOrder.Language.realize_noTopOrder_iff`, `instNoTopOrderOfNoMaxOrder`, `OrderDual.noTopOrder`, `FirstOrder.Language.noTopOrder_of_dlo`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNoBotOrderOfNoMinOrder` 📖	mathematical	—	`NoBotOrder` `Preorder.toLE`	—	`not_le_of_gt` `NoMinOrder.exists_lt`
`instNoMaxOrderForallOfNonempty` 📖	mathematical	`NoMaxOrder` `Preorder.toLT`	`Pi.preorder`	—	`NoMaxOrder.exists_gt` `lt_update_self_iff`
`instNoMinOrderForallOfNonempty` 📖	mathematical	`NoMinOrder` `Preorder.toLT`	`Pi.preorder`	—	`NoMinOrder.exists_lt` `update_lt_self_iff`
`instNoTopOrderOfNoMaxOrder` 📖	mathematical	—	`NoTopOrder` `Preorder.toLE`	—	`not_le_of_gt` `NoMaxOrder.exists_gt`
`isBot_ofDual_iff` 📖	mathematical	—	`IsBot` `DFunLike.coe` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `IsTop` `OrderDual.instLE`	—	—
`isBot_toDual_iff` 📖	mathematical	—	`IsBot` `OrderDual` `OrderDual.instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `IsTop`	—	—
`isMax_iff_forall_not_lt` 📖	mathematical	—	`IsMax` `Preorder.toLE` `Preorder.toLT`	—	`IsMax.not_lt` `of_not_not` `LE.le.lt_of_not_ge`
`isMax_ofDual_iff` 📖	mathematical	—	`IsMax` `DFunLike.coe` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `IsMin` `OrderDual.instLE`	—	—
`isMax_toDual_iff` 📖	mathematical	—	`IsMax` `OrderDual` `OrderDual.instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `IsMin`	—	—
`isMin_iff_forall_not_lt` 📖	mathematical	—	`IsMin` `Preorder.toLE` `Preorder.toLT`	—	`IsMin.not_lt` `of_not_not` `LE.le.lt_of_not_ge`
`isMin_ofDual_iff` 📖	mathematical	—	`IsMin` `DFunLike.coe` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `IsMax` `OrderDual.instLE`	—	—
`isMin_toDual_iff` 📖	mathematical	—	`IsMin` `OrderDual` `OrderDual.instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `IsMax`	—	—
`isTop_ofDual_iff` 📖	mathematical	—	`IsTop` `DFunLike.coe` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `IsBot` `OrderDual.instLE`	—	—
`isTop_toDual_iff` 📖	mathematical	—	`IsTop` `OrderDual` `OrderDual.instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `IsBot`	—	—
`noBotOrder_iff_noMinOrder` 📖	mathematical	—	`NoBotOrder` `Preorder.toLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `NoMinOrder` `Preorder.toLT`	—	`NoBotOrder.to_noMinOrder` `instNoBotOrderOfNoMinOrder`
`noMaxOrder_of_left` 📖	mathematical	—	`NoMaxOrder` `Preorder.toLT` `Prod.instPreorder`	—	`NoMaxOrder.exists_gt` `Prod.mk_lt_mk_iff_left`
`noMaxOrder_of_right` 📖	mathematical	—	`NoMaxOrder` `Preorder.toLT` `Prod.instPreorder`	—	`NoMaxOrder.exists_gt` `Prod.mk_lt_mk_iff_right`
`noMinOrder_of_left` 📖	mathematical	—	`NoMinOrder` `Preorder.toLT` `Prod.instPreorder`	—	`NoMinOrder.exists_lt` `Prod.mk_lt_mk_iff_left`
`noMinOrder_of_right` 📖	mathematical	—	`NoMinOrder` `Preorder.toLT` `Prod.instPreorder`	—	`NoMinOrder.exists_lt` `Prod.mk_lt_mk_iff_right`
`noTopOrder_iff_noMaxOrder` 📖	mathematical	—	`NoTopOrder` `Preorder.toLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `NoMaxOrder` `Preorder.toLT`	—	`NoTopOrder.to_noMaxOrder` `instNoTopOrderOfNoMaxOrder`
`nonempty_gt` 📖	—	—	—	—	`nonempty_subtype` `NoMaxOrder.exists_gt`
`nonempty_lt` 📖	—	—	—	—	`nonempty_subtype` `NoMinOrder.exists_lt`
`not_isBot` 📖	mathematical	—	`IsBot`	—	`NoBotOrder.exists_not_ge`
`not_isMax` 📖	mathematical	—	`IsMax` `Preorder.toLE`	—	`not_isMax_iff` `NoMaxOrder.exists_gt`
`not_isMax_iff` 📖	mathematical	—	`IsMax` `Preorder.toLE` `Preorder.toLT`	—	`lt_iff_le_not_ge`
`not_isMax_of_lt` 📖	mathematical	`Preorder.toLT`	`IsMax` `Preorder.toLE`	—	`IsMax.not_lt`
`not_isMin` 📖	mathematical	—	`IsMin` `Preorder.toLE`	—	`not_isMin_iff` `NoMinOrder.exists_lt`
`not_isMin_iff` 📖	mathematical	—	`IsMin` `Preorder.toLE` `Preorder.toLT`	—	—
`not_isMin_of_lt` 📖	mathematical	`Preorder.toLT`	`IsMin` `Preorder.toLE`	—	`IsMin.not_lt`
`not_isTop` 📖	mathematical	—	`IsTop`	—	`NoTopOrder.exists_not_le`

---

← Back to Index