WithBot

📁 Source: Mathlib/Order/WithBot.lean

Statistics

Metric	Count
Definitions withBotCongr, withBotSubtypeNe, withTopCongr, withTopSubtypeNe, WithBot, LE, LT, decidableEq, decidableLE, decidableLT, distribLattice, instBoundedOrder, instLE, instLT, instOrderBot, instOrderTop, instPartialOrder, instPreorder, instTop, instUniqueOfIsEmpty, lattice, linearOrder, map, map₂, ofDual, semilatticeInf, semilatticeSup, toDual, unbot, unbotA, unbotD, decidableEq, decidableLE, decidableLT, distribLattice, instBot, instBoundedOrder, instLE, instLT, instOrderBot, instOrderTop, instPartialOrder, instPreorder, instUniqueOfIsEmpty, lattice, linearOrder, map, map₂, ofDual, semilatticeInf, semilatticeSup, toDual, untop, untopA, untopD	55
Theorems withBotCongr_apply, withBotCongr_refl, withBotCongr_symm, withBotCongr_trans, withBotSubtypeNe_apply, withBotSubtypeNe_symm_apply_coe, withTopCongr_apply, withTopCongr_refl, withTopCongr_symm, withTopCongr_trans, withTopSubtypeNe_apply, withTopSubtypeNe_symm_apply_coe, withBot, withTop, withBot_map, withTop_map, withBot_map, withTop_map, gt, lt, bot_lt_coe, bot_lt_iff_ne_bot, bot_ne_coe, canLift, coe_eq_coe, coe_eq_top, coe_inf, coe_inj, coe_injective, coe_le, coe_le_coe, coe_le_iff, coe_lt_coe, coe_max, coe_min, coe_mono, coe_ne_bot, coe_strictMono, coe_sup, coe_top, coe_unbot, comp_map, denselyOrdered, denselyOrdered_iff, eq_bot_iff_forall_le, eq_bot_iff_forall_lt, eq_bot_iff_forall_ne, eq_of_forall_coe_le_iff, eq_of_forall_le_coe_iff, eq_top_iff_forall_ge, eq_unbot_iff, exists, exists_coe_le, exists_coe_lt, exists_ne_bot, forall, forall_coe_le, forall_coe_le_iff_le, forall_coe_lt, forall_le_coe_iff_le, forall_ne_bot, ge_of_forall_gt_iff_ge, instWellFoundedGT, instWellFoundedLT, le_bot_iff, le_coe_iff, le_coe_unbotD, le_def, le_def', le_def_aux, le_iff_forall, le_ofDual_iff, le_of_forall_lt_iff_le, le_toDual_iff, le_unbotA, le_unbotA_iff, le_unbotD, le_unbotD_iff, le_unbot_iff, lt_coe_bot, lt_coe_iff, lt_def, lt_def', lt_def_aux, lt_iff_exists, lt_iff_exists_coe, lt_iff_exists_coe_btwn, lt_iff_exists_coe_btwn', lt_ofDual_iff, lt_toDual_iff, lt_unbotA_iff, lt_unbotD_iff, lt_unbot_iff, map_bot, map_coe, map_comm, map_comp_map, map_eq_bot_iff, map_eq_some_iff, map_id, map_injective, map_le_iff, map_map, map_ofDual, map_toDual, map₂_bot_left, map₂_bot_right, map₂_coe_coe, map₂_coe_left, map₂_coe_right, map₂_eq_bot_iff, monotone_iff, monotone_map_iff, ne_bot_iff_exists, noMaxOrder, noTopOrder, none_eq_bot, nontrivial, not_coe_le_bot, not_lt_bot, ofDual_apply_bot, ofDual_apply_coe, ofDual_bot, ofDual_le_iff, ofDual_le_ofDual_iff, ofDual_lt_iff, ofDual_lt_ofDual_iff, ofDual_map, ofDual_symm, ofDual_symm_apply, some_eq_coe, some_eq_map_iff, strictAnti_iff, strictMono_iff, strictMono_map_iff, toDual_apply_bot, toDual_apply_coe, toDual_bot, toDual_le_iff, toDual_le_toDual_iff, toDual_lt_iff, toDual_lt_toDual_iff, toDual_map, toDual_symm, toDual_symm_apply, top_eq_coe, total_le, gt, lt, unbotA_eq_unbot, unbotA_le_iff, unbotA_lt_iff, unbotA_mono, unbotD_bot, unbotD_coe, unbotD_eq_iff, unbotD_eq_self_iff, unbotD_eq_unbotD_iff, unbotD_le_iff, unbotD_lt_iff, unbotD_mono, unbot_coe, unbot_eq_iff, unbot_le_iff, unbot_le_unbot, unbot_le_unbot_iff, unbot_lt_iff, unbot_lt_unbot, unbot_lt_unbot_iff, unbot_mono, gt, lt, bot_eq_coe, canLift, coe_bot, coe_eq_bot, coe_eq_coe, coe_inf, coe_inj, coe_injective, coe_le_coe, coe_le_iff, coe_lt_coe, coe_lt_iff, coe_lt_top, coe_max, coe_min, coe_mono, coe_ne_top, coe_strictMono, coe_sup, coe_top_lt, coe_untop, coe_untopD_le, comp_map, denselyOrdered, denselyOrdered_iff, eq_bot_iff_forall_le, eq_of_forall_coe_le_iff, eq_of_forall_le_coe_iff, eq_top_iff_forall_ge, eq_top_iff_forall_gt, eq_top_iff_forall_ne, eq_untop_iff, exists, exists_le_coe, exists_lt_coe, exists_ne_top, forall, forall_coe_le_iff_le, forall_le_coe, forall_le_coe_iff_le, forall_lt_coe, forall_ne_top, ge_of_forall_gt_iff_ge, instWellFoundedGT, instWellFoundedLT, le_coe, le_coe_iff, le_def, le_def', le_iff_forall, le_ofDual_iff, le_of_forall_lt_iff_le, le_toDual_iff, le_untopA_iff, le_untopD_iff, le_untop_iff, lt_def, lt_def', lt_iff_exists, lt_iff_exists_coe, lt_iff_exists_coe_btwn, lt_iff_exists_coe_btwn', lt_ofDual_iff, lt_toDual_iff, lt_top_iff_ne_top, lt_untopA_iff, lt_untopD_iff, lt_untop_iff, map_coe, map_comm, map_comp_map, map_eq_some_iff, map_eq_top_iff, map_id, map_injective, map_le_iff, map_map, map_ofDual, map_toDual, map_top, map₂_coe_coe, map₂_coe_left, map₂_coe_right, map₂_eq_top_iff, map₂_top_left, map₂_top_right, monotone_iff, monotone_map_iff, ne_top_iff_exists, noBotOrder, noMinOrder, none_eq_top, nontrivial, not_top_le_coe, not_top_lt, ofDual_apply_coe, ofDual_apply_top, ofDual_le_iff, ofDual_le_ofDual_iff, ofDual_lt_iff, ofDual_lt_ofDual_iff, ofDual_map, ofDual_symm, ofDual_symm_apply, ofDual_top, some_eq_coe, some_eq_map_iff, strictAnti_iff, strictMono_iff, strictMono_map_iff, toDual_apply_coe, toDual_apply_top, toDual_le_iff, toDual_le_toDual_iff, toDual_lt_iff, toDual_lt_toDual_iff, toDual_map, toDual_symm, toDual_symm_apply, toDual_top, top_le_iff, top_ne_coe, total_le, gt, lt, untopA_eq_untop, untopA_le, untopA_le_iff, untopA_lt_iff, untopA_mono, untopD_coe, untopD_eq_iff, untopD_eq_self_iff, untopD_eq_untopD_iff, untopD_le, untopD_le_iff, untopD_lt_iff, untopD_mono, untopD_top, untop_coe, untop_eq_iff, untop_le_iff, untop_le_untop_iff, untop_lt_iff, untop_lt_untop_iff, untop_mono	318
Total	373

Equiv

Definitions

Name	Category	Theorems
withBotCongr 📖	CompOp	5 math math: withBotCongr_apply, OrderIso.withBotCongr_symm_apply, withBotCongr_refl, withBotCongr_symm, withBotCongr_trans
withBotSubtypeNe 📖	CompOp	2 math math: withBotSubtypeNe_symm_apply_coe, withBotSubtypeNe_apply
withTopCongr 📖	CompOp	5 math math: withTopCongr_trans, withTopCongr_apply, withTopCongr_refl, withTopCongr_symm, OrderIso.withTopCongr_symm_apply
withTopSubtypeNe 📖	CompOp	2 math math: withTopSubtypeNe_symm_apply_coe, withTopSubtypeNe_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
withBotCongr_apply 📖	mathematical	—	DFunLike.coe Equiv WithBot EquivLike.toFunLike instEquivLike withBotCongr WithBot.map	—	—
withBotCongr_refl 📖	mathematical	—	withBotCongr refl WithBot	—	ext WithBot.map_id
withBotCongr_symm 📖	mathematical	—	withBotCongr symm WithBot	—	—
withBotCongr_trans 📖	mathematical	—	withBotCongr trans WithBot	—	ext WithBot.map_map
withBotSubtypeNe_apply 📖	mathematical	—	DFunLike.coe Equiv WithBot Bot.bot WithBot.bot EquivLike.toFunLike instEquivLike withBotSubtypeNe WithBot.unbot	—	—
withBotSubtypeNe_symm_apply_coe 📖	mathematical	—	WithBot Bot.bot WithBot.bot DFunLike.coe Equiv EquivLike.toFunLike instEquivLike symm withBotSubtypeNe WithBot.some	—	—
withTopCongr_apply 📖	mathematical	—	DFunLike.coe Equiv WithTop EquivLike.toFunLike instEquivLike withTopCongr WithTop.map	—	—
withTopCongr_refl 📖	mathematical	—	withTopCongr refl WithTop	—	ext WithTop.map_id
withTopCongr_symm 📖	mathematical	—	withTopCongr symm WithTop	—	—
withTopCongr_trans 📖	mathematical	—	withTopCongr trans WithTop	—	ext WithTop.map_map
withTopSubtypeNe_apply 📖	mathematical	—	DFunLike.coe Equiv WithTop Top.top WithTop.top EquivLike.toFunLike instEquivLike withTopSubtypeNe WithTop.untop	—	—
withTopSubtypeNe_symm_apply_coe 📖	mathematical	—	WithTop Top.top WithTop.top DFunLike.coe Equiv EquivLike.toFunLike instEquivLike symm withTopSubtypeNe WithTop.some	—	—

IsMax

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
withBot 📖	mathematical	IsMax	WithBot WithBot.instLE WithBot.some	—	—

IsMin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
withTop 📖	mathematical	IsMin	WithTop WithTop.instLE WithTop.some	—	WithTop.top_le_iff WithTop.coe_ne_top le_top WithTop.coe_le_coe

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
withBot_map 📖	mathematical	Monotone	WithBot WithBot.instPreorder WithBot.map	—	WithBot.monotone_map_iff
withTop_map 📖	mathematical	Monotone	WithTop WithTop.instPreorder WithTop.map	—	WithTop.monotone_map_iff

StrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
withBot_map 📖	mathematical	StrictMono	WithBot WithBot.instPreorder WithBot.map	—	WithBot.strictMono_map_iff
withTop_map 📖	mathematical	StrictMono	WithTop WithTop.instPreorder WithTop.map	—	WithTop.strictMono_map_iff

WithBot

Definitions

Name	Category	Theorems
LE 📖	CompData	1 math math: le_def_aux
LT 📖	CompData	1 math math: lt_def_aux
decidableEq 📖	CompOp	6 math math: mul_bot', Finset.max_mem_image_coe, Finset.max_mem_insert_bot_image_coe, mul_def, bot_mul', Polynomial.integralNormalization_coeff
decidableLE 📖	CompOp	—
decidableLT 📖	CompOp	—
distribLattice 📖	CompOp	—
instBoundedOrder 📖	CompOp	—
instLE 📖	CompOp	61 math math: coe_toDualTopEquiv_eq, add_le_add_iff_right', le_unbotA_iff, coe_le_zero, WithTop.toDualBotEquiv_coe, le_unbot_iff, addRightMono, not_coe_le_bot, zeroLEOneClass, orderIsoPUnitSumLex_symm_inl, addLeftMono, WithBotTop.coe_le_coe, WithTop.le_toDual_iff, ofDual_le_iff, orderIsoPUnitSumLex_symm_inr, noTopOrder, add_le_add_iff_left, IsMax.withBot, addLECancellable_of_ne_bot, coe_le_iff, le_unbotD_iff, le_coe_iff, coe_le, le_iff_forall, le_toDual_iff, WithTop.toDualBotEquiv_symm_top, add_le_add_iff_right, addLECancellable_coe, toDualTopEquiv_coe, coe_le_coe, toDual_le_iff, WithTop.ofDual_le_ofDual_iff, coe_nonneg, toDualTopEquiv_symm_bot, unbot_le_unbot, toDualTopEquiv_symm_coe, unbotD_le_iff, WithTop.toDual_le_toDual_iff, unbot_le_unbot_iff, WithTop.le_ofDual_iff, le_ofDual_iff, orderIsoPUnitSumLex_toLex, total_le, WithTop.toDualBotEquiv_symm_coe, unbot_le_iff, WithTop.ofDual_le_iff, le_add_self, toDualTopEquiv_bot, le_def', toDual_le_toDual_iff, le_bot_iff, le_self_add, WithTop.toDual_le_iff, le_def, ofDual_le_ofDual_iff, unbotA_le_iff, WithTop.coe_toDualBotEquiv, WithTop.toDualBotEquiv_top, coe_le_one, orderIsoPUnitSumLex_bot, one_le_coe
instLT 📖	CompOp	49 math math: lt_ofDual_iff, coe_lt_one, lt_unbotA_iff, WithTop.lt_toDual_iff, lt_coe_iff, one_lt_coe, addLeftReflectLT, lt_unbotD_iff, unbot_lt_iff, coe_pos, WithTop.ofDual_lt_ofDual_iff, unbotD_lt_iff, WithTop.toDual_lt_iff, coe_lt_zero, lt_iff_exists_coe, bot_lt_add, bot_neg, bot_lt_natCast, lt_def, instWellFoundedLT, ofDual_lt_iff, toDual_lt_toDual_iff, lt_unbot_iff, ofDual_lt_ofDual_iff, noMaxOrder, WithTop.toDual_lt_toDual_iff, lt_toDual_iff, not_lt_bot, denselyOrdered, coe_lt_coe, bot_lt_iff_ne_bot, denselyOrdered_iff, bot_lt_coe, sum_lt_bot, toDual_lt_iff, unbotA_lt_iff, WithTop.ofDual_lt_iff, lt_def', unbot_lt_unbot, instWellFoundedGT, bot_lt_sum_iff, addRightReflectLT, unbot_lt_unbot_iff, lt_iff_exists, WithTop.lt_ofDual_iff, WithBotTop.coe_lt_coe, bot_lt_one, add_lt_add_iff_left, add_lt_add_iff_right
instOrderBot 📖	CompOp	19 math math: LatticeHom.withTopWithBot_apply, LatticeHom.coe_withTopWithBot, BoxIntegral.Box.disjoint_withBotCoe, LatticeHom.withTopWithBot_id, LatticeHom.withTopWithBot_comp, LatticeHom.withTopWithBot'_toFun, Finset.max_eq_sup_coe, Finset.coe_sup', Polynomial.degree_sum_le, Finset.coe_sup_of_nonempty, Finset.max_eq_sup_withBot, BoxIntegral.Box.not_disjoint_coe_iff_nonempty_inter, LatticeHom.withTopWithBot_toFun, BoxIntegral.Box.disjoint_splitLower_splitUpper, BoxIntegral.Box.disjoint_coe, Polynomial.supDegree_eq_degree, Polynomial.degree_sum_eq_of_disjoint, AddMonoidAlgebra.supDegree_withBot_some_comp, Finset.sup_of_mem
instOrderTop 📖	CompOp	—
instPartialOrder 📖	CompOp	7 math math: BoxIntegral.Box.disjoint_withBotCoe, BoxIntegral.Box.not_disjoint_coe_iff_nonempty_inter, BoxIntegral.Box.disjoint_splitLower_splitUpper, BoxIntegral.Box.disjoint_coe, isOrderedAddMonoid, instArchimedean, instIsOrderedRing
instPreorder 📖	CompOp	347 math math: Polynomial.degree_map_le, Polynomial.modByMonic_eq_self_iff, IsAlgClosed.roots_eq_zero_iff_degree_nonpos, Polynomial.degree_mul_le, Order.LTSeries.length_le_krullDim, Polynomial.exists_degree_le_of_mem_span_of_finite, instPosMulStrictMono, Order.krullDim_le_of_strictComono_and_surj, WithBotTop.coe_strictMono, ringKrullDim_succ_le_ringKrullDim_polynomial, Order.krullDim_lt_coe_iff, Polynomial.coe_lt_degree, CategoryTheory.Retract.injectiveDimension_le, Polynomial.degree_le_degree, lt_iff_exists_coe_btwn, trichotomous.gt, CategoryTheory.injectiveDimension_le_iff, subtypeOrderIso_symm_apply, Cubic.degree_of_b_eq_zero, Polynomial.degree_quadratic_lt, instMulPosMono, Polynomial.degree_pow_le, Order.krullDim_nonneg_iff, Ring.krullDimLE_iff, Polynomial.zero_le_degree_iff, eq_bot_iff_forall_lt, Polynomial.mod_eq_self_iff, le_of_forall_lt_iff_le, range_coe, PowerSeries.degree_weierstrassMod_lt, Polynomial.degree_gcd_le_left, Order.krullDim_pos_iff, Order.krullDim_le_one_iff, image_coe_Ioo, Polynomial.degree_le_of_dvd, Polynomial.div_tendsto_zero_iff_degree_lt, BoxIntegral.Box.splitUpper_le, Polynomial.degree_lt_degree_mul_X, Polynomial.Splits.degree_le_one_of_irreducible, Polynomial.divByMonic_eq_zero_iff, Order.le_krullDim_iff, minpoly.degree_pos, lt_add_one_iff, Polynomial.tendsto_atTop_iff_leadingCoeff_nonneg, Polynomial.degree_list_prod_le, IsWellOrder.lt, Finset.max_mono, ringKrullDim_succ_le_ringKrullDim_powerseries, Lagrange.eq_interpolate_iff, lt_succ, Order.coheight_le_krullDim, Polynomial.degree_pos_of_root, Order.krullDim_nonpos_iff_forall_isMax, PowerSeries.degree_trunc_lt, Polynomial.card_roots_map_le_degree, Cubic.degree_of_a_eq_zero', ringKrullDim_nonneg_of_nontrivial, eq_top_iff_forall_ge, Ioc_bot_coe, Order.krullDim_nonpos_iff_forall_isMin, Polynomial.degree_mono, Polynomial.degree_C_lt_degree_C_mul_X, Polynomial.tendsto_atBot_iff_leadingCoeff_nonpos, List.coe_le_maximum_iff, Ioi_coe, monotone_map_iff, Module.supportDim_le_of_injective, instPosMulReflectLE, OrderHom.withBotMap_coe, minpoly.degree_le, image_coe_Ici, Ico_bot_coe, Polynomial.abs_tendsto_atTop_iff, PowerSeries.IsWeierstrassDivisionAt.degree_lt, Polynomial.degree_lt_wf, Polynomial.degree_cubic_lt, strictAnti_iff, ge_of_forall_gt_iff_ge, Order.height_le_krullDim, Polynomial.degree_modByMonic_le, Polynomial.natDegree_lt_natDegree_iff, CategoryTheory.injectiveDimension_ge_iff, OrderIso.withBotCongr_symm_apply, Polynomial.degree_divX_lt, exists_coe_le, Order.bot_lt_krullDim, Polynomial.degree_eraseLead_lt, instMulPosStrictMono, topologicalKrullDim_subspace_le, Polynomial.degree_X_pow_le, StrictMono.withBot_map, succ_mono, topologicalKrullDim_zero_of_discreteTopology, ringKrullDim_quotient_le, Polynomial.degree_monomial_le, pred_coe, Polynomial.natDegree_lt_iff_degree_lt, Lagrange.degree_interpolate_erase_lt, ringKrullDim_succ_le_of_surjective, BoxIntegral.Box.splitLower_le, Ideal.primeHeight_le_ringKrullDim, Polynomial.degree_quadratic_le, CategoryTheory.projectiveDimension_lt_iff, Lagrange.degree_interpolate_lt, preimage_coe_Ioc, Polynomial.abs_tendsto_atBot_iff, Polynomial.degree_X_le, coe_wcovBy_coe, preimage_coe_Ioi, ringKrullDim_le_iff_height_le, Polynomial.degree_derivative_lt, minpoly.degree_le_of_ne_zero, div_eq_quo_add_sum_rem_div, PowerBasis.mem_span_pow', Order.krullDim_nonpos_of_subsingleton, Iio_coe, WithZero.toMulBot_lt, Polynomial.degree_erase_lt, eq_bot_iff_forall_le, IsInducing.topologicalKrullDim_le, Polynomial.degree_le_of_natDegree_le, ringKrullDim_le_ringKrullDim_quotient_add_card, IsDiscreteValuationRing.bot_lt_toWithBotNat_iff, image_coe_Iio, Ideal.height_le_ringKrullDim_quotient_add_one, Iic_coe, Polynomial.degree_sum_le, Polynomial.degree_pos_of_ne_zero_of_nonunit, Irreducible.degree_pos, image_coe_Ico, Ioc_coe, instPosMulMono, Polynomial.Monic.degree_pos, lt_iff_exists_coe_btwn', Polynomial.degree_le_natDegree, image_coe_Ioi, monotone_iff, Polynomial.degree_divByMonic_le, Polynomial.degree_le_mul_left, IsClosedEmbedding.topologicalKrullDim_le, ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank, Polynomial.exists_multiset_roots, Finset.max_le_iff, Ideal.mem_leadingCoeffNth, Monotone.withBot_map, preimage_coe_Iio, Polynomial.degree_C_lt, Polynomial.degree_C_mul_X_pow_le, Polynomial.degree_intCast_le, Polynomial.div_eq_zero_iff, image_coe_Iic, Nat.WithBot.lt_zero_iff, Polynomial.exists_degree_le_of_mem_span, bot_covBy_coe, image_coe_Ioc, Order.krullDim_le_one_iff_of_boundedOrder, Polynomial.eraseLead_degree_le, OrderIso.withBotCongr_refl, Polynomial.degree_X_sub_C_le, preimage_coe_Ici, Polynomial.degree_C_mul_X_le, preimage_coe_Ico, Ideal.height_le_ringKrullDim_quotient_add_encard, Polynomial.degree_wronskian_lt_add, orderSucc_bot, pred_coe_of_not_isMin, Nat.WithBot.one_le_iff_zero_lt, Polynomial.degree_one_le, Polynomial.tendsto_nhds_iff, succ_unbot, ringKrullDim_quotient_succ_le_of_nonZeroDivisor, OrderIso.withBotCongr_apply, strictMono_iff, Cubic.degree_of_a_eq_zero, map_le_iff, Cubic.equiv_symm_apply_b, ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial, instIsEmptySuccOrderOfNonempty, Polynomial.Splits.splits, minpoly.IsIntegrallyClosed.degree_le_of_ne_zero, Polynomial.degree_prod_le, OrderEmbedding.withBotCoe_apply, Polynomial.div_eq_quo_add_rem_div, BoxIntegral.Box.withBotCoe_subset_iff, Polynomial.degree_zero_le, Polynomial.Monic.degree_pos_of_not_isUnit, Polynomial.isBoundedUnder_abs_atBot_iff, Order.one_le_krullDim_iff, Order.krullDim_le_of_strictMono, Polynomial.degree_pos_of_not_isUnit_of_dvd_monic, ringKrullDim_le_iff_isMaximal_height_le, strictMono_map_iff, ringKrullDim_le_ringKrullDim_add_card, Lagrange.degree_interpolate_le, CategoryTheory.projectiveDimension_le_iff, minpoly.min, Module.supportDim_le_ringKrullDim, Polynomial.mem_closure_X_union_C, Module.supportDim_le_supportDim_quotSMulTop_succ, addLECancellable_iff_ne_bot, CategoryTheory.projectiveDimension_ge_iff, WithBotTop.coe_monotone, Polynomial.degree_multiset_prod_le, ringKrullDim_lt_top, List.not_maximum_lt_of_mem', CategoryTheory.injectiveDimension_lt_iff, List.le_maximum_of_mem', Polynomial.degree_sub_le, preimage_coe_Icc, Polynomial.ringKrullDim_le, Matrix.charpoly_sub_diagonal_degree_lt, Polynomial.degree_smul_le, Nat.WithBot.lt_one_iff_le_zero, Cubic.equiv_symm_apply_c, lt_coe_bot, Polynomial.degree_lt_degree, Polynomial.degree_le_iff_coeff_zero, orderSucc_coe, Polynomial.isBoundedUnder_abs_atTop_iff, Polynomial.card_roots, pred_coe_of_isMin, Polynomial.ofFn_degree_lt, subtypeOrderIso_apply_coe, Ico_coe, Order.krullDim_le_one_iff_forall_isMax, Order.krullDim_withBot, Order.krullDim_pos_iff_of_orderTop, Polynomial.degree_modByMonic_lt, instMulPosReflectLT, Polynomial.degree_lt_iff_coeff_zero, Polynomial.div_tendsto_atBot_zero_iff_degree_lt, Icc_coe, div_eq_quo_add_rem_div_add_rem_div, Polynomial.degree_le_zero_iff, coe_mono, Order.krullDim_pos_iff_of_orderBot, Polynomial.degree_add_le, preimage_coe_Iic, List.maximum_mono, Polynomial.degree_pos_of_aeval_root, Order.coheight_coe_withBot, Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson, Ioo_coe, Polynomial.le_degree_of_ne_zero, Cubic.equiv_apply_coe, Polynomial.le_degree_of_mem_supp, Polynomial.degree_annIdealGenerator_le_of_mem, Ico_coe_coe, height_le_ringKrullDim_quotient_add_spanFinrank, Polynomial.abs_isBoundedUnder_iff, instMulPosReflectLE, Polynomial.natDegree_eq_zero_iff_degree_le_zero, Polynomial.degree_sub_lt, PowerSeries.isWeierstrassDivisionAt_iff, Polynomial.degree_update_le, coeOrderHom_apply, ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial, Polynomial.Sequence.degree_strictMono, Ioo_coe_coe, Polynomial.degree_pos_of_irreducible, Cubic.degree_of_b_eq_zero', Order.KrullDimLE.krullDim_le, forall_le_coe_iff_le, ringKrullDim_le_ringKrullDim_add_spanFinrank, Polynomial.degree_cubic_le, OrderIso.withBotCongr_trans, Cubic.equiv_symm_apply_d, Ioo_bot_coe, Polynomial.degree_div_le, Irreducible.degree_le_two, Polynomial.degree_linear_le, forall_coe_le_iff_le, preimage_coe_Ioc_bot, Order.krullDim_nonneg, Polynomial.degree_linear_lt_degree_C_mul_X_sq, Polynomial.degree_cyclotomic_pos, WithZero.toMulBot_le, preimage_coe_Ioi_bot, Polynomial.degree_pos_of_eval₂_root, Polynomial.degree_quadratic_lt_degree_C_mul_X_cb, denselyOrdered_set_iff_subsingleton, Cubic.degree_of_c_eq_zero, Cubic.equiv_symm_apply_a, Order.krullDim_le_one_iff_forall_isMin, Order.height_coe_withBot, Polynomial.natDegree_pos_iff_degree_pos, Polynomial.degree_mod_lt, Ioc_coe_coe, IsDiscreteValuationRing.toWithBotNat_le_toWithBotNat_iff, Polynomial.mem_degreeLE, CategoryTheory.Retract.projectiveDimension_le, Polynomial.degree_sum_fin_lt, succ_eq_succ, coe_covBy_coe, Polynomial.degree_map_lt, Ideal.height_le_ringKrullDim_of_ne_top, Cubic.degree_of_c_eq_zero', Polynomial.natDegree_le_iff_degree_le, Polynomial.Sequence.basis_degree_strictMono, succ_strictMono, instPosMulReflectLT, List.le_maximum_of_length_pos_iff, exists_coe_lt, LaurentPolynomial.degree_T_le, Polynomial.div_tendsto_atTop_zero_iff_degree_lt, ringKrullDim_le_of_surjective, image_coe_Icc, Nat.WithBot.coe_nonneg, ringKrullDim_le_ringKrullDim_quotSMulTop_succ, Module.supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes, OrderEmbedding.withBotMap_apply, Polynomial.degree_erase_le, Module.supportDim_le_of_surjective, le_coe_unbotD, Finset.le_max, IsWellOrder.gt, Icc_coe_coe, Polynomial.degree_derivative_le, Order.bot_lt_krullDim_iff, Polynomial.mem_degreeLT, Polynomial.Monic.degree_le_zero_iff_eq_one, preimage_coe_Ioo_bot, PowerBasis.dim_le_degree_of_root, Ici_coe, trichotomous.lt, WithZero.toMulBot_strictMono, one_le_iff_pos, Icc_bot_coe, LaurentPolynomial.degree_C_le, Polynomial.degree_list_sum_le, Polynomial.degree_linear_lt, coe_strictMono, Polynomial.degree_natCast_le, Polynomial.degree_modByMonic_le_left, ringKrullDim_le_ringKrullDim_quotient_add_encard, bot_wcovBy_coe, Order.krullDimLE_iff, Polynomial.exists_mul_add_mul_eq_C_resultant, Polynomial.roots_def, LaurentPolynomial.degree_C_mul_T_le, WithTop.eq_bot_iff_forall_le, degree_radical_le, Polynomial.degree_gcd_le_right, Polynomial.degree_C_le, add_one_le_iff, OrderIso.withBotCongr_symm, preimage_coe_Ioo
instTop 📖	CompOp	18 math math: Order.krullDim_of_noMaxOrder, Order.krullDim_eq_top, coe_eq_top, eq_top_iff_forall_ge, Order.krullDim_int, Interval.dual_top, top_eq_coe, NonemptyInterval.coe_top_interval, Order.krullDim_enat, Interval.coe_top, sInf_empty, Finset.max_eq_top, ringKrullDim_lt_top, WithBotTop.rec_top, coe_top, Order.krullDim_of_noMinOrder, Order.krullDim_nat, Order.krullDim_eq_top_iff
instUniqueOfIsEmpty 📖	CompOp	—
lattice 📖	CompOp	12 math math: LatticeHom.withTopWithBot_apply, LatticeHom.coe_withTopWithBot, LatticeHom.withTopWithBot_id, LatticeHom.withTopWithBot_comp, LatticeHom.withTopWithBot'_toFun, LatticeHom.withBot_id, LatticeHom.withBot_toFun, LatticeHom.withTopWithBot_toFun, LatticeHom.withBot_comp, LatticeHom.withBot'_toFun, LatticeHom.coe_withBot, LatticeHom.withBot_apply
linearOrder 📖	CompOp	1 math math: Finset.fold_max_add
map 📖	CompOp	54 math math: ofDual_map, LatticeHom.withTopWithBot_apply, map_ofNat, map_eq_one_iff, map_eq_natCast_iff, map_comm, LatticeHom.coe_withTopWithBot, Equiv.withBotCongr_apply, Finset.map_ofDual_max, ofNat_eq_map_iff, map_ofDual, map_eq_zero_iff, monotone_map_iff, OrderHom.withBotMap_coe, toDual_map, StrictMono.withBot_map, map_bot, Finset.map_toDual_max, map₂_coe_left, map_natCast, AddMonoidHom.withBotMap_apply, map_eq_some_iff, map_map, InfHom.withBot_toFun, natCast_eq_map_iff, map_one, Monotone.withBot_map, map_add, some_eq_map_iff, map_eq_bot_iff, LatticeHom.withTopWithBot_toFun, OrderIso.withBotCongr_apply, map_le_iff, WithTop.ofDual_map, SupHom.withBot_toFun, map_comp_map, strictMono_map_iff, map_eq_ofNat_iff, comp_map, zero_eq_map_iff, map₂_coe_right, map_injective, ZeroHom.withBotMap_apply, LatticeHom.coe_withBot, WithTop.toDual_map, map_coe, OneHom.withBotMap_apply, map_id, OrderEmbedding.withBotMap_apply, map_zero, AddHom.withBotMap_apply, LatticeHom.withBot_apply, map_toDual, one_eq_map_iff
map₂ 📖	CompOp	7 math math: map₂_eq_bot_iff, map₂_coe_left, map₂_bot_left, mul_def, map₂_coe_right, map₂_bot_right, map₂_coe_coe
ofDual 📖	CompOp	20 math math: coe_toDualTopEquiv_eq, ofDual_map, lt_ofDual_iff, WithTop.lt_toDual_iff, WithTop.le_toDual_iff, ofDual_le_iff, map_ofDual, ofDual_apply_coe, WithTop.toDual_lt_iff, ofDual_lt_iff, ofDual_lt_ofDual_iff, ofDual_symm_apply, WithTop.toDual_symm_apply, WithTop.toDual_symm, ofDual_bot, le_ofDual_iff, ofDual_symm, WithTop.toDual_le_iff, ofDual_le_ofDual_iff, ofDual_apply_bot
semilatticeInf 📖	CompOp	6 math math: coe_inf, coe_min, InfHom.withBot_toFun, InfHom.withBot'_toFun, InfHom.withBot_comp, InfHom.withBot_id
semilatticeSup 📖	CompOp	30 math math: Finset.max_union, List.maximum_cons, SupHom.withBot_id, Finset.max_pair, Finset.max_eq_sup_coe, Finset.fold_max_add, Finset.coe_sup', LatticeHom.withBot_toFun, WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis, Polynomial.degree_sum_le, Finset.coe_sup_of_nonempty, Finset.max_eq_sup_withBot, SupHom.withBot_comp, Polynomial.degree_add_le_of_le, SupHom.withBot_toFun, SupHom.withBot'_toFun, Polynomial.supDegree_eq_degree, Polynomial.degree_sub_le, Finset.max_insert, Polynomial.degree_sum_eq_of_disjoint, Polynomial.degree_add_le, Polynomial.degree_update_le, coe_max, coe_sup, AddMonoidAlgebra.supDegree_withBot_some_comp, Polynomial.degree_sub_le_of_le, Polynomial.degree_add_eq_of_leadingCoeff_add_ne_zero, List.maximum_concat, Finset.sup_of_mem, List.maximum_append
toDual 📖	CompOp	19 math math: WithTop.ofDual_symm, toDual_map, le_toDual_iff, toDual_bot, toDual_apply_bot, toDual_le_iff, toDual_apply_coe, toDual_lt_toDual_iff, lt_toDual_iff, WithTop.le_ofDual_iff, WithTop.ofDual_le_iff, toDual_lt_iff, toDual_le_toDual_iff, WithTop.ofDual_lt_iff, WithTop.ofDual_symm_apply, toDual_symm_apply, toDual_symm, WithTop.lt_ofDual_iff, map_toDual
unbot 📖	CompOp	18 math math: le_unbot_iff, unbotA_eq_unbot, unbot_eq_iff, eq_unbot_iff, coe_unbot, unbot_one, unbot_mono, unbot_lt_iff, unbot_zero, lt_unbot_iff, unbot_coe, succ_unbot, unbot_le_unbot, Equiv.withBotSubtypeNe_apply, unbot_le_unbot_iff, unbot_le_iff, unbot_lt_unbot, unbot_lt_unbot_iff
unbotA 📖	CompOp	7 math math: le_unbotA_iff, lt_unbotA_iff, unbotA_eq_unbot, unbotA_mono, le_unbotA, unbotA_lt_iff, unbotA_le_iff
unbotD 📖	CompOp	16 math math: List.getD_max?_eq_unbotD_maximum, unbotD_mono, lt_unbotD_iff, le_unbotD_iff, unbotD_bot, unbotD_lt_iff, unbotD_eq_iff, unbotD_zero_mul, unbotD_le_iff, unbotD_one, unbotD_zero, unbotD_coe, le_unbotD, unbotD_eq_unbotD_iff, le_coe_unbotD, unbotD_eq_self_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_lt_coe 📖	mathematical	—	WithBot instLT Bot.bot bot some	—	—
bot_lt_iff_ne_bot 📖	mathematical	—	WithBot instLT Bot.bot bot	—	—
bot_ne_coe 📖	—	—	—	—	—
canLift 📖	mathematical	—	CanLift WithBot some Bot.bot bot	—	coe_unbot
coe_eq_coe 📖	mathematical	—	some	—	—
coe_eq_top 📖	mathematical	—	some Top.top WithBot instTop	—	coe_eq_coe
coe_inf 📖	mathematical	—	some SemilatticeInf.toMin WithBot semilatticeInf	—	—
coe_inj 📖	mathematical	—	some	—	—
coe_injective 📖	mathematical	—	WithBot some	—	Option.some_injective
coe_le 📖	mathematical	—	WithBot instLE some	—	coe_le_coe
coe_le_coe 📖	mathematical	—	WithBot instLE some	—	—
coe_le_iff 📖	mathematical	—	WithBot instLE some	—	—
coe_lt_coe 📖	mathematical	—	WithBot instLT some	—	—
coe_max 📖	mathematical	—	some SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder WithBot semilatticeSup	—	—
coe_min 📖	mathematical	—	some SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithBot semilatticeInf	—	—
coe_mono 📖	mathematical	—	Monotone WithBot instPreorder some	—	coe_le_coe
coe_ne_bot 📖	—	—	—	—	—
coe_strictMono 📖	mathematical	—	StrictMono WithBot instPreorder some	—	coe_lt_coe
coe_sup 📖	mathematical	—	some SemilatticeSup.toMax WithBot semilatticeSup	—	—
coe_top 📖	mathematical	—	some Top.top WithBot instTop	—	—
coe_unbot 📖	mathematical	—	some unbot	—	—
comp_map 📖	mathematical	—	map	—	map_map
denselyOrdered 📖	mathematical	—	DenselyOrdered WithBot instLT	—	denselyOrdered_iff
denselyOrdered_iff 📖	mathematical	—	DenselyOrdered WithBot instLT	—	exists_between coe_lt_coe DenselyOrdered.dense
eq_bot_iff_forall_le 📖	mathematical	—	Bot.bot WithBot bot Preorder.toLE instPreorder some	—	eq_bot_iff_forall_ne not_isBot coe_le_coe
eq_bot_iff_forall_lt 📖	mathematical	—	Bot.bot WithBot bot Preorder.toLT instPreorder some	—	lt_irrefl
eq_bot_iff_forall_ne 📖	mathematical	—	Bot.bot WithBot bot	—	—
eq_of_forall_coe_le_iff 📖	—	WithBot Preorder.toLE instPreorder PartialOrder.toPreorder some	—	—	le_antisymm forall_coe_le_iff_le
eq_of_forall_le_coe_iff 📖	—	WithBot Preorder.toLE instPreorder PartialOrder.toPreorder some	—	—	le_antisymm forall_le_coe_iff_le
eq_top_iff_forall_ge 📖	mathematical	—	Top.top WithBot WithTop instTop WithTop.top Preorder.toLE instPreorder WithTop.instPreorder PartialOrder.toPreorder some WithTop.some	—	—
eq_unbot_iff 📖	mathematical	—	unbot some	—	—
exists 📖	mathematical	—	Bot.bot WithBot bot some	—	—
exists_coe_le 📖	mathematical	—	WithBot Preorder.toLE instPreorder some	—	—
exists_coe_lt 📖	mathematical	—	WithBot Preorder.toLT instPreorder some	—	—
exists_ne_bot 📖	mathematical	—	some	—	—
forall 📖	mathematical	—	Bot.bot WithBot bot some	—	—
forall_coe_le 📖	mathematical	—	some	—	instIsEmptyFalse
forall_coe_le_iff_le 📖	mathematical	—	WithBot Preorder.toLE instPreorder some	—	not_isBot le_rfl LE.le.trans'
forall_coe_lt 📖	mathematical	—	some	—	instIsEmptyFalse
forall_le_coe_iff_le 📖	mathematical	—	WithBot Preorder.toLE instPreorder some	—	le_rfl LE.le.trans
forall_ne_bot 📖	mathematical	—	some	—	—
ge_of_forall_gt_iff_ge 📖	mathematical	—	WithBot Preorder.toLE instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder some	—	instIsEmptyFalse
instWellFoundedGT 📖	mathematical	—	WellFoundedGT WithBot instLT	—	instIsEmptyFalse wellFounded_gt
instWellFoundedLT 📖	mathematical	—	WellFoundedLT WithBot instLT	—	instIsEmptyFalse coe_lt_coe wellFounded_lt
le_bot_iff 📖	mathematical	—	WithBot instLE Bot.bot bot	—	—
le_coe_iff 📖	mathematical	—	WithBot instLE some	—	—
le_coe_unbotD 📖	mathematical	—	WithBot Preorder.toLE instPreorder some unbotD	—	—
le_def 📖	mathematical	—	WithBot instLE Bot.bot bot some	—	le_def_aux
le_def' 📖	mathematical	—	WithBot instLE Bot.bot bot some	—	—
le_def_aux 📖	mathematical	—	LE Bot.bot WithBot bot some	—	—
le_iff_forall 📖	mathematical	—	WithBot instLE some	—	instIsEmptyFalse
le_ofDual_iff 📖	mathematical	—	WithTop WithTop.instLE DFunLike.coe Equiv WithBot OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual instLE OrderDual.instLE WithTop.toDual	—	—
le_of_forall_lt_iff_le 📖	mathematical	—	WithBot Preorder.toLE instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder some	—	—
le_toDual_iff 📖	mathematical	—	WithTop OrderDual WithTop.instLE OrderDual.instLE DFunLike.coe Equiv WithBot EquivLike.toFunLike Equiv.instEquivLike toDual instLE WithTop.ofDual	—	—
le_unbotA 📖	mathematical	WithBot Preorder.toLE instPreorder PartialOrder.toPreorder some	unbotA	—	le_unbotD
le_unbotA_iff 📖	mathematical	—	unbotA WithBot instLE some	—	le_unbotD_iff
le_unbotD 📖	mathematical	WithBot Preorder.toLE instPreorder PartialOrder.toPreorder some	unbotD	—	le_unbotD_iff ne_bot_of_le_ne_bot
le_unbotD_iff 📖	mathematical	—	unbotD WithBot instLE some	—	CanLift.prf canLift
le_unbot_iff 📖	mathematical	—	unbot WithBot instLE some	—	CanLift.prf canLift
lt_coe_bot 📖	mathematical	—	WithBot Preorder.toLT instPreorder some Bot.bot OrderBot.toBot Preorder.toLE bot	—	—
lt_coe_iff 📖	mathematical	—	WithBot instLT some	—	—
lt_def 📖	mathematical	—	WithBot instLT Bot.bot bot some	—	lt_def_aux
lt_def' 📖	mathematical	—	WithBot instLT some Bot.bot bot	—	—
lt_def_aux 📖	mathematical	—	LT Bot.bot WithBot bot some	—	—
lt_iff_exists 📖	mathematical	—	WithBot instLT some	—	instIsEmptyFalse
lt_iff_exists_coe 📖	mathematical	—	WithBot instLT some	—	—
lt_iff_exists_coe_btwn 📖	mathematical	—	WithBot Preorder.toLT instPreorder some	—	exists_between denselyOrdered lt_iff_exists_coe lt_trans
lt_iff_exists_coe_btwn' 📖	mathematical	—	WithBot Preorder.toLT instPreorder some	—	lt_iff_exists_coe_btwn
lt_ofDual_iff 📖	mathematical	—	WithTop WithTop.instLT DFunLike.coe Equiv WithBot OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual instLT OrderDual.instLT WithTop.toDual	—	—
lt_toDual_iff 📖	mathematical	—	WithTop OrderDual WithTop.instLT OrderDual.instLT DFunLike.coe Equiv WithBot EquivLike.toFunLike Equiv.instEquivLike toDual instLT WithTop.ofDual	—	—
lt_unbotA_iff 📖	mathematical	—	unbotA WithBot instLT some	—	lt_unbotD_iff
lt_unbotD_iff 📖	mathematical	—	unbotD WithBot instLT some	—	CanLift.prf canLift
lt_unbot_iff 📖	mathematical	—	unbot WithBot instLT some	—	CanLift.prf canLift
map_bot 📖	mathematical	—	map Bot.bot WithBot bot	—	—
map_coe 📖	mathematical	—	map some	—	—
map_comm 📖	mathematical	—	map some	—	Option.map_comm
map_comp_map 📖	mathematical	—	WithBot map	—	—
map_eq_bot_iff 📖	mathematical	—	map Bot.bot WithBot bot	—	—
map_eq_some_iff 📖	mathematical	—	map some	—	—
map_id 📖	mathematical	—	map WithBot	—	—
map_injective 📖	mathematical	—	WithBot map	—	—
map_le_iff 📖	mathematical	Preorder.toLE	WithBot instPreorder map	—	—
map_map 📖	mathematical	—	map	—	—
map_ofDual 📖	mathematical	—	map DFunLike.coe Equiv WithBot OrderDual WithTop EquivLike.toFunLike Equiv.instEquivLike ofDual OrderDual.ofDual	—	—
map_toDual 📖	mathematical	—	map OrderDual DFunLike.coe Equiv WithBot WithTop EquivLike.toFunLike Equiv.instEquivLike toDual OrderDual.toDual	—	—
map₂_bot_left 📖	mathematical	—	map₂ Bot.bot WithBot bot	—	—
map₂_bot_right 📖	mathematical	—	map₂ Bot.bot WithBot bot	—	—
map₂_coe_coe 📖	mathematical	—	map₂ some	—	—
map₂_coe_left 📖	mathematical	—	map₂ some map	—	—
map₂_coe_right 📖	mathematical	—	map₂ some map	—	—
map₂_eq_bot_iff 📖	mathematical	—	map₂ Bot.bot WithBot bot	—	Option.map₂_eq_none_iff
monotone_iff 📖	mathematical	—	Monotone WithBot instPreorder some Preorder.toLE Bot.bot bot	—	Monotone.comp coe_mono bot_le forall le_rfl not_coe_le_bot coe_le_coe
monotone_map_iff 📖	mathematical	—	Monotone WithBot instPreorder map	—	monotone_iff
ne_bot_iff_exists 📖	mathematical	—	some	—	—
noMaxOrder 📖	mathematical	—	NoMaxOrder WithBot instLT	—	NoMaxOrder.exists_gt
noTopOrder 📖	mathematical	—	NoTopOrder WithBot instLE	—	NoTopOrder.exists_not_le
none_eq_bot 📖	mathematical	—	Bot.bot WithBot bot	—	—
nontrivial 📖	mathematical	—	Nontrivial WithBot	—	Option.nontrivial
not_coe_le_bot 📖	mathematical	—	WithBot instLE some Bot.bot bot	—	—
not_lt_bot 📖	mathematical	—	WithBot instLT Bot.bot bot	—	—
ofDual_apply_bot 📖	mathematical	—	DFunLike.coe Equiv WithBot OrderDual WithTop EquivLike.toFunLike Equiv.instEquivLike ofDual Bot.bot bot Top.top WithTop.top	—	ofDual_bot
ofDual_apply_coe 📖	mathematical	—	DFunLike.coe Equiv WithBot OrderDual WithTop EquivLike.toFunLike Equiv.instEquivLike ofDual some WithTop.some OrderDual.ofDual	—	—
ofDual_bot 📖	mathematical	—	DFunLike.coe Equiv WithBot OrderDual WithTop EquivLike.toFunLike Equiv.instEquivLike ofDual Bot.bot bot Top.top WithTop.top	—	—
ofDual_le_iff 📖	mathematical	—	WithTop WithTop.instLE DFunLike.coe Equiv WithBot OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual instLE OrderDual.instLE WithTop.toDual	—	—
ofDual_le_ofDual_iff 📖	mathematical	—	WithTop WithTop.instLE DFunLike.coe Equiv WithBot OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual instLE OrderDual.instLE	—	—
ofDual_lt_iff 📖	mathematical	—	WithTop WithTop.instLT DFunLike.coe Equiv WithBot OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual instLT OrderDual.instLT WithTop.toDual	—	—
ofDual_lt_ofDual_iff 📖	mathematical	—	WithTop WithTop.instLT DFunLike.coe Equiv WithBot OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual instLT OrderDual.instLT	—	—
ofDual_map 📖	mathematical	—	DFunLike.coe Equiv WithBot OrderDual WithTop EquivLike.toFunLike Equiv.instEquivLike ofDual map WithTop.map OrderDual.ofDual OrderDual.toDual	—	—
ofDual_symm 📖	mathematical	—	Equiv.symm WithBot OrderDual WithTop ofDual WithTop.toDual	—	—
ofDual_symm_apply 📖	mathematical	—	DFunLike.coe Equiv WithTop WithBot OrderDual EquivLike.toFunLike Equiv.instEquivLike Equiv.symm ofDual WithTop.toDual	—	—
some_eq_coe 📖	mathematical	—	some	—	—
some_eq_map_iff 📖	mathematical	—	some map	—	—
strictAnti_iff 📖	mathematical	—	StrictAnti WithBot instPreorder some Preorder.toLT Bot.bot bot	—	strictMono_iff
strictMono_iff 📖	mathematical	—	StrictMono WithBot instPreorder some Preorder.toLT Bot.bot bot	—	StrictMono.comp coe_strictMono bot_lt_coe forall lt_irrefl not_lt_bot coe_lt_coe
strictMono_map_iff 📖	mathematical	—	StrictMono WithBot instPreorder map	—	strictMono_iff
toDual_apply_bot 📖	mathematical	—	DFunLike.coe Equiv WithBot WithTop OrderDual EquivLike.toFunLike Equiv.instEquivLike toDual Bot.bot bot Top.top WithTop.top	—	toDual_bot
toDual_apply_coe 📖	mathematical	—	DFunLike.coe Equiv WithBot WithTop OrderDual EquivLike.toFunLike Equiv.instEquivLike toDual some WithTop.some OrderDual.toDual	—	—
toDual_bot 📖	mathematical	—	DFunLike.coe Equiv WithBot WithTop OrderDual EquivLike.toFunLike Equiv.instEquivLike toDual Bot.bot bot Top.top WithTop.top	—	—
toDual_le_iff 📖	mathematical	—	WithTop OrderDual WithTop.instLE OrderDual.instLE DFunLike.coe Equiv WithBot EquivLike.toFunLike Equiv.instEquivLike toDual instLE WithTop.ofDual	—	—
toDual_le_toDual_iff 📖	mathematical	—	WithTop OrderDual WithTop.instLE OrderDual.instLE DFunLike.coe Equiv WithBot EquivLike.toFunLike Equiv.instEquivLike toDual instLE	—	—
toDual_lt_iff 📖	mathematical	—	WithTop OrderDual WithTop.instLT OrderDual.instLT DFunLike.coe Equiv WithBot EquivLike.toFunLike Equiv.instEquivLike toDual instLT WithTop.ofDual	—	—
toDual_lt_toDual_iff 📖	mathematical	—	WithTop OrderDual WithTop.instLT OrderDual.instLT DFunLike.coe Equiv WithBot EquivLike.toFunLike Equiv.instEquivLike toDual instLT	—	—
toDual_map 📖	mathematical	—	DFunLike.coe Equiv WithBot WithTop OrderDual EquivLike.toFunLike Equiv.instEquivLike toDual map WithTop.map OrderDual.toDual OrderDual.ofDual	—	—
toDual_symm 📖	mathematical	—	Equiv.symm WithBot WithTop OrderDual toDual WithTop.ofDual	—	—
toDual_symm_apply 📖	mathematical	—	DFunLike.coe Equiv WithTop OrderDual WithBot EquivLike.toFunLike Equiv.instEquivLike Equiv.symm toDual WithTop.ofDual	—	—
top_eq_coe 📖	mathematical	—	Top.top WithBot instTop some	—	coe_eq_coe
total_le 📖	mathematical	—	WithBot instLE	—	—
unbotA_eq_unbot 📖	mathematical	—	unbotA unbot	—	—
unbotA_le_iff 📖	mathematical	—	unbotA WithBot instLE some	—	CanLift.prf canLift
unbotA_lt_iff 📖	mathematical	—	unbotA WithBot instLT some	—	CanLift.prf canLift
unbotA_mono 📖	mathematical	WithBot instLE	unbotA	—	unbotD_mono
unbotD_bot 📖	mathematical	—	unbotD Bot.bot WithBot bot	—	—
unbotD_coe 📖	mathematical	—	unbotD some	—	—
unbotD_eq_iff 📖	mathematical	—	unbotD some Bot.bot WithBot bot	—	—
unbotD_eq_self_iff 📖	mathematical	—	unbotD some Bot.bot WithBot bot	—	—
unbotD_eq_unbotD_iff 📖	mathematical	—	unbotD some Bot.bot WithBot bot	—	—
unbotD_le_iff 📖	mathematical	—	unbotD WithBot instLE some	—	—
unbotD_lt_iff 📖	mathematical	—	unbotD WithBot instLT some	—	—
unbotD_mono 📖	mathematical	WithBot instLE	unbotD	—	CanLift.prf canLift
unbot_coe 📖	mathematical	WithBot some Bot.bot bot coe_ne_bot	unbot	—	—
unbot_eq_iff 📖	mathematical	—	unbot some	—	—
unbot_le_iff 📖	mathematical	—	unbot WithBot instLE some	—	CanLift.prf canLift
unbot_le_unbot 📖	mathematical	—	unbot WithBot instLE	—	unbot_le_unbot_iff
unbot_le_unbot_iff 📖	mathematical	—	unbot WithBot instLE	—	coe_unbot
unbot_lt_iff 📖	mathematical	—	unbot WithBot instLT some	—	CanLift.prf canLift
unbot_lt_unbot 📖	mathematical	—	unbot WithBot instLT	—	unbot_lt_unbot_iff
unbot_lt_unbot_iff 📖	mathematical	—	unbot WithBot instLT	—	coe_unbot
unbot_mono 📖	mathematical	WithBot instLE	unbot	—	unbot_le_unbot_iff

WithBot.IsWellOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gt 📖	mathematical	—	IsWellOrder WithBot Preorder.toLT WithBot.instPreorder	—	WithBot.trichotomous.gt IsWellOrder.toTrichotomous instIsTransGt WithBot.instWellFoundedGT IsWellOrder.toIsWellFounded
lt 📖	mathematical	—	IsWellOrder WithBot Preorder.toLT WithBot.instPreorder	—	WithBot.trichotomous.lt IsWellOrder.toTrichotomous instIsTransLt WithBot.instWellFoundedLT IsWellOrder.toIsWellFounded

WithBot.trichotomous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gt 📖	mathematical	—	WithBot Preorder.toLT WithBot.instPreorder	—	Std.Trichotomous.swap lt
lt 📖	mathematical	—	WithBot Preorder.toLT WithBot.instPreorder	—	—

WithTop

Definitions

Name	Category	Theorems
decidableEq 📖	CompOp	6 math math: mul_def, top_mul', Finset.min_mem_image_coe, MeasureTheory.stoppedValue_stoppedProcess, mul_top', Finset.min_mem_insert_top_image_coe
decidableLE 📖	CompOp	—
decidableLT 📖	CompOp	1 math math: HahnSeries.SummableFamily.powers_toFun
distribLattice 📖	CompOp	—
instBot 📖	CompOp	5 math math: coe_eq_bot, coe_bot, Finset.min_eq_bot, bot_eq_coe, eq_bot_iff_forall_le
instBoundedOrder 📖	CompOp	6 math math: LatticeHom.withTopWithBot_apply, LatticeHom.coe_withTopWithBot, LatticeHom.withTopWithBot_id, LatticeHom.withTopWithBot_comp, LatticeHom.withTopWithBot'_toFun, LatticeHom.withTopWithBot_toFun
instLE 📖	CompOp	60 math math: WithBot.coe_toDualTopEquiv_eq, WithBot.add_le_add_iff_right', toDualBotEquiv_coe, WithBotTop.coe_le_coe, le_toDual_iff, le_def, WithBot.ofDual_le_iff, untop_le_untop_iff, addLECancellable_coe, instOrderedSub, le_iff_forall, coe_le_zero, orderIsoSumLexPUnit_toLex, orderIsoSumLexPUnit_symm_inl, WithBot.le_toDual_iff, toDualBotEquiv_symm_top, existsAddOfLE, orderIsoSumLexPUnit_top, zeroLEOneClass, WithBot.toDualTopEquiv_coe, coe_le_iff, not_top_le_coe, WithBot.toDual_le_iff, ofDual_le_ofDual_iff, noBotOrder, WithBot.toDualTopEquiv_symm_bot, le_coe_iff, untop_le_iff, WithBot.toDualTopEquiv_symm_coe, coe_le_one, toDual_le_toDual_iff, le_ofDual_iff, WithBot.le_ofDual_iff, le_untop_iff, toDualBotEquiv_symm_coe, ofDual_le_iff, WithBot.toDualTopEquiv_bot, untopA_le_iff, WithBot.toDual_le_toDual_iff, coe_nonneg, le_untopD_iff, total_le, addRightMono, orderIsoSumLexPUnit_symm_inr, top_le_iff, one_le_coe, coe_le_coe, le_def', IsMin.withTop, addLeftMono, toDual_le_iff, le_coe, addLECancellable_of_ne_top, le_untopA_iff, add_le_add_iff_left, WithBot.ofDual_le_ofDual_iff, coe_toDualBotEquiv, toDualBotEquiv_top, untopD_le_iff, add_le_add_iff_right
instLT 📖	CompOp	47 math math: lt_def, instWellFoundedGT, WithBot.lt_ofDual_iff, lt_untopD_iff, denselyOrdered, untopA_lt_iff, lt_toDual_iff, coe_lt_top, lt_def', not_top_lt, one_lt_top, one_lt_coe, add_lt_top, ofDual_lt_ofDual_iff, toDual_lt_iff, lt_untop_iff, addLeftReflectLT, addRightReflectLT, WithBot.ofDual_lt_iff, untopD_lt_iff, WithBot.toDual_lt_toDual_iff, WithBot.ofDual_lt_ofDual_iff, toDual_lt_toDual_iff, coe_lt_one, denselyOrdered_iff, coe_lt_coe, lt_iff_exists, WithBot.lt_toDual_iff, natCast_lt_top, untop_lt_iff, lt_untopA_iff, add_lt_add_iff_right, coe_lt_iff, instWellFoundedLT, WithBot.toDual_lt_iff, noMinOrder, ofDual_lt_iff, untop_lt_untop_iff, top_pos, coe_pos, lt_ofDual_iff, WithBotTop.coe_lt_coe, sum_lt_top, add_lt_add_iff_left, lt_top_iff_ne_top, coe_lt_zero, lt_iff_exists_coe
instOrderBot 📖	CompOp	—
instOrderTop 📖	CompOp	10 math math: Finset.coe_inf', Finset.min_eq_inf_withTop, untrop_sum, trop_iInf, Finset.coe_inf_of_nonempty, Finset.untrop_sum, Finset.inf_of_mem, untrop_sum_eq_sInf_image, AddMonoidAlgebra.infDegree_withTop_some_comp, trop_sInf_image
instPartialOrder 📖	CompOp	2 math math: isOrderedAddMonoid, instIsOrderedRing
instPreorder 📖	CompOp	221 math math: MeasureTheory.IsStoppingTime.measurableSet_inter_le_iff, tendsto_zero_iff_meromorphicOrderAt_pos, pred_eq_pred, HahnSeries.orderTop_single_le, WithBotTop.coe_strictMono, coe_mono, Ico_coe_coe, OrderIso.withTopCongr_apply, OrderIso.withTopCongr_refl, tendsto_cobounded_iff_meromorphicOrderAt_neg, pred_untop, lt_iff_exists_coe_btwn', MeasureTheory.hittingAfter_bot_le_iff, MeasureTheory.IsStoppingTime.measurableSet, MeasureTheory.IsStoppingTime.measurableSet_gt, Field.Emb.Cardinal.directed_filtration, IsWellOrder.gt, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, Ioc_coe_coe, List.minimum_of_length_pos_le_iff, Field.Emb.Cardinal.instInverseSystemWithTopToTypeOrdRankAlgHomSubtypeMemIntermediateFieldCoeOrderEmbeddingFiltrationAlgebraicClosureEmbFunctor, Ico_coe_top, HahnSeries.orderTop_sub_pos, MeromorphicNFAt.meromorphicOrderAt_nonneg_iff_analyticAt, Ici_coe, preimage_coe_Iio_top, MvPowerSeries.min_lexOrder_le, ENat.monotone_map_iff, pow_right_strictMono, MeasureTheory.hittingAfter_mono, eq_top_iff_forall_gt, Ioo_coe_top, IsWellOrder.lt, exists_le_coe, MeasureTheory.IsStoppingTime.measurableSet_ge', MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable, HahnSeries.le_orderTop_of_leadingCoeff_eq, TopologicalSpace.instOrderTopologyWithTop, MeasureTheory.IsStoppingTime.measurableSet_lt_of_isLUB, preimage_coe_Ici, le_minSmoothness, image_coe_Ioc, MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time, ENat.map_natCast_strictMono, IsContDiffImplicitAt.one_le, image_coe_Ioo, WithBot.eq_top_iff_forall_ge, preimage_coe_Iio, preimage_coe_Ioc, FiniteMulArchimedeanClass.withTopOrderIso_apply_coe, Icc_coe_coe, OrderIso.withTopCongr_trans, untop₀_nonneg, meromorphicOrderAt_add, monotone_map_iff, strictMono_map_iff, Ioo_coe_coe, Ioo_coe, MeasureTheory.IsStoppingTime.measurableSet_inter_le_const_iff, Finset.min_le, HahnSeries.zero_lt_orderTop_of_order, MvPowerSeries.le_lexOrder_iff, OrderEmbedding.withTopCoe_apply, HahnSeries.addVal_le_of_coeff_ne_zero, Order.height_coe_withTop, preimage_coe_Ico, MeasureTheory.IsStoppingTime.measurableSet_lt, Monotone.withTop_map, AnalyticAt.meromorphicOrderAt_nonneg, MeasureTheory.IsStoppingTime.measurableSet_lt_of_pred, Iic_coe, image_coe_Ico, MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable', MeasureTheory.IsStoppingTime.measurableSet_le, lt_iff_exists_coe_btwn, coe_covBy_top, tendsto_nhds_iff_meromorphicOrderAt_nonneg, OrderIso.withTopCongr_symm, coe_covBy_coe, HahnSeries.lt_orderTop_single, Padic.AddValuation.map_add, HahnSeries.orderTop_le_of_coeff_ne_zero, Order.krullDim_WithTop, FiniteMulArchimedeanClass.withTopOrderIso_symm_apply, meromorphicNFAt_iff_analyticAt_or, Associates.factors_le, MeasureTheory.IsStoppingTime.measurableSet_ge, eq_top_iff_forall_ge, Field.Emb.Cardinal.equivSucc_coherence, subtypeOrderIso_symm_apply, iSup_coe_lt_top, image_coe_Iic, HahnSeries.orderTop_lt_top, ge_of_forall_gt_iff_ge, Order.coheight_coe_withTop, ENat.one_le_iff_ne_zero_withTop, MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable, pred_mono, HahnSeries.unit_aux, orderPred_coe, Iio_coe, MeasureTheory.hittingAfter_apply_anti, Associates.factors_mono, OrderEmbedding.withTopMap_apply, iInf_coe_lt_top, MeasureTheory.measurableSet_preimage_stoppedValue_inter, image_coe_Ici, pred_strictMono, ENat.LEInfty.out, image_coe_Ioi, tangentBundleCore.isContMDiff, orderPred_top, pow_lt_top_iff, coe_wcovBy_top, MeasureTheory.stoppedProcess_eq'', MeasureTheory.IsStoppingTime.measurableSet_le', TangentBundle.contMDiffVectorBundle, preimage_coe_Iic, MeasureTheory.IsStoppingTime.measurableSet_lt_le, image_coe_Iio, Field.Emb.Cardinal.filtration_apply, MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_le_const, HahnSeries.orderTop_nsmul_le_orderTop_pow, HahnSeries.archimedeanClassOrderIsoWithTop_apply, Ioi_coe, Ioc_coe, forall_coe_le_iff_le, MeasureTheory.stoppedProcess_eq_of_mem_finset, isGLB_sInf, MeasureTheory.IsStoppingTime.measurableSet_inter_le, preimage_coe_Ioo, map_le_iff, Ico_coe, strictAnti_iff, HahnSeries.orderTop_add_le_mul, forall_le_coe_iff_le, MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable_range, WithBotTop.coe_monotone, hahnEmbedding_isOrderedModule_rat, HahnModule.orderTop_vAdd_le_orderTop_smul, Finset.le_min_iff, coeOrderHom_apply, HahnSeries.orderTop_le_orderTop_smul, HahnSeries.orderTop_lt_iff_exists, canonicallyOrderedAdd, FiniteArchimedeanClass.withTopOrderIso_symm_apply, MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable_range', coe_strictMono, trichotomous.lt, List.minimum_anti, HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff, MeasureTheory.IsStoppingTime.measurableSet_stopping_time_le_min, preimage_coe_Ioi, isLUB_sSup, exists_lt_coe, ENat.map_natCast_nonneg, Icc_coe, MeasureTheory.IsStoppingTime.measurableSet_gt', HahnSeries.SummableFamily.powers_toFun, coe_untopD_le, HahnSeries.orderTop_self_sub_one_pos_iff, HahnSeries.min_orderTop_le_orderTop_sub, MeasureTheory.hittingAfter_le_iff, instIsEmptyPredOrderOfNonempty, denselyOrdered_set_iff_subsingleton, subtypeOrderIso_apply_coe, ENat.strictMono_map_iff, coe_wcovBy_coe, monotone_iff, List.minimum_le_of_mem', MeasureTheory.hittingAfter_apply_mono, MeasureTheory.le_hittingAfter, succ_coe_of_isMax, le_of_forall_lt_iff_le, Ioc_coe_top, HahnSeries.zero_lt_orderTop_iff, tendsto_nhds_top_iff, MeasureTheory.hittingAfter_le_of_mem, coe_top_lt, Finset.min_mono, succ_coe, MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable_range, preimage_coe_Ioo_top, HahnSeries.zero_le_orderTop_iff, MvPowerSeries.lexOrder_le_of_coeff_ne_zero, OrderHom.withTopMap_coe, strictMono_iff, HahnSeries.orderTop_smul_not_lt, trichotomous.gt, Icc_coe_top, OrderIso.withTopCongr_symm_apply, image_coe_Icc, untop₀_le_untop₀_iff, List.minimum_le_coe_iff, preimage_coe_Icc, Associates.prod_le, MvPowerSeries.le_lexOrder_mul, HahnSeries.mem_orderTopSubOnePos_iff, minSmoothness_monotone, MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable', MeasureTheory.hittingAfter_anti, MeasureTheory.IsStoppingTime.measurableSet_stopping_time_le, preimage_coe_Ico_top, HahnSeries.min_orderTop_le_orderTop_add, addLECancellable_iff_ne_top, MeasureTheory.hittingAfter_lt_iff, MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_le, succ_coe_of_not_isMax, List.not_lt_minimum_of_mem', FiniteArchimedeanClass.withTopOrderIso_apply_coe, MeasureTheory.IsStoppingTime.measurableSet_lt', range_coe, le_of_untop₀_le_untop₀, HahnSeries.le_orderTop_iff_forall, isLUB_sSup', MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable_range', hahnEmbedding_isOrderedAddMonoid, MvPowerSeries.lexOrder_mul_ge, StrictMono.withTop_map, eq_bot_iff_forall_le, hahnEmbedding_isOrderedModule
instUniqueOfIsEmpty 📖	CompOp	—
lattice 📖	CompOp	12 math math: LatticeHom.withTopWithBot_apply, LatticeHom.coe_withTopWithBot, LatticeHom.withTopWithBot_id, LatticeHom.withTopWithBot_comp, LatticeHom.withTopWithBot'_toFun, LatticeHom.withTop_apply, LatticeHom.withTop_toFun, LatticeHom.withTop'_toFun, LatticeHom.coe_withTop, LatticeHom.withTopWithBot_toFun, LatticeHom.withTop_comp, LatticeHom.withTop_id
linearOrder 📖	CompOp	7 math math: untrop_sum, Tropical.add_eq_zero_iff, trop_iInf, Finset.untrop_sum, untrop_sum_eq_sInf_image, trop_sInf_image, List.trop_minimum
map 📖	CompOp	59 math math: WithBot.ofDual_map, map_ofDual, LatticeHom.withTopWithBot_apply, OneHom.withTopMap_apply, OrderIso.withTopCongr_apply, one_eq_map_iff, LatticeHom.coe_withTopWithBot, map₂_coe_right, AddHom.withTopMap_apply, map_eq_top_iff, ZeroHom.withTopMap_apply, map_id, map_ofNat, monotone_map_iff, strictMono_map_iff, map_sub, LatticeHom.withTop_apply, AddMonoidHom.withTopMap_apply, WithBot.toDual_map, Monotone.withTop_map, LatticeHom.withTop_toFun, map_zero, map_eq_natCast_iff, ENat.toENNRealOrderEmbedding_apply, map₂_coe_left, Equiv.withTopCongr_apply, Finset.map_toDual_min, map_injective, LatticeHom.coe_withTop, natCast_eq_map_iff, SupHom.withTop_toFun, OrderEmbedding.withTopMap_apply, InfHom.withTop_toFun, LatticeHom.withTopWithBot_toFun, map_comp_map, ofDual_map, map_toDual, comp_map, map_eq_some_iff, map_eq_one_iff, map_eq_ofNat_iff, map_le_iff, ofNat_eq_map_iff, map_eq_zero_iff, MonoidWithZeroHom.withTopMap_apply, zero_eq_map_iff, map_comm, some_eq_map_iff, map_top, map_natCast, toDual_map, Finset.map_ofDual_min, OrderHom.withTopMap_coe, map_map, map_coe, HahnSeries.orderTop_embDomain, map_one, StrictMono.withTop_map, map_add
map₂ 📖	CompOp	7 math math: mul_def, map₂_coe_right, map₂_coe_left, map₂_top_left, map₂_top_right, map₂_eq_top_iff, map₂_coe_coe
ofDual 📖	CompOp	20 math math: map_ofDual, ofDual_symm, ofDual_apply_top, WithBot.le_toDual_iff, ofDual_lt_ofDual_iff, ofDual_apply_coe, WithBot.toDual_le_iff, ofDual_le_ofDual_iff, ofDual_map, WithBot.lt_toDual_iff, le_ofDual_iff, ofDual_le_iff, WithBot.toDual_lt_iff, ofDual_lt_iff, ofDual_symm_apply, WithBot.toDual_symm_apply, WithBot.toDual_symm, ofDual_top, lt_ofDual_iff, coe_toDualBotEquiv
semilatticeInf 📖	CompOp	47 math math: MeasureTheory.IsStoppingTime.measurableSet_inter_le_iff, Finset.coe_inf', MeasureTheory.stoppedProcess_stoppedProcess, Finset.min_eq_inf_withTop, meromorphicOrderAt_add_of_ne, MvPowerSeries.min_lexOrder_le, Finset.min_union, untop₀_min, MeasureTheory.IsStoppingTime.min, meromorphicOrderAt_add, MeasureTheory.IsStoppingTime.measurableSet_inter_le_const_iff, MeasureTheory.stoppedProcess_eq_stoppedValue_apply, List.minimum_append, MeasureTheory.IsStoppingTime.measurableSet_eq_stopping_time_min, Padic.AddValuation.map_add, MeasureTheory.stoppedValue_stoppedProcess_apply, MeasureTheory.Martingale.stoppedValue_min_ae_eq_condExp, List.minimum_cons, MeasureTheory.stoppedValue_stoppedProcess, InfHom.withTop_toFun, MeasureTheory.IsStoppingTime.measurableSpace_min, MeasureTheory.IsStoppingTime.measurableSet_min_iff, InfHom.withTop'_toFun, Finset.min_pair, MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_le_const, MeasureTheory.IsStoppingTime.measurableSpace_min_const, Finset.coe_inf_of_nonempty, MeasureTheory.IsStoppingTime.measurableSet_inter_le, MeasureTheory.IsStoppingTime.min_const, Finset.inf_of_mem, MeasureTheory.progMeasurable_min_stopping_time, InfHom.withTop_id, MeasureTheory.stoppedProcess_stoppedProcess', MeasureTheory.IsStoppingTime.measurableSet_stopping_time_le_min, Finset.min_insert, HahnSeries.min_orderTop_le_orderTop_sub, MeasureTheory.stoppedValue_stoppedProcess_ae_eq, List.minimum_concat, coe_min, MeasureTheory.IsStoppingTime.measurableSet_min_const_iff, coe_inf, AddMonoidAlgebra.infDegree_withTop_some_comp, Associates.FactorSet.sup_add_inf_eq_add, HahnSeries.min_orderTop_le_orderTop_add, MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_le, InfHom.withTop_comp, MeasureTheory.stoppedProcess_eq_stoppedValue
semilatticeSup 📖	CompOp	10 math math: coe_max, coe_sup, SupHom.withTop'_toFun, untop₀_max, SupHom.withTop_toFun, MeasureTheory.IsStoppingTime.max, SupHom.withTop_id, Associates.FactorSet.sup_add_inf_eq_add, MeasureTheory.IsStoppingTime.max_const, SupHom.withTop_comp
toDual 📖	CompOp	19 math math: WithBot.lt_ofDual_iff, toDual_top, lt_toDual_iff, le_toDual_iff, WithBot.ofDual_le_iff, toDual_lt_iff, toDual_apply_top, WithBot.ofDual_lt_iff, toDual_lt_toDual_iff, WithBot.ofDual_symm_apply, toDual_symm_apply, map_toDual, toDual_symm, toDual_le_toDual_iff, WithBot.le_ofDual_iff, WithBot.ofDual_symm, toDual_map, toDual_le_iff, toDual_apply_coe
untop 📖	CompOp	22 math math: HahnSeries.untop_orderTop_of_ne_zero, pred_untop, untop_eq_iff, untop_le_untop_iff, untop_coe, tendsto_untop, coe_untop, untop_zero, HahnSeries.coeff_untop_eq_leadingCoeff, untopA_eq_untop, lt_untop_iff, HahnSeries.leadingCoeff_of_ne, untop_le_iff, untop_lt_iff, le_untop_iff, eq_untop_iff, untop_mono, untop_lt_untop_iff, untop_one, Equiv.withTopSubtypeNe_apply, continuous_untop, HahnSeries.leadingCoeff_of_ne_zero
untopA 📖	CompOp	19 math math: untopA_lt_iff, MeasureTheory.hittingAfter_mem_set, MeasureTheory.stoppedProcess_eq_of_ge, untopA_eq_untop, MeasureTheory.isStoppingTime_hittingBtwn_isStoppingTime, measurable_untopA, tendsto_untopA, MeasureTheory.progMeasurable_min_stopping_time, untopA_mono, MeasureTheory.stoppedValue_sub_eq_sum, MeasureTheory.hittingAfter_mem_set_of_ne_top, lt_untopA_iff, untopA_le_iff, MeasureTheory.isStoppingTime_hitting_isStoppingTime, untopA_le, continuousOn_untopA, le_untopA_iff, MeasureTheory.Adapted.isStoppingTime_hittingBtwn_isStoppingTime, Measurable.untopA
untopD 📖	CompOp	22 math math: lt_untopD_iff, continuousOn_untopD, untopD_coe_enat, untopD_top, untopD_zero_mul, untopD_mono, untopD_zero, List.getD_min?_eq_untopD_minimum, untopD_lt_iff, untopD_eq_iff, untopD_le, tendsto_untopD, coe_untopD_le, le_untopD_iff, untopD_one, untopD_eq_untopD_iff, measurable_untopD, Measurable.untopD, untopD_add, untopD_coe, untopD_le_iff, untopD_eq_self_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_eq_coe 📖	mathematical	—	Bot.bot WithTop instBot some	—	coe_eq_coe
canLift 📖	mathematical	—	CanLift WithTop some Top.top top	—	coe_untop
coe_bot 📖	mathematical	—	some Bot.bot WithTop instBot	—	—
coe_eq_bot 📖	mathematical	—	some Bot.bot WithTop instBot	—	coe_eq_coe
coe_eq_coe 📖	mathematical	—	some	—	—
coe_inf 📖	mathematical	—	some SemilatticeInf.toMin WithTop semilatticeInf	—	—
coe_inj 📖	mathematical	—	some	—	—
coe_injective 📖	mathematical	—	WithTop some	—	Option.some_injective
coe_le_coe 📖	mathematical	—	WithTop instLE some	—	le_def' coe_ne_top
coe_le_iff 📖	mathematical	—	WithTop instLE some	—	le_iff_forall
coe_lt_coe 📖	mathematical	—	WithTop instLT some	—	lt_def' coe_ne_top
coe_lt_iff 📖	mathematical	—	WithTop instLT some	—	lt_iff_exists
coe_lt_top 📖	mathematical	—	WithTop instLT some Top.top top	—	lt_def' top_ne_coe
coe_max 📖	mathematical	—	some SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop semilatticeSup	—	—
coe_min 📖	mathematical	—	some SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop semilatticeInf	—	—
coe_mono 📖	mathematical	—	Monotone WithTop instPreorder some	—	coe_le_coe
coe_ne_top 📖	—	—	—	—	—
coe_strictMono 📖	mathematical	—	StrictMono WithTop instPreorder some	—	coe_lt_coe
coe_sup 📖	mathematical	—	some SemilatticeSup.toMax WithTop semilatticeSup	—	—
coe_top_lt 📖	mathematical	—	WithTop Preorder.toLT instPreorder some Top.top OrderTop.toTop Preorder.toLE top	—	coe_lt_top coe_lt_coe not_top_lt coe_ne_top
coe_untop 📖	mathematical	—	some untop	—	—
coe_untopD_le 📖	mathematical	—	WithTop Preorder.toLE instPreorder some untopD	—	le_top le_refl
comp_map 📖	mathematical	—	map	—	map_map
denselyOrdered 📖	mathematical	—	DenselyOrdered WithTop instLT	—	denselyOrdered_iff
denselyOrdered_iff 📖	mathematical	—	DenselyOrdered WithTop instLT	—	exists_between coe_lt_coe DenselyOrdered.dense
eq_bot_iff_forall_le 📖	mathematical	—	Bot.bot WithTop WithBot instBot WithBot.bot Preorder.toLE instPreorder WithBot.instPreorder PartialOrder.toPreorder some WithBot.some	—	bot_le top_le_iff coe_ne_top coe_eq_bot WithBot.eq_bot_iff_forall_le coe_le_coe
eq_of_forall_coe_le_iff 📖	—	WithTop Preorder.toLE instPreorder PartialOrder.toPreorder some	—	—	ge_antisymm forall_coe_le_iff_le
eq_of_forall_le_coe_iff 📖	—	WithTop Preorder.toLE instPreorder PartialOrder.toPreorder some	—	—	ge_antisymm forall_le_coe_iff_le
eq_top_iff_forall_ge 📖	mathematical	—	Top.top WithTop top Preorder.toLE instPreorder some	—	le_top eq_top_iff_forall_ne not_isTop coe_le_coe
eq_top_iff_forall_gt 📖	mathematical	—	Top.top WithTop top Preorder.toLT instPreorder some	—	coe_lt_top coe_ne_top coe_lt_coe lt_irrefl
eq_top_iff_forall_ne 📖	mathematical	—	Top.top WithTop top	—	—
eq_untop_iff 📖	mathematical	—	untop some	—	coe_ne_top
exists 📖	mathematical	—	Top.top WithTop top some	—	—
exists_le_coe 📖	mathematical	—	WithTop Preorder.toLE instPreorder some	—	exists top_le_iff coe_ne_top coe_le_coe
exists_lt_coe 📖	mathematical	—	WithTop Preorder.toLT instPreorder some	—	exists not_top_lt coe_lt_coe
exists_ne_top 📖	mathematical	—	some	—	ne_top_iff_exists exists_exists_eq_and
forall 📖	mathematical	—	Top.top WithTop top some	—	—
forall_coe_le_iff_le 📖	mathematical	—	WithTop Preorder.toLE instPreorder some	—	le_top top_le_iff eq_top_iff_forall_ge le_rfl LE.le.trans'
forall_le_coe 📖	mathematical	—	some	—	forall top_le_iff coe_ne_top IsEmpty.forall_iff instIsEmptyFalse coe_le_coe
forall_le_coe_iff_le 📖	mathematical	—	WithTop Preorder.toLE instPreorder some	—	top_le_iff eq_top_iff_forall_ge coe_le_coe le_top not_isTop le_rfl LE.le.trans
forall_lt_coe 📖	mathematical	—	some	—	forall not_top_lt IsEmpty.forall_iff instIsEmptyFalse coe_lt_coe
forall_ne_top 📖	mathematical	—	some	—	ne_top_iff_exists
ge_of_forall_gt_iff_ge 📖	mathematical	—	WithTop Preorder.toLE instPreorder PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder some	—	coe_lt_top le_top le_refl coe_le_coe top_le_iff coe_ne_top not_le NoMaxOrder.exists_gt coe_lt_coe forall_lt_imp_le_iff_le_of_dense
instWellFoundedGT 📖	mathematical	—	WellFoundedGT WithTop instLT	—	not_top_lt IsEmpty.forall_iff instIsEmptyFalse coe_lt_coe wellFounded_gt
instWellFoundedLT 📖	mathematical	—	WellFoundedLT WithTop instLT	—	forall not_top_lt IsEmpty.forall_iff instIsEmptyFalse coe_lt_coe wellFounded_lt coe_lt_top
le_coe 📖	mathematical	—	WithTop instLE some	—	coe_le_coe
le_coe_iff 📖	mathematical	—	WithTop instLE some	—	le_iff_forall
le_def 📖	mathematical	—	WithTop instLE Top.top top some	—	—
le_def' 📖	mathematical	—	WithTop instLE Top.top top some	—	WithBot.le_def
le_iff_forall 📖	mathematical	—	WithTop instLE some	—	le_def' top_ne_coe IsEmpty.forall_iff instIsEmptyFalse coe_ne_top
le_ofDual_iff 📖	mathematical	—	WithBot WithBot.instLE DFunLike.coe Equiv WithTop OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual instLE OrderDual.instLE WithBot.toDual	—	bot_le le_top WithBot.le_bot_iff WithBot.coe_ne_bot top_le_iff coe_ne_top WithBot.coe_le_coe coe_le_coe OrderDual.le_toDual
le_of_forall_lt_iff_le 📖	mathematical	—	WithTop Preorder.toLE instPreorder PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder some	—	not_top_lt top_le_iff coe_ne_top le_refl coe_le_coe IsEmpty.forall_iff instIsEmptyFalse le_top coe_lt_coe not_lt not_le NoMaxOrder.exists_gt forall_gt_imp_ge_iff_le_of_dense
le_toDual_iff 📖	mathematical	—	WithBot OrderDual WithBot.instLE OrderDual.instLE DFunLike.coe Equiv WithTop EquivLike.toFunLike Equiv.instEquivLike toDual instLE WithBot.ofDual	—	bot_le le_top WithBot.le_bot_iff WithBot.coe_ne_bot top_le_iff coe_ne_top WithBot.coe_le_coe OrderDual.le_toDual coe_le_coe
le_untopA_iff 📖	mathematical	—	untopA WithTop instLE some	—	CanLift.prf canLift coe_le_coe
le_untopD_iff 📖	mathematical	—	untopD WithTop instLE some	—	le_top coe_le_coe
le_untop_iff 📖	mathematical	—	untop WithTop instLE some	—	CanLift.prf canLift coe_le_coe
lt_def 📖	mathematical	—	WithTop instLT some Top.top top	—	—
lt_def' 📖	mathematical	—	WithTop instLT Top.top top some	—	WithBot.lt_def
lt_iff_exists 📖	mathematical	—	WithTop instLT some	—	lt_def' top_ne_coe IsEmpty.forall_iff instIsEmptyFalse coe_ne_top
lt_iff_exists_coe 📖	mathematical	—	WithTop instLT some	—	not_top_lt top_ne_coe
lt_iff_exists_coe_btwn 📖	mathematical	—	WithTop Preorder.toLT instPreorder some	—	lt_iff_exists_coe_btwn'
lt_iff_exists_coe_btwn' 📖	mathematical	—	WithTop Preorder.toLT instPreorder some	—	exists_between' denselyOrdered lt_iff_exists_coe gt_trans
lt_ofDual_iff 📖	mathematical	—	WithBot WithBot.instLT DFunLike.coe Equiv WithTop OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual instLT OrderDual.instLT WithBot.toDual	—	WithBot.not_lt_bot not_top_lt WithBot.bot_lt_coe coe_lt_top WithBot.coe_lt_coe coe_lt_coe OrderDual.lt_toDual
lt_toDual_iff 📖	mathematical	—	WithBot OrderDual WithBot.instLT OrderDual.instLT DFunLike.coe Equiv WithTop EquivLike.toFunLike Equiv.instEquivLike toDual instLT WithBot.ofDual	—	WithBot.not_lt_bot not_top_lt WithBot.bot_lt_coe coe_lt_top WithBot.coe_lt_coe OrderDual.lt_toDual coe_lt_coe
lt_top_iff_ne_top 📖	mathematical	—	WithTop instLT Top.top top	—	not_top_lt coe_lt_top coe_ne_top
lt_untopA_iff 📖	mathematical	—	untopA WithTop instLT some	—	CanLift.prf canLift coe_lt_coe
lt_untopD_iff 📖	mathematical	—	untopD WithTop instLT some	—	coe_lt_top coe_lt_coe
lt_untop_iff 📖	mathematical	—	untop WithTop instLT some	—	CanLift.prf canLift coe_lt_coe
map_coe 📖	mathematical	—	map some	—	—
map_comm 📖	mathematical	—	map some	—	Option.map_comm
map_comp_map 📖	mathematical	—	WithTop map	—	—
map_eq_some_iff 📖	mathematical	—	map some	—	—
map_eq_top_iff 📖	mathematical	—	map Top.top WithTop top	—	—
map_id 📖	mathematical	—	map WithTop	—	—
map_injective 📖	mathematical	—	WithTop map	—	—
map_le_iff 📖	mathematical	Preorder.toLE	WithTop instPreorder map	—	le_refl le_top top_le_iff coe_ne_top coe_le_coe
map_map 📖	mathematical	—	map	—	—
map_ofDual 📖	mathematical	—	map DFunLike.coe Equiv WithTop OrderDual WithBot EquivLike.toFunLike Equiv.instEquivLike ofDual OrderDual.ofDual	—	—
map_toDual 📖	mathematical	—	map OrderDual DFunLike.coe Equiv WithTop WithBot EquivLike.toFunLike Equiv.instEquivLike toDual OrderDual.toDual	—	—
map_top 📖	mathematical	—	map Top.top WithTop top	—	—
map₂_coe_coe 📖	mathematical	—	map₂ some	—	—
map₂_coe_left 📖	mathematical	—	map₂ some map	—	—
map₂_coe_right 📖	mathematical	—	map₂ some map	—	—
map₂_eq_top_iff 📖	mathematical	—	map₂ Top.top WithTop top	—	Option.map₂_eq_none_iff
map₂_top_left 📖	mathematical	—	map₂ Top.top WithTop top	—	—
map₂_top_right 📖	mathematical	—	map₂ Top.top WithTop top	—	—
monotone_iff 📖	mathematical	—	Monotone WithTop instPreorder some Preorder.toLE Top.top top	—	Monotone.comp coe_mono le_top forall le_rfl not_top_le_coe coe_le_coe
monotone_map_iff 📖	mathematical	—	Monotone WithTop instPreorder map	—	monotone_iff coe_le_coe le_top
ne_top_iff_exists 📖	mathematical	—	some	—	—
noBotOrder 📖	mathematical	—	NoBotOrder WithTop instLE	—	top_le_iff coe_ne_top NoBotOrder.exists_not_ge coe_le_coe
noMinOrder 📖	mathematical	—	NoMinOrder WithTop instLT	—	coe_lt_top NoMinOrder.exists_lt coe_lt_coe
none_eq_top 📖	mathematical	—	Top.top WithTop top	—	—
nontrivial 📖	mathematical	—	Nontrivial WithTop	—	Option.nontrivial
not_top_le_coe 📖	mathematical	—	WithTop instLE Top.top top some	—	le_def' coe_ne_top top_ne_coe
not_top_lt 📖	mathematical	—	WithTop instLT Top.top top	—	lt_def' top_ne_coe
ofDual_apply_coe 📖	mathematical	—	DFunLike.coe Equiv WithTop OrderDual WithBot EquivLike.toFunLike Equiv.instEquivLike ofDual some WithBot.some OrderDual.ofDual	—	—
ofDual_apply_top 📖	mathematical	—	DFunLike.coe Equiv WithTop OrderDual WithBot EquivLike.toFunLike Equiv.instEquivLike ofDual Top.top top Bot.bot WithBot.bot	—	ofDual_top
ofDual_le_iff 📖	mathematical	—	WithBot WithBot.instLE DFunLike.coe Equiv WithTop OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual instLE OrderDual.instLE WithBot.toDual	—	bot_le le_top WithBot.le_bot_iff WithBot.coe_ne_bot top_le_iff coe_ne_top WithBot.coe_le_coe coe_le_coe OrderDual.toDual_le
ofDual_le_ofDual_iff 📖	mathematical	—	WithBot WithBot.instLE DFunLike.coe Equiv WithTop OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual instLE OrderDual.instLE	—	bot_le le_top WithBot.le_bot_iff WithBot.coe_ne_bot top_le_iff coe_ne_top WithBot.coe_le_coe OrderDual.ofDual_le_ofDual coe_le_coe
ofDual_lt_iff 📖	mathematical	—	WithBot WithBot.instLT DFunLike.coe Equiv WithTop OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual instLT OrderDual.instLT WithBot.toDual	—	WithBot.not_lt_bot not_top_lt WithBot.bot_lt_coe coe_lt_top WithBot.coe_lt_coe coe_lt_coe OrderDual.toDual_lt
ofDual_lt_ofDual_iff 📖	mathematical	—	WithBot WithBot.instLT DFunLike.coe Equiv WithTop OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual instLT OrderDual.instLT	—	WithBot.not_lt_bot not_top_lt WithBot.bot_lt_coe coe_lt_top WithBot.coe_lt_coe OrderDual.ofDual_lt_ofDual coe_lt_coe
ofDual_map 📖	mathematical	—	DFunLike.coe Equiv WithTop OrderDual WithBot EquivLike.toFunLike Equiv.instEquivLike ofDual map WithBot.map OrderDual.ofDual OrderDual.toDual	—	—
ofDual_symm 📖	mathematical	—	Equiv.symm WithTop OrderDual WithBot ofDual WithBot.toDual	—	—
ofDual_symm_apply 📖	mathematical	—	DFunLike.coe Equiv WithBot WithTop OrderDual EquivLike.toFunLike Equiv.instEquivLike Equiv.symm ofDual WithBot.toDual	—	—
ofDual_top 📖	mathematical	—	DFunLike.coe Equiv WithTop OrderDual WithBot EquivLike.toFunLike Equiv.instEquivLike ofDual Top.top top Bot.bot WithBot.bot	—	—
some_eq_coe 📖	mathematical	—	some	—	—
some_eq_map_iff 📖	mathematical	—	some map	—	top_ne_coe
strictAnti_iff 📖	mathematical	—	StrictAnti WithTop instPreorder some Preorder.toLT Top.top top	—	strictMono_iff
strictMono_iff 📖	mathematical	—	StrictMono WithTop instPreorder some Preorder.toLT Top.top top	—	StrictMono.comp coe_strictMono coe_lt_top forall lt_irrefl not_top_lt coe_lt_coe
strictMono_map_iff 📖	mathematical	—	StrictMono WithTop instPreorder map	—	strictMono_iff coe_lt_coe coe_lt_top
toDual_apply_coe 📖	mathematical	—	DFunLike.coe Equiv WithTop WithBot OrderDual EquivLike.toFunLike Equiv.instEquivLike toDual some WithBot.some OrderDual.toDual	—	—
toDual_apply_top 📖	mathematical	—	DFunLike.coe Equiv WithTop WithBot OrderDual EquivLike.toFunLike Equiv.instEquivLike toDual Top.top top Bot.bot WithBot.bot	—	toDual_top
toDual_le_iff 📖	mathematical	—	WithBot OrderDual WithBot.instLE OrderDual.instLE DFunLike.coe Equiv WithTop EquivLike.toFunLike Equiv.instEquivLike toDual instLE WithBot.ofDual	—	bot_le le_top WithBot.le_bot_iff WithBot.coe_ne_bot top_le_iff coe_ne_top WithBot.coe_le_coe OrderDual.toDual_le coe_le_coe
toDual_le_toDual_iff 📖	mathematical	—	WithBot OrderDual WithBot.instLE OrderDual.instLE DFunLike.coe Equiv WithTop EquivLike.toFunLike Equiv.instEquivLike toDual instLE	—	bot_le le_top WithBot.le_bot_iff WithBot.coe_ne_bot top_le_iff coe_ne_top WithBot.coe_le_coe OrderDual.toDual_le_toDual coe_le_coe
toDual_lt_iff 📖	mathematical	—	WithBot OrderDual WithBot.instLT OrderDual.instLT DFunLike.coe Equiv WithTop EquivLike.toFunLike Equiv.instEquivLike toDual instLT WithBot.ofDual	—	WithBot.not_lt_bot not_top_lt WithBot.bot_lt_coe coe_lt_top WithBot.coe_lt_coe OrderDual.toDual_lt coe_lt_coe
toDual_lt_toDual_iff 📖	mathematical	—	WithBot OrderDual WithBot.instLT OrderDual.instLT DFunLike.coe Equiv WithTop EquivLike.toFunLike Equiv.instEquivLike toDual instLT	—	WithBot.not_lt_bot not_top_lt WithBot.bot_lt_coe coe_lt_top WithBot.coe_lt_coe OrderDual.toDual_lt_toDual coe_lt_coe
toDual_map 📖	mathematical	—	DFunLike.coe Equiv WithTop WithBot OrderDual EquivLike.toFunLike Equiv.instEquivLike toDual map WithBot.map OrderDual.toDual OrderDual.ofDual	—	—
toDual_symm 📖	mathematical	—	Equiv.symm WithTop WithBot OrderDual toDual WithBot.ofDual	—	—
toDual_symm_apply 📖	mathematical	—	DFunLike.coe Equiv WithBot OrderDual WithTop EquivLike.toFunLike Equiv.instEquivLike Equiv.symm toDual WithBot.ofDual	—	—
toDual_top 📖	mathematical	—	DFunLike.coe Equiv WithTop WithBot OrderDual EquivLike.toFunLike Equiv.instEquivLike toDual Top.top top Bot.bot WithBot.bot	—	—
top_le_iff 📖	mathematical	—	WithTop instLE Top.top top	—	not_top_le_coe coe_ne_top le_top
top_ne_coe 📖	—	—	—	—	—
total_le 📖	mathematical	—	WithTop instLE	—	—
untopA_eq_untop 📖	mathematical	—	untopA untop	—	—
untopA_le 📖	mathematical	WithTop Preorder.toLE instPreorder PartialOrder.toPreorder some	untopA	—	untopD_le
untopA_le_iff 📖	mathematical	—	untopA WithTop instLE some	—	untopD_le_iff
untopA_lt_iff 📖	mathematical	—	untopA WithTop instLT some	—	untopD_lt_iff
untopA_mono 📖	mathematical	WithTop instLE	untopA	—	untopD_mono
untopD_coe 📖	mathematical	—	untopD some	—	—
untopD_eq_iff 📖	mathematical	—	untopD some Top.top WithTop top	—	top_ne_coe coe_ne_top
untopD_eq_self_iff 📖	mathematical	—	untopD some Top.top WithTop top	—	untopD_eq_iff
untopD_eq_untopD_iff 📖	mathematical	—	untopD some Top.top WithTop top	—	untopD_eq_self_iff top_ne_coe untopD_eq_iff coe_ne_top
untopD_le 📖	mathematical	WithTop Preorder.toLE instPreorder PartialOrder.toPreorder some	untopD	—	untopD_le_iff ne_top_of_le_ne_top coe_ne_top
untopD_le_iff 📖	mathematical	—	untopD WithTop instLE some	—	CanLift.prf canLift coe_le_coe
untopD_lt_iff 📖	mathematical	—	untopD WithTop instLT some	—	CanLift.prf canLift coe_lt_coe
untopD_mono 📖	mathematical	WithTop instLE	untopD	—	CanLift.prf canLift top_le_iff coe_ne_top coe_le_coe
untopD_top 📖	mathematical	—	untopD Top.top WithTop top	—	—
untop_coe 📖	mathematical	WithTop some Top.top top coe_ne_top	untop	—	—
untop_eq_iff 📖	mathematical	—	untop some	—	top_ne_coe
untop_le_iff 📖	mathematical	—	untop WithTop instLE some	—	CanLift.prf canLift coe_le_coe
untop_le_untop_iff 📖	mathematical	—	untop WithTop instLE	—	untop_le_iff coe_untop
untop_lt_iff 📖	mathematical	—	untop WithTop instLT some	—	CanLift.prf canLift coe_lt_coe
untop_lt_untop_iff 📖	mathematical	—	untop WithTop instLT	—	untop_lt_iff coe_untop
untop_mono 📖	mathematical	WithTop instLE	untop	—	untop_le_untop_iff

WithTop.IsWellOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gt 📖	mathematical	—	IsWellOrder WithTop Preorder.toLT WithTop.instPreorder	—	WithTop.trichotomous.gt IsWellOrder.toTrichotomous instIsTransGt WithTop.instWellFoundedGT IsWellOrder.toIsWellFounded
lt 📖	mathematical	—	IsWellOrder WithTop Preorder.toLT WithTop.instPreorder	—	WithTop.trichotomous.lt IsWellOrder.toTrichotomous instIsTransLt WithTop.instWellFoundedLT IsWellOrder.toIsWellFounded

WithTop.trichotomous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gt 📖	mathematical	—	WithTop Preorder.toLT WithTop.instPreorder	—	Std.Trichotomous.swap lt
lt 📖	mathematical	—	WithTop Preorder.toLT WithTop.instPreorder	—	—

(root)

Definitions

Name	Category	Theorems
WithBot 📖	CompOp	829 math math: Polynomial.degree_map_le, WithBot.coe_toDualTopEquiv_eq, Polynomial.modByMonic_eq_self_iff, WithBot.ofDual_map, WithTop.map_ofDual, WithBot.mul_bot', WithBot.add_le_add_iff_right', IsAlgClosed.roots_eq_zero_iff_degree_nonpos, WittVector.RecursionMain.succNthDefiningPoly_degree, LaurentPolynomial.degree_C_mul_T_ite, WithBot.coe_eq_one, LatticeHom.withTopWithBot_apply, Polynomial.degree_mul_le, Order.LTSeries.length_le_krullDim, Polynomial.exists_degree_le_of_mem_span_of_finite, WithBot.instPosMulStrictMono, WithBot.lt_ofDual_iff, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim, Finset.max_union, Order.krullDim_le_of_strictComono_and_surj, WithBot.le_unbotA_iff, NonemptyInterval.mem_coe_interval, ringKrullDim_succ_le_ringKrullDim_polynomial, Order.krullDim_of_noMaxOrder, WithBot.coe_le_zero, WithTop.toDualBotEquiv_coe, WithBot.le_unbot_iff, NonemptyInterval.coe_inv_interval, WithBot.sum_eq_bot_iff, WithBot.addRightMono, WithBot.not_coe_le_bot, WithBot.zeroLEOneClass, Order.krullDim_lt_coe_iff, WithBot.orderIsoPUnitSumLex_symm_inl, Polynomial.coe_lt_degree, CategoryTheory.Retract.injectiveDimension_le, Polynomial.degree_le_degree, WithTop.toDual_top, BoxIntegral.Box.splitUpper_eq_bot, WithBot.coe_inf, WithBot.lt_iff_exists_coe_btwn, WithBot.addLeftMono, WithBot.trichotomous.gt, NonemptyInterval.coe_neg_interval, Polynomial.MonicDegreeEq.degree, List.maximum_cons, CategoryTheory.injectiveDimension_le_iff, WithBot.subtypeOrderIso_symm_apply, Lagrange.degree_basisDivisor_self, WithBot.coe_lt_one, WithBot.lt_unbotA_iff, Cubic.degree_of_b_eq_zero, Polynomial.degree_quadratic_lt, WithBot.instMulPosMono, Module.supportDim_eq_bot_iff_subsingleton, WithTop.ofDual_symm, WithBot.map_eq_one_iff, Polynomial.degree_pow_le, Order.krullDim_nonneg_iff, WithBot.map_eq_natCast_iff, Ring.krullDimLE_iff, ringKrullDim_eq_one_iff_of_isLocalRing_isDomain, BoxIntegral.Box.coe_bot, WithBot.eq_bot_iff_forall_ne, Polynomial.zero_le_degree_iff, WithBot.eq_bot_iff_forall_lt, Polynomial.Sequence.degree_eq', Polynomial.degree_pow, Polynomial.mod_eq_self_iff, WithBot.le_of_forall_lt_iff_le, WithTop.lt_toDual_iff, WithBot.range_coe, SupHom.withBot_id, PowerSeries.degree_weierstrassMod_lt, Polynomial.degree_eq_natDegree, LatticeHom.coe_withTopWithBot, Polynomial.degree_gcd_le_left, Order.krullDim_pos_iff, WithTop.le_toDual_iff, Order.krullDim_le_one_iff, Equiv.withBotCongr_apply, Module.supportDim_add_length_eq_supportDim_of_isRegular, WithBot.ofDual_le_iff, BoxIntegral.Box.disjoint_withBotCoe, WithBot.coe_eq_zero, WithBot.image_coe_Ioo, Nat.WithBot.add_eq_two_iff, WithBot.orderIsoPUnitSumLex_symm_inr, WithBot.coe_injective, WithBot.noTopOrder, WithBot.lt_coe_iff, Polynomial.degree_le_of_dvd, LatticeHom.withTopWithBot_id, Polynomial.div_tendsto_zero_iff_degree_lt, Polynomial.degree_list_prod, BoxIntegral.Box.splitUpper_le, Polynomial.degree_lt_degree_mul_X, Polynomial.Splits.degree_le_one_of_irreducible, Polynomial.divByMonic_eq_zero_iff, Order.krullDim_eq_zero_of_unique, Order.le_krullDim_iff, NonemptyInterval.coe_sub_interval, Ordnode.Bounded.weak_left, NonemptyInterval.coe_one_interval, minpoly.degree_pos, WithBot.lt_add_one_iff, WithBot.coe_sInf', Polynomial.tendsto_atTop_iff_leadingCoeff_nonneg, Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map, WithBot.instUncountable, Polynomial.degree_list_prod_le, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson, WithBot.IsWellOrder.lt, Finset.max_mono, WithBot.add_le_add_iff_left, ringKrullDim_succ_le_ringKrullDim_powerseries, Lagrange.eq_interpolate_iff, WithBot.unbot_one, Order.krullDim_eq_top, LatticeHom.withTopWithBot_comp, WithBot.map_ofDual, WithBot.lt_succ, WithBot.one_lt_coe, Polynomial.degree_X_pow_add_C, Order.coheight_le_krullDim, Polynomial.degree_pos_of_root, Polynomial.degree_X_sub_C, WithBot.addLeftReflectLT, Order.krullDim_nonpos_iff_forall_isMax, WithBot.map_eq_zero_iff, PowerSeries.degree_trunc_lt, Polynomial.card_roots_map_le_degree, WithBot.add_coe_eq_bot_iff, NonemptyInterval.coe_nsmul_interval, Cubic.degree_of_a_eq_zero', MvPolynomial.degree_optionEquivLeft, WithBot.coe_eq_top, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim, IsMax.withBot, ringKrullDim_nonneg_of_nontrivial, WithBot.eq_top_iff_forall_ge, WithBot.Ioc_bot_coe, ringKrullDimZero_iff_ringKrullDim_eq_zero, LatticeHom.withTopWithBot'_toFun, WithBot.lt_unbotD_iff, WithBot.addLECancellable_of_ne_bot, Order.krullDim_nonpos_iff_forall_isMin, Finset.max_pair, WithBot.mul_coe_eq_bind, Polynomial.degree_mono, WithBot.coe_le_iff, Polynomial.Splits.degree_eq_card_roots, Polynomial.degree_C_lt_degree_C_mul_X, Polynomial.tendsto_atBot_iff_leadingCoeff_nonpos, List.coe_le_maximum_iff, WithBot.Ioi_coe, Cubic.degree_of_a_ne_zero', WithBot.ofDual_apply_coe, WithBot.monotone_map_iff, Module.supportDim_le_of_injective, Order.succ_eq_zero, Order.krullDim_int, Polynomial.degree_quadratic, WithBot.instPosMulReflectLE, NonemptyInterval.coe_pow_interval, WithBot.coe_addHom, OrderHom.withBotMap_coe, minpoly.degree_le, WithBot.le_unbotD_iff, NonemptyInterval.coe_add_interval, WithBot.image_coe_Ici, WithBot.Ico_bot_coe, Polynomial.abs_tendsto_atTop_iff, PowerSeries.IsWeierstrassDivisionAt.degree_lt, Polynomial.degree_lt_wf, Equiv.withBotSubtypeNe_symm_apply_coe, WithTop.ofDual_apply_top, WithBot.map₂_eq_bot_iff, WithBot.unbotD_bot, Polynomial.degree_cubic_lt, WithBot.strictAnti_iff, WithBot.le_coe_iff, Polynomial.degree_C, WithBot.ge_of_forall_gt_iff_ge, Order.height_le_krullDim, Finset.max_eq_sup_coe, WithBot.bot_add, WithBot.coe_le, Polynomial.degree_modByMonic_le, WithBot.succ_eq_bot, Polynomial.Splits.degree_eq_one_of_irreducible, NonemptyInterval.coe_div_interval, Polynomial.natDegree_lt_natDegree_iff, Matrix.charpoly_degree_eq_dim, CategoryTheory.injectiveDimension_ge_iff, WithBot.le_iff_forall, WithBot.toDual_map, OrderIso.withBotCongr_symm_apply, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_maximalIdeal, Polynomial.int_cyclotomic_rw, LaurentPolynomial.degree_C, Polynomial.degree_divX_lt, WithBot.unbot_lt_iff, WithBot.exists_coe_le, LatticeHom.withBot_id, Order.bot_lt_krullDim, Polynomial.degree_eraseLead_lt, WithBot.coe_pos, WithBot.instMulPosStrictMono, topologicalKrullDim_subspace_le, Polynomial.Chebyshev.degree_T, Polynomial.degree_X_pow_le, StrictMono.withBot_map, WithBot.succ_mono, topologicalKrullDim_zero_of_discreteTopology, ringKrullDim_quotient_le, WithBot.map_bot, WithBot.le_toDual_iff, Polynomial.degree_monomial_le, WithBot.pred_coe, Polynomial.natDegree_lt_iff_degree_lt, WithTop.ofDual_lt_ofDual_iff, Lagrange.degree_interpolate_erase_lt, WithBot.unbotD_lt_iff, ringKrullDim_succ_le_of_surjective, BoxIntegral.Box.splitLower_le, WithBot.toDual_bot, Finset.max_mem_image_coe, Finset.fold_max_add, IsDiscreteValuationRing.toWithBotNat_zero, Ideal.primeHeight_le_ringKrullDim, ringKrullDim_eq_bot_of_subsingleton, WithTop.toDualBotEquiv_symm_top, WithBot.unbot_zero, Polynomial.degree_quadratic_le, CategoryTheory.projectiveDimension_lt_iff, Equiv.withBotCongr_refl, Lagrange.degree_interpolate_lt, Finset.coe_sup', WithBot.preimage_coe_Ioc, WithBot.coe_min, WithBot.add_bot, WithBot.map_natCast, Polynomial.abs_tendsto_atBot_iff, Polynomial.degree_X_le, Polynomial.Sequence.degree_eq, WithBot.coe_wcovBy_coe, WithBot.top_eq_coe, WithTop.toDual_lt_iff, WithBot.coe_lt_zero, WithBot.zero_eq_coe, WithBot.preimage_coe_Ioi, AddMonoidHom.withBotMap_apply, Cubic.degree_of_d_ne_zero, ringKrullDim_le_iff_height_le, Polynomial.degree_derivative_lt, minpoly.degree_le_of_ne_zero, div_eq_quo_add_sum_rem_div, Polynomial.degree_freeMonic, Interval.coe_injective, PowerBasis.mem_span_pow', Finset.max_mem_insert_bot_image_coe, Nat.WithBot.add_eq_one_iff, WithBot.exists, LatticeHom.withBot_toFun, WithBot.add_le_add_iff_right, WithBot.lt_iff_exists_coe, Order.krullDim_nonpos_of_subsingleton, WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis, WithBot.Iio_coe, List.maximum_nil, Polynomial.degree_derivative_eq, WithZero.toMulBot_lt, WithBot.bot_lt_add, Module.ringKrullDim_quotient_add_one_of_mem_nonZeroDivisors, WithBot.unbotD_eq_iff, Polynomial.degree_erase_lt, WithBot.eq_bot_iff_forall_le, Order.krullDim_WithTop, IsInducing.topologicalKrullDim_le, Polynomial.degree_le_of_natDegree_le, InfHom.withBot_toFun, ringKrullDim_le_ringKrullDim_quotient_add_card, Polynomial.Splits.def, IsDiscreteValuationRing.bot_lt_toWithBotNat_iff, WithBot.succ_one, Nat.WithBot.add_eq_three_iff, WithBot.image_coe_Iio, Lagrange.degree_basisDivisor_of_ne, Ideal.height_le_ringKrullDim_quotient_add_one, WithBot.addLECancellable_coe, PowerBasis.degree_minpoly, WithBot.Iic_coe, Polynomial.splits_iff, WithBot.map₂_bot_left, Polynomial.degree_sum_le, Polynomial.degree_pos_of_ne_zero_of_nonunit, withBotSucc_zero, WithBot.toDual_apply_bot, Polynomial.degree_hermite, Irreducible.degree_pos, WithBot.image_coe_Ico, WithBot.Ioc_coe, WithBot.instPosMulMono, Lagrange.degree_nodal, Polynomial.Monic.degree_pos, Finset.coe_sup_of_nonempty, Polynomial.degree_multiset_prod_of_monic, Cubic.degree_of_d_eq_zero, WithBot.unbotD_zero_mul, WithBot.lt_iff_exists_coe_btwn', WithBot.toDualTopEquiv_coe, WithBot.bot_neg, Polynomial.degree_X_pow_sub_C, Polynomial.degree_le_natDegree, WithBot.natCast_eq_map_iff, WithBot.image_coe_Ioi, WithBot.monotone_iff, WithBot.range_eq, NonemptyInterval.coe_top_interval, Polynomial.degree_divByMonic_le, Polynomial.degree_le_mul_left, IsClosedEmbedding.topologicalKrullDim_le, ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank, WithBot.map_one, Polynomial.exists_multiset_roots, Finset.max_le_iff, Ideal.mem_leadingCoeffNth, Monotone.withBot_map, WithBot.bot_lt_natCast, Function.Embedding.coeWithBot_apply, WithBot.preimage_coe_Iio, Order.krullDim_enat, WithBot.lt_def, Finset.max_eq_sup_withBot, WithBot.bot_mul_bot, WithZero.toMulBot_coe_ofAdd, Polynomial.degree_C_lt, Polynomial.degree_C_mul_X_pow_le, WithBot.add_eq_coe, WithBot.instWellFoundedLT, WithTop.ofDual_apply_coe, BoxIntegral.Box.not_disjoint_coe_iff_nonempty_inter, Polynomial.degree_zero, WithTop.toDual_apply_top, Polynomial.rootOfSplits'_eq_rootOfSplits, Polynomial.degree_intCast_le, Polynomial.div_eq_zero_iff, Interval.coe_coe, WithBot.image_coe_Iic, BoxIntegral.Box.biUnion_coe_eq_coe, Nat.WithBot.lt_zero_iff, Polynomial.exists_degree_le_of_mem_span, List.maximum_eq_bot, WithBot.map_add, WithBot.bot_covBy_coe, WithBot.coe_le_coe, WithBot.charZero, Polynomial.Chebyshev.degree_U_of_ne_neg_one, WithBot.image_coe_Ioc, Finset.max_zero, WithBot.preimage_coe_bot, ringKrullDim_add_length_eq_ringKrullDim_of_isRegular, Order.krullDim_le_one_iff_of_boundedOrder, Polynomial.eraseLead_degree_le, Polynomial.degreeLT_succ_eq_degreeLE, OrderIso.withBotCongr_refl, WithBot.mul_def, WithBot.toDual_le_iff, WithBot.ofDual_lt_iff, Polynomial.degree_X_sub_C_le, WithBot.preimage_coe_Ici, Polynomial.degree_eq_iff_natDegree_eq_of_pos, Polynomial.degree_C_mul_X_le, WithBot.toDual_apply_coe, WithBot.preimage_coe_Ico, WithBot.toDual_lt_toDual_iff, Ideal.is_fg_degreeLE, Ideal.height_le_ringKrullDim_quotient_add_encard, Polynomial.degree_wronskian_lt_add, WithBot.lt_unbot_iff, withBotSucc_one, WithBot.ofDual_lt_ofDual_iff, WithTop.ofDual_le_ofDual_iff, WithBot.orderSucc_bot, WithBot.pred_coe_of_not_isMin, WithBot.map_eq_bot_iff, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_nonZeroDivisors, LatticeHom.withTopWithBot_toFun, WithBot.coe_add_eq_bot_iff, WithBot.bot_mul', Order.krullDim_eq_iSup_coheight, Order.krullDim_eq_bot_iff, SupHom.withBot_comp, WithBot.sSup_empty, WithBot.coe_iInf, WithBot.noMaxOrder, Module.supportDim_quotSMulTop_succ_eq_supportDim, Nat.WithBot.one_le_iff_zero_lt, WithTop.toDual_lt_toDual_iff, Polynomial.degree_mul', WithBot.ofDual_symm_apply, Polynomial.degree_one_le, WithBot.recBotCoe_bot, Polynomial.tendsto_nhds_iff, WithBot.succ_unbot, BoxIntegral.Box.splitLower_eq_bot, ringKrullDim_quotient_succ_le_of_nonZeroDivisor, BoxIntegral.Box.coe_inf, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_jacobson, WithZero.toMulBot_zero, Polynomial.Chebyshev.degree_U_neg_one, OrderIso.withBotCongr_apply, WithBot.strictMono_iff, Polynomial.degree_cubic, WithBot.forall, BoxIntegral.Box.mk'_eq_bot, WithBot.coe_nonneg, Cubic.degree_of_a_eq_zero, WithBot.map_le_iff, WithBot.toDualTopEquiv_symm_bot, Polynomial.degree_X_pow, Order.krullDim_eq_iSup_height, Cubic.equiv_symm_apply_b, WithTop.toDual_symm_apply, WithTop.ofDual_map, BoxIntegral.Box.disjoint_splitLower_splitUpper, WithTop.map_toDual, IsPrincipalIdealRing.ringKrullDim_eq_one, Lagrange.degree_basis, ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial, WithBot.unbot_le_unbot, WithBot.succ_zero, Order.krullDim_eq_zero_iff_of_orderTop, Finset.max_eq_bot, Polynomial.degree_one, WithBot.instIsEmptySuccOrderOfNonempty, Polynomial.Splits.splits, minpoly.IsIntegrallyClosed.degree_le_of_ne_zero, WithBot.coe_iSup, Polynomial.degree_prod_le, OrderEmbedding.withBotCoe_apply, Polynomial.div_eq_quo_add_rem_div, Polynomial.degree_prod, SupHom.withBot_toFun, BoxIntegral.Box.withBotCoe_subset_iff, Polynomial.degree_zero_le, Polynomial.Monic.degree_pos_of_not_isUnit, ringKrullDim_eq_zero_of_isField, WithBot.instNoZeroDivisors, Polynomial.isBoundedUnder_abs_atBot_iff, WithBot.lt_toDual_iff, Order.one_le_krullDim_iff, InfHom.withBot'_toFun, WithBot.sInf_empty, Equiv.withBotCongr_symm, LatticeHom.withBot_comp, WithBot.not_lt_bot, WeierstrassCurve.Affine.degree_polynomial, Order.krullDim_le_of_strictMono, WithBot.toDualTopEquiv_symm_coe, SupHom.withBot'_toFun, WithBot.unbotD_le_iff, WithTop.toDual_symm, Polynomial.degree_pos_of_not_isUnit_of_dvd_monic, WithBot.map_comp_map, WithBot.ofDual_bot, LinearRecurrence.charPoly_degree_eq_order, ringKrullDim_le_iff_isMaximal_height_le, Finset.max_eq_top, WithBot.strictMono_map_iff, Finset.max_empty, ringKrullDim_le_ringKrullDim_add_card, WithBot.ciSup_empty, Lagrange.degree_interpolate_le, Cubic.degree_of_c_ne_zero, CategoryTheory.projectiveDimension_le_iff, Cubic.degree_of_a_ne_zero, minpoly.min, MvPolynomial.degree_finSuccEquiv, Module.supportDim_le_ringKrullDim, BoxIntegral.Box.disjoint_coe, WithTop.toDual_le_toDual_iff, Polynomial.mem_closure_X_union_C, Polynomial.supDegree_eq_degree, Module.supportDim_le_supportDim_quotSMulTop_succ, WithBot.addLECancellable_iff_ne_bot, CategoryTheory.projectiveDimension_ge_iff, Field.primitive_element_iff_minpoly_degree_eq, WithBot.denselyOrdered, Equiv.withBotSubtypeNe_apply, Polynomial.degree_X, WithBot.unbot_le_unbot_iff, Ordnode.Bounded.weak, Module.supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson, WithBot.succ_bot, Polynomial.degree_multiset_prod_le, ringKrullDim_lt_top, List.not_maximum_lt_of_mem', WithTop.le_ofDual_iff, CategoryTheory.injectiveDimension_lt_iff, Polynomial.degree_prod_of_monic, List.le_maximum_of_mem', Polynomial.degree_sub_le, Polynomial.degree_of_subsingleton, WithBot.le_ofDual_iff, WithBot.preimage_coe_Icc, Polynomial.Monic.degree_mul, WithBot.isOrderedAddMonoid, WithBot.orderIsoPUnitSumLex_toLex, Polynomial.ringKrullDim_le, Matrix.charpoly_sub_diagonal_degree_lt, WithBot.unbotD_one, Polynomial.degree_eq_zero_of_isUnit, LatticeHom.withBot'_toFun, Polynomial.degree_smul_le, WithBot.coe_lt_coe, WithBot.lt_def_aux, Finset.max_insert, Nat.WithBot.lt_one_iff_le_zero, Cubic.equiv_symm_apply_c, WithBot.mul_eq_bot_iff, NonemptyInterval.coe_zero_interval, minpoly.degree_eq_one_iff, WithBot.lt_coe_bot, Polynomial.degree_lt_degree, WithBot.total_le, Polynomial.degree_le_iff_coeff_zero, WithTop.toDualBotEquiv_symm_coe, WithBot.instArchimedean, WithBot.coe_biInf, WithBot.orderSucc_coe, Polynomial.isBoundedUnder_abs_atTop_iff, WithBot.bot_lt_iff_ne_bot, Polynomial.card_roots, WithBot.pred_coe_of_isMin, Polynomial.ofFn_degree_lt, CategoryTheory.projectiveDimension_eq_bot_iff, WithBot.canLift, WithZero.toMulBot_coe, IsSepClosed.degree_eq_one_of_irreducible, Polynomial.degree_eq_card_roots, WithBot.subtypeOrderIso_apply_coe, Polynomial.degree_add_degree_leadingCoeff_inv, WithBot.one_eq_coe, WithBot.Ico_coe, PowerBasis.degree_minpolyGen, Order.krullDim_le_one_iff_forall_isMax, WithBot.unbot_le_iff, WithBot.ofDual_symm, Order.krullDim_withBot, WithTop.ofDual_le_iff, WithBot.le_def_aux, WithBot.denselyOrdered_iff, Order.krullDim_pos_iff_of_orderTop, Polynomial.degree_modByMonic_lt, WithBot.succ_natCast, WithBot.instMulPosReflectLT, Cubic.degree_of_d_eq_zero', Polynomial.degree_eq_one_of_irreducible_of_splits, ringKrullDim_nat, Polynomial.degree_lt_iff_coeff_zero, IsDiscreteValuationRing.toWithBotNat_eq_bot_iff, WithBot.nontrivial, WithBot.le_add_self, Polynomial.div_tendsto_atBot_zero_iff_degree_lt, Nat.cast_withBot, WithBot.bot_lt_coe, LaurentPolynomial.degree_C_ite, WithBot.Icc_coe, WithBot.toDualTopEquiv_bot, WithBot.le_def', div_eq_quo_add_rem_div_add_rem_div, WithBot.sum_lt_bot, Order.krullDim_eq_zero, WithBot.toDual_lt_iff, WithBot.coe_pow, Polynomial.degree_le_zero_iff, WithBot.coe_mono, Order.krullDim_pos_iff_of_orderBot, Equiv.withBotCongr_trans, Polynomial.degree_add_le, WithBot.preimage_coe_Iic, CategoryTheory.injectiveDimension_eq_bot_iff, WithBot.toDual_le_toDual_iff, List.maximum_mono, Polynomial.isUnit_iff_degree_eq_zero, WithBot.instIsOrderedRing, WithBot.coe_one, Polynomial.degree_pos_of_aeval_root, Polynomial.degree_cyclotomic', WithBot.mul_bot, Order.coheight_coe_withBot, InfHom.withBot_comp, WithBot.coe_top, WithBot.unbotD_zero, MvPolynomial.weightedTotalDegree'_zero, WithBot.unbotA_lt_iff, WithTop.ofDual_lt_iff, Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson, WithBot.Ioo_coe, Polynomial.le_degree_of_ne_zero, WithBot.lt_def', Cubic.equiv_apply_coe, PowerSeries.IsWeierstrassFactorization.degree_eq_coe_lift_order_map, instFiniteWithBot, Polynomial.degree_eq_one_of_irreducible_of_root, WithBot.unbot_lt_unbot, WithBot.zero_eq_map_iff, Polynomial.degree_mul_X, Polynomial.le_degree_of_mem_supp, Polynomial.degree_annIdealGenerator_le_of_mem, WithBot.coe_nsmul, WithBot.Ico_coe_coe, height_le_ringKrullDim_quotient_add_spanFinrank, WithBot.le_bot_iff, PowerSeries.IsWeierstrassFactorizationAt.degree_eq_coe_lift_order_map_of_ne_top, Polynomial.abs_isBoundedUnder_iff, WithBot.instMulPosReflectLE, Polynomial.natDegree_eq_zero_iff_degree_le_zero, Polynomial.degree_sub_lt, PowerSeries.isWeierstrassDivisionAt_iff, WithBot.instWellFoundedGT, BoxIntegral.Prepartition.mem_inf, Nat.WithBot.add_eq_zero_iff, Polynomial.degree_update_le, WithBot.coeOrderHom_apply, ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial, Order.krullDim_eq_bot, WithBot.map₂_bot_right, Polynomial.integralNormalization_coeff, Cubic.degree_of_b_ne_zero', Polynomial.degree_leadingCoeff_inv, Polynomial.Sequence.degree_strictMono, WithBot.add_right_inj, Polynomial.degree_shiftedLegendre, WithTop.ofDual_symm_apply, Order.krullDim_eq_length_of_finiteDimensionalOrder, Polynomial.span_le_degreeLE_of_finite, WithBot.Ioo_coe_coe, WithBot.toDual_symm_apply, WithBot.map_injective, BoxIntegral.Prepartition.mem_restrict, Polynomial.degree_pos_of_irreducible, Cubic.degree_of_b_eq_zero', Order.KrullDimLE.krullDim_le, WithBot.coe_max, WithBot.forall_le_coe_iff_le, ringKrullDim_le_ringKrullDim_add_spanFinrank, Polynomial.degree_cubic_le, LaurentPolynomial.degree_eq_bot_iff, Cubic.degree_of_c_ne_zero', WithBot.le_self_add, WithBot.bot_lt_sum_iff, Cubic.degree_of_d_ne_zero', OrderIso.withBotCongr_trans, Cubic.equiv_symm_apply_d, ZeroHom.withBotMap_apply, LatticeHom.coe_withBot, WithBot.Ioo_bot_coe, Polynomial.degree_div_le, Irreducible.degree_le_two, Polynomial.degree_linear_le, WithBot.bot_mul, WithTop.toDual_map, Order.krullDim_eq_one_iff_of_boundedOrder, WithBot.forall_coe_le_iff_le, MvPolynomial.weightedTotalDegree'_eq_bot_iff, WithBot.preimage_coe_Ioc_bot, Order.krullDim_nonneg, Polynomial.degree_eq_card_roots', WithBot.coe_sup, WithBot.coe_add, Polynomial.degree_linear_lt_degree_C_mul_X_sq, Polynomial.degree_cyclotomic_pos, WithZero.toMulBot_le, WithBot.preimage_coe_Ioi_bot, Polynomial.degree_pos_of_eval₂_root, ringKrullDim_eq_zero_of_field, WithBot.coe_biSup, Polynomial.degree_quadratic_lt_degree_C_mul_X_cb, WithBot.none_eq_bot, WithBot.denselyOrdered_set_iff_subsingleton, Cubic.degree_of_c_eq_zero, Cubic.equiv_symm_apply_a, WithBot.coe_sSup', Polynomial.degree_C_mul_X, NonemptyInterval.coe_sup_interval, Order.krullDim_le_one_iff_forall_isMin, Polynomial.degree_pow', WithBot.toDual_symm, WithBot.addRightReflectLT, Polynomial.ringKrullDim_of_isNoetherianRing, Order.height_coe_withBot, OneHom.withBotMap_apply, Polynomial.natDegree_pos_iff_degree_pos, MvPolynomial.ringKrullDim_of_isNoetherianRing, Polynomial.degree_mod_lt, WithBot.unbotD_eq_unbotD_iff, WithBot.coe_sum, WithBot.Ioc_coe_coe, IsDiscreteValuationRing.toWithBotNat_le_toWithBotNat_iff, Polynomial.degree_multiset_prod, WithBot.unbot_lt_unbot_iff, Polynomial.mem_degreeLE, WithTop.toDual_le_iff, AddMonoidAlgebra.supDegree_withBot_some_comp, Polynomial.splits_iff_splits, CategoryTheory.Retract.projectiveDimension_le, WithBot.lt_iff_exists, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson, Polynomial.degree_sum_fin_lt, IsAlgClosed.degree_eq_one_of_irreducible, Polynomial.degree_eq_iff_natDegree_eq, WithBot.coe_mul_eq_bind, Polynomial.degreeLE_eq_span_X_pow, WithBot.succ_eq_succ, WithTop.ofDual_top, WithTop.lt_ofDual_iff, WithBot.coe_covBy_coe, Polynomial.degree_map_lt, Ideal.height_le_ringKrullDim_of_ne_top, WithBot.map_id, Cubic.degree_of_c_eq_zero', Polynomial.natDegree_le_iff_degree_le, Polynomial.Sequence.basis_degree_strictMono, WithBot.succ_strictMono, Polynomial.degree_add_eq_of_leadingCoeff_add_ne_zero, WithBot.instPosMulReflectLT, Polynomial.degree_monomial, Polynomial.degree_mul_X_pow, List.le_maximum_of_length_pos_iff, WithBot.instCountable, Order.krullDim_of_noMinOrder, WithBot.exists_coe_lt, LaurentPolynomial.degree_T_le, Polynomial.div_tendsto_atTop_zero_iff_degree_lt, ringKrullDim_le_of_surjective, WithBot.image_coe_Icc, Nat.WithBot.coe_nonneg, Polynomial.degree_C_mul_X_pow, WithBot.coe_natCast, Order.krullDim_of_isSimpleOrder, ringKrullDim_le_ringKrullDim_quotSMulTop_succ, Module.supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes, Polynomial.Chebyshev.degree_U_natCast, OrderEmbedding.withBotMap_apply, Polynomial.degree_erase_le, Module.supportDim_le_of_surjective, WithBot.map_zero, Polynomial.degree_cyclotomic, WithBot.le_coe_unbotD, Polynomial.leadingCoeff_eq_zero_iff_deg_eq_bot, Cubic.degree_of_zero, Order.krullDim_eq_zero_iff_of_orderBot, AddHom.withBotMap_apply, Finset.le_max, WithZero.toMulBot_symm_bot, WithBot.bot_lt_one, WithBot.IsWellOrder.gt, WithBot.Icc_coe_coe, NonemptyInterval.coe_mul_interval, Module.supportDim_eq_bot_of_subsingleton, Polynomial.degree_derivative_le, WithBot.unbotD_eq_self_iff, WithBot.add_left_inj, Polynomial.degree_linear, Order.bot_lt_krullDim_iff, Polynomial.mem_degreeLT, WithBot.le_def, Polynomial.Monic.degree_le_zero_iff_eq_one, WithBot.preimage_coe_Ioo_bot, PowerBasis.dim_le_degree_of_root, WithBot.Ici_coe, WithBot.add_lt_add_iff_left, WithBot.trichotomous.lt, LaurentPolynomial.degree_zero, WithBot.ofDual_le_ofDual_iff, Finset.max_one, WithZero.toMulBot_strictMono, Polynomial.degree_eq_bot, WithBot.some_mem_insertBot, WithTop.toDual_apply_coe, WithBot.unbotA_le_iff, LatticeHom.withBot_apply, WithBot.one_le_iff_pos, WithTop.coe_toDualBotEquiv, WithBot.bot_mem_insertBot, WithBot.Icc_bot_coe, LaurentPolynomial.degree_C_le, Polynomial.degree_list_sum_le, WithBot.map_toDual, List.maximum_concat, WithBot.one_eq_map_iff, Polynomial.degree_linear_lt, WithBot.coe_strictMono, Polynomial.degree_natCast_le, Polynomial.degree_coe_units, WithTop.toDualBotEquiv_top, Order.krullDim_nat, Polynomial.degree_modByMonic_le_left, Finset.sup_of_mem, List.maximum_append, ringKrullDim_le_ringKrullDim_quotient_add_encard, WithBot.bot_wcovBy_coe, Order.krullDimLE_iff, WithBot.coe_le_one, Polynomial.exists_mul_add_mul_eq_C_resultant, Cubic.degree_of_b_ne_zero, Polynomial.roots_def, InfHom.withBot_id, LaurentPolynomial.degree_C_mul_T_le, WithTop.eq_bot_iff_forall_le, Order.krullDim_eq_top_iff, WithBot.orderIsoPUnitSumLex_bot, WithBot.coe_zero, WithBot.one_le_coe, Polynomial.degree_X_add_C, degree_radical_le, Polynomial.degree_mul, Polynomial.degree_gcd_le_right, Polynomial.degree_C_le, WithBot.add_lt_add_iff_right, WithBot.add_eq_bot, WithBot.ofDual_apply_bot, WithBot.add_one_le_iff, WithBot.coe_mul, OrderIso.withBotCongr_symm, WithBot.preimage_coe_Ioo

---

← Back to Index