Basic

📁 Source: Mathlib/Order/Basic.lean

Statistics

Metric	Count
Definitions AsLinearOrder, linearOrder, linearOrder, partialOrder, preorder, lift', liftWithOrd, liftWithOrd', ofSubsingleton, exactLeOfLt, decidable, instLinearOrder, hasLe, instCompl, partialOrder, preorder, sdiff, instDecidableLE, instLE_mathlib, instPartialOrder, instPreorder, instCompl, le, partialOrder, StrongLT, decidableLE, decidableLT, instLinearOrder, partialOrder, preorder, instInhabitedAsLinearOrder, instLinearOrderEmpty, instLinearOrderPEmpty, «term_⁻¹'o_»	34
Theorems eq_iff_ge_not_gt, eq_iff_le_not_lt, eq_or_lt_of_le, eq_or_lt_of_le', le_iff_eq_or_lt, le_iff_eq_or_lt', ne_iff_gt_iff_ge, ne_iff_lt_iff_le, dense, dense', ge, le, not_gt, not_lt, trans_ge, trans_gt, trans_le, trans_lt, const_le_const, const_lt_const, le, lt, ext, ext_iff, antisymm, antisymm', eq_of_not_lt, eq_of_not_lt', eq_or_lt, eq_or_lt', eq_or_lt_dec, eq_or_lt_dec', ge, ge_iff_eq, ge_iff_eq', ge_or_le, ge_or_lt, gt_or_le, le_or_ge, le_or_gt, lt_iff_ne, lt_iff_ne', lt_of_ne, lt_of_ne', lt_of_not_ge, lt_or_eq, lt_or_eq', lt_or_eq_dec, lt_or_eq_dec', lt_or_ge, not_lt_iff_eq, not_lt_iff_eq', trans, trans', trans_eq, trans_eq', trans_lt, trans_lt', trans_strongLT, asymm, false, gt, gt_or_lt, le, lt_or_gt, ne, ne', not_gt, trans, trans', trans_eq, trans_eq', trans_le, trans_le', ext, ext_lt, toPartialOrder_injective, toPartialOrder_injective_iff, ge_iff_gt, gt_or_lt, instIsEquiv_compl, le_iff_lt, lt_of_le, lt_of_le', lt_or_gt, not_ge_or_not_le, not_le_or_not_ge, instDenselyOrdered, le, max_eq, min_eq, not_lt, ext, ext_lt, toPreorder_injective, toPreorder_injective_iff, compl_apply, compl_def, le_def, lt_def, sdiff_apply, sdiff_def, ext, toLE_injective, toLE_injective_iff, mk_le_mk, le_def, lt_iff, lt_of_le_of_lt, lt_of_lt_of_le, mk_le_mk, mk_le_mk_iff_left, mk_le_mk_iff_right, mk_le_swap, mk_lt_mk, mk_lt_mk_iff_left, mk_lt_mk_iff_right, mk_lt_mk_of_le_of_lt, mk_lt_mk_of_lt_of_le, mk_lt_swap, swap_le_mk, swap_le_swap, swap_lt_mk, swap_lt_swap, compl, compl, le, lt, trans_le, instDenselyOrdered, coe_le_coe, coe_lt_coe, mk_le_mk, mk_lt_mk, const_le_elim_iff, elim_le_const_iff, elim_le_elim_iff, associative_of_commutative_of_le, commutative_of_le, compare_of_injective_eq_compareOfLessAndEq, compl_ge, compl_gt, compl_le, compl_lt, dense_or_discrete, dense_or_discrete', eq_iff_eq_of_lt_iff_lt_of_gt_iff_gt, eq_iff_ge_not_gt, eq_iff_le_not_lt, eq_of_forall_ge_iff, eq_of_forall_gt_iff, eq_of_forall_le_iff, eq_of_forall_lt_iff, eq_of_le_of_forall_gt_imp_ge_of_dense, eq_of_le_of_forall_lt_imp_le_of_dense, eq_of_le_of_not_lt, eq_of_le_of_not_lt', eq_or_eq_or_eq_of_forall_not_lt_lt, eq_or_lt_of_le, eq_or_lt_of_le', exists_between, exists_between', exists_forall_ge_and, exists_forall_le_and, exists_ge_of_linear, exists_le_of_linear, forall_ge_iff_le, forall_ge_imp_ne_iff_lt, forall_gt_iff_le, forall_gt_imp_ge_iff_le_of_dense, forall_gt_imp_ne_iff_le, forall_le_iff_le, forall_le_imp_ne_iff_lt, forall_lt_iff_le, forall_lt_imp_le_iff_le_of_dense, forall_lt_imp_ne_iff_le, ge_trans', gt_trans', instDenselyOrderedForall, instDenselyOrderedProd, le_Prop_eq, le_iff_eq_or_lt, le_iff_eq_or_lt', le_iff_le_iff_lt_iff_lt, le_imp_eq_iff_le_imp_ge, le_imp_eq_iff_le_imp_ge', le_imp_le_iff_lt_imp_lt, le_imp_le_of_le_of_le, le_of_eq_of_le', le_of_forall_ge, le_of_forall_gt, le_of_forall_gt_imp_ge_of_dense, le_of_forall_gt_imp_ne, le_of_forall_le, le_of_forall_lt, le_of_forall_lt_imp_le_of_dense, le_of_forall_lt_imp_ne, le_of_le_of_eq', le_of_strongLT, le_of_subsingleton, le_trans', le_update_iff, le_update_self_iff, lt_iff_le_and_ne, lt_iff_le_and_ne', lt_iff_lt_of_le_iff_le, lt_iff_lt_of_le_iff_le', lt_imp_lt_of_le_imp_le, lt_imp_lt_of_le_of_le, lt_of_eq_of_lt', lt_of_forall_ge_imp_ne, lt_of_forall_le_imp_ne, lt_of_lt_of_eq', lt_of_strongLT, lt_or_gt_iff_ne', lt_or_lt_iff_ne, lt_self_iff_false, lt_trans', lt_update_self_iff, max_def_lt, max_def_lt', max_rec, max_rec', min_def_lt, min_def_lt', min_rec, min_rec', ne_iff_gt_iff_ge, ne_iff_lt_iff_le, ne_of_not_ge, ne_of_not_le, not_lt_iff_eq_or_lt, not_lt_iff_eq_or_lt', not_lt_iff_le_imp_ge, not_lt_iff_not_le_or_ge, not_lt_of_subsingleton, rel_imp_eq_of_rel_imp_le, strongLT_of_le_of_strongLT, strongLT_of_strongLT_of_le, subrelation_iff_le, update_le_iff, update_le_self_iff, update_le_update_iff, update_le_update_iff', update_lt_self_iff, update_lt_update_iff	246
Total	280

AsLinearOrder

Definitions

Name	Category	Theorems
linearOrder 📖	CompOp	—

Decidable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_iff_ge_not_gt 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder Preorder.toLT	—	Eq.ge lt_irrefl LE.le.antisymm' LE.le.lt_of_not_ge
eq_iff_le_not_lt 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder Preorder.toLT	—	Eq.le lt_irrefl LE.le.antisymm LE.le.lt_of_not_ge
eq_or_lt_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	lt_or_eq_of_le
eq_or_lt_of_le' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	lt_or_eq_of_le'
le_iff_eq_or_lt 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder Preorder.toLT	—	le_iff_lt_or_eq
le_iff_eq_or_lt' 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder Preorder.toLT	—	le_iff_lt_or_eq'
ne_iff_gt_iff_ge 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder Preorder.toLE	—	ge_of_eq le_of_lt lt_of_le_of_ne' ne_of_gt
ne_iff_lt_iff_le 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder Preorder.toLE	—	le_of_eq le_of_lt lt_of_le_of_ne ne_of_lt

DenselyOrdered

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dense 📖	—	—	—	—	—
dense' 📖	—	—	—	—	dense

Eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ge 📖	mathematical	—	Preorder.toLE	—	ge_of_eq
le 📖	mathematical	—	Preorder.toLE	—	le_of_eq
not_gt 📖	mathematical	—	Preorder.toLT	—	LT.lt.ne'
not_lt 📖	mathematical	—	Preorder.toLT	—	LT.lt.ne
trans_ge 📖	—	—	—	—	le_of_eq_of_le''
trans_gt 📖	—	—	—	—	lt_of_eq_of_lt''
trans_le 📖	—	—	—	—	—
trans_lt 📖	—	—	—	—	—

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_le_const 📖	mathematical	—	Pi.hasLe Preorder.toLE	—	—
const_lt_const 📖	mathematical	—	Preorder.toLT Pi.preorder	—	le_of_lt

Function.Injective

Definitions

Name	Category	Theorems
linearOrder 📖	CompOp	—
partialOrder 📖	CompOp	—
preorder 📖	CompOp	—

GE.ge

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le 📖	—	—	—	—	—

GT.gt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lt 📖	—	—	—	—	—

LE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	—	—	—	—
ext_iff 📖	—	—	—	—	ext

LE.le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antisymm 📖	—	Preorder.toLE PartialOrder.toPreorder	—	—	le_antisymm
antisymm' 📖	—	Preorder.toLE PartialOrder.toPreorder	—	—	ge_antisymm
eq_of_not_lt 📖	—	Preorder.toLE PartialOrder.toPreorder Preorder.toLT	—	—	eq_of_le_of_not_lt
eq_of_not_lt' 📖	—	Preorder.toLE PartialOrder.toPreorder Preorder.toLT	—	—	eq_of_le_of_not_lt'
eq_or_lt 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	eq_or_lt_of_le
eq_or_lt' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	eq_or_lt_of_le'
eq_or_lt_dec 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	Decidable.eq_or_lt_of_le
eq_or_lt_dec' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	Decidable.eq_or_lt_of_le'
ge 📖	—	—	—	—	—
ge_iff_eq 📖	—	Preorder.toLE PartialOrder.toPreorder	—	—	antisymm Eq.ge
ge_iff_eq' 📖	—	Preorder.toLE PartialOrder.toPreorder	—	—	antisymm' Eq.le
ge_or_le 📖	—	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder	—	—	le_of_lt gt_or_le
ge_or_lt 📖	mathematical	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder	Preorder.toLT	—	trans_lt' le_or_gt
gt_or_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder	Preorder.toLT	—	trans' lt_or_ge
le_or_ge 📖	—	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder	—	—	le_of_lt lt_or_ge
le_or_gt 📖	mathematical	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder	Preorder.toLT	—	trans_lt le_or_gt
lt_iff_ne 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	ne_of_lt lt_of_ne
lt_iff_ne' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	ne_of_gt lt_of_ne'
lt_of_ne 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	lt_of_le_of_ne
lt_of_ne' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	lt_of_le_of_ne'
lt_of_not_ge 📖	mathematical	Preorder.toLE	Preorder.toLT	—	lt_of_le_not_ge
lt_or_eq 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	lt_or_eq_of_le
lt_or_eq' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	lt_or_eq_of_le'
lt_or_eq_dec 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	Decidable.lt_or_eq_of_le
lt_or_eq_dec' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	Decidable.lt_or_eq_of_le'
lt_or_ge 📖	mathematical	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder	Preorder.toLT	—	trans lt_or_ge
not_lt_iff_eq 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	Iff.not_left lt_iff_ne
not_lt_iff_eq' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	Iff.not_left lt_iff_ne'
trans 📖	—	Preorder.toLE	—	—	le_trans
trans' 📖	—	Preorder.toLE	—	—	ge_trans
trans_eq 📖	—	—	—	—	—
trans_eq' 📖	—	—	—	—	le_of_le_of_eq''
trans_lt 📖	—	Preorder.toLE Preorder.toLT	—	—	lt_of_le_of_lt
trans_lt' 📖	—	Preorder.toLE Preorder.toLT	—	—	lt_of_le_of_lt'
trans_strongLT 📖	—	Pi.hasLe Preorder.toLE StrongLT Preorder.toLT	—	—	strongLT_of_le_of_strongLT

LT.lt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asymm 📖	—	Preorder.toLT	—	—	lt_asymm
false 📖	—	Preorder.toLT	—	—	lt_irrefl
gt 📖	—	—	—	—	—
gt_or_lt 📖	—	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	—	—	trans_le le_or_gt
le 📖	mathematical	Preorder.toLT	Preorder.toLE	—	le_of_lt
lt_or_gt 📖	—	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	—	—	trans_le' le_or_gt
ne 📖	—	Preorder.toLT	—	—	ne_of_lt
ne' 📖	—	Preorder.toLT	—	—	ne_of_gt
not_gt 📖	—	Preorder.toLT	—	—	lt_asymm
trans 📖	—	Preorder.toLT	—	—	lt_trans
trans' 📖	—	Preorder.toLT	—	—	gt_trans
trans_eq 📖	—	—	—	—	—
trans_eq' 📖	—	—	—	—	lt_of_lt_of_eq''
trans_le 📖	—	Preorder.toLT Preorder.toLE	—	—	lt_of_lt_of_le
trans_le' 📖	—	Preorder.toLT Preorder.toLE	—	—	lt_of_lt_of_le'

LinearOrder

Definitions

Name	Category	Theorems
lift' 📖	CompOp	—
liftWithOrd 📖	CompOp	—
liftWithOrd' 📖	CompOp	—
ofSubsingleton 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	Preorder.toLE PartialOrder.toPreorder toPartialOrder	—	—	toPartialOrder_injective PartialOrder.toPreorder_injective Preorder.toLE_injective LE.ext
ext_lt 📖	—	Preorder.toLT PartialOrder.toPreorder toPartialOrder	—	—	toPartialOrder_injective PartialOrder.ext_lt
toPartialOrder_injective 📖	mathematical	—	LinearOrder PartialOrder toPartialOrder	—	—
toPartialOrder_injective_iff 📖	mathematical	—	toPartialOrder	—	toPartialOrder_injective

Mathlib.Tactic.GCongr

Definitions

Name	Category	Theorems
exactLeOfLt 📖	CompOp	—

Ne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ge_iff_gt 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder Preorder.toLT	—	lt_of_le_of_ne' LT.lt.le
gt_or_lt 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	—	gt_or_lt_of_ne
instIsEquiv_compl 📖	mathematical	—	IsEquiv Compl.compl Pi.instCompl Prop.instCompl	—	eq_isEquiv
le_iff_lt 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder Preorder.toLT	—	lt_of_le_of_ne LT.lt.le
lt_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	lt_of_le_of_ne
lt_of_le' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	lt_of_le_of_ne'
lt_or_gt 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	—	lt_or_gt_of_ne
not_ge_or_not_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder	—	not_and_or Iff.not ge_antisymm_iff
not_le_or_not_ge 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder	—	not_and_or Iff.not le_antisymm_iff

Order.Preimage

Definitions

Name	Category	Theorems
decidable 📖	CompOp	—

PUnit

Definitions

Name	Category	Theorems
instLinearOrder 📖	CompOp	7 math math: min_eq, le, isOrderedCancelAddMonoid, max_eq, not_lt, canonicallyOrderedAdd, instDenselyOrdered

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDenselyOrdered 📖	mathematical	—	DenselyOrdered Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder instLinearOrder	—	—
le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder instLinearOrder	—	—
max_eq 📖	mathematical	—	LinearOrder.toMax instLinearOrder	—	—
min_eq 📖	mathematical	—	LinearOrder.toMin instLinearOrder	—	—
not_lt 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder instLinearOrder	—	—

PartialOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	Preorder.toLE toPreorder	—	—	toPreorder_injective Preorder.toLE_injective LE.ext
ext_lt 📖	—	Preorder.toLT toPreorder	—	—	toPreorder_injective Preorder.toLE_injective LE.ext le_iff_lt_or_eq
toPreorder_injective 📖	mathematical	—	PartialOrder Preorder toPreorder	—	—
toPreorder_injective_iff 📖	mathematical	—	toPreorder	—	toPreorder_injective

Pi

Definitions

Name	Category	Theorems
hasLe 📖	CompOp	247 math math: CategoryTheory.ObjectProperty.isoModSerre_isInvertedBy_iff, AddGroupNorm.coe_le_coe, Function.const_nonpos_of_nonpos, MeasureTheory.lintegral_def, CategoryTheory.ObjectProperty.le_limitsClosure, existsMulOfLe, Function.one_le_const_of_one_le, RootPairing.Base.not_nonneg_iff_neg_of_sum_mem_range_root, instCanonicallyOrderedAddForall, GroupNorm.le_def, Finsupp.coe_le_coe, Prod.rprod_le_transGen_gameAdd, le_update_self_iff, instZeroLEOneClass, CategoryTheory.ObjectProperty.le_shiftClosure, ValueDistribution.proximity_zero_mul_le, Function.one_le_const, OrderHom.mk_le_mk, CategoryTheory.ObjectProperty.le_isoClosure, BoxIntegral.Box.le_TFAE, CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.colimitsOfShape_le, OrderHom.piIso_symm_apply, Seminorm.coe_le_coe, single_nonpos, CategoryTheory.exactFunctor_le_additiveFunctor, PartitionOfUnity.nonneg', SimpleGraph.Reachable.mono', thickenedIndicatorAux_mono, Fin.insertNth_le_iff, CategoryTheory.IsCardinalLocallyPresentable.iff_exists_isStrongGenerator, thickenedIndicatorAux_subset, Part.Fix.approx_le_fix, Prod.gameAdd_le_lex, bddBelow_range_pi, AddGroupNorm.le_def, Set.indicator_le_indicator_nonneg, ValueDistribution.proximity_nonneg, lt_def, pure_le_nhds, update_le_update_iff', Fin.insertNthOrderIso_symm_apply, indicator_le_thickenedIndicatorAux, Set.mulIndicator_le_self', OrderHom.coe_le_coe, Sum.one_le_elim_iff, Sym2.fromRel_mono_iff, CategoryTheory.ObjectProperty.op_monotone_iff, Fin.insertNthOrderIso_toEquiv, AlgebraicGeometry.IsLocalIso.le_of_isZariskiLocalAtSource, MeasureTheory.Measure.LebesgueDecomposition.iSup_le_le, Set.piecewise_mono, BoxIntegral.Box.le_iff_bounds, bddAbove_pi, CategoryTheory.ObjectProperty.colimitsOfShape_le_of_final, update_le_update_iff, MeasureTheory.SimpleFunc.coe_le, CategoryTheory.Localization.LeftBousfield.le_W_iff, TopologicalSpace.le_def, CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le', Function.const_le_one_of_le_one, SimpleGraph.cliqueSet_mono', Function.locallyFinsuppWithin.le_def, CategoryTheory.isCardinalPresentable_monotone, Set.indicator_nonpos_le_indicator, CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.le_isCardinalPresentable, Sum.nonneg_elim_iff, Function.const_nonneg_of_nonneg, CategoryTheory.ObjectProperty.strictLimitsOfShape_le_limitsOfShape, PseudoMetric.coe_le_coe, ValueDistribution.proximity_sum_top_le, Sum.elim_le_const_iff, CircleDeg1Lift.iterate_mono, Finset.piecewise_le_piecewise', Ordinal.IsNormal.id_le, CategoryTheory.ObjectProperty.ofObj_le_iff, AlgebraicGeometry.IsLocalIso.le_of_isLocalAtSource, AlgebraicGeometry.Scheme.IdealSheafData.le_ofIdeals_iff, CategoryTheory.ObjectProperty.le_strictLimitsClosureStep, MeasureTheory.exists_measurable_le_forall_setLIntegral_eq, CategoryTheory.leftExactFunctor_le_additiveFunctor, exists_continuous_nonneg_pos, MeasureTheory.SimpleFunc.mk_le_mk, Function.const_le_one, Matrix.IsHermitian.posSemidef_iff_eigenvalues_nonneg, disjointed_le_id, ValueDistribution.proximity_mul_zero_le, Fin.cons_le_cons, CategoryTheory.ObjectProperty.strictLimitsClosureIter_le_limitsClosure, Seminorm.bddAbove_iff, Ideal.pi_le_pi_iff, OrderIso.funUnique_toEquiv, indicator_le_thickenedIndicator, ValueDistribution.proximity_add_top_le, isGLB_pi, CategoryTheory.GrothendieckTopology.le_def, Set.indicator_le_self', CategoryTheory.ObjectProperty.shiftClosure_le_iff, MeasureTheory.iSup_lintegral_measurable_le_eq_lintegral, subrelation_iff_le, Set.piecewise_le, Function.const_nonpos, DFinsupp.coe_orderEmbeddingToFun, Sum.elim_le_one_iff, one_le_mulSingle, extend_partialOrder, Fin.snocOrderIso_apply, BoxIntegral.Prepartition.upper_le_upper, Set.le_mulIndicator, GroupNorm.coe_le_coe, Relation.cutExpand_le_invImage_lex, conjneg_nonpos, RootPairing.Base.not_nonpos_iff_pos_of_sum_mem_range_root, Fin.cons_le, CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff, CategoryTheory.ObjectProperty.le_isLocal_iff, BumpCovering.nonneg', ValueDistribution.proximity_mul_top_le, CategoryTheory.ObjectProperty.isoClosure_le_iff, NonarchAddGroupNorm.le_def, Fin.snocOrderIso_symm_apply, instCanonicallyOrderedMulForall, Finsupp.orderEmbeddingToFun_apply, Fin.consOrderIso_apply, CategoryTheory.ObjectProperty.strictMap_le_map, MeasureTheory.SimpleFunc.coe_le_coe, IsOpen.measure_eq_biSup_integral_continuous, CategoryTheory.ObjectProperty.le_isLocal_isLocal, AddGroupSeminorm.coe_le_coe, CategoryTheory.ObjectProperty.le_isColocal_iff, ConvexOn.real_univ_sSup_affine_eq, mulSingle_le_one, Set.le_indicator, disjointed_le, le_update_iff, Matrix.zero_le_one_row, thickenedIndicator_subset, CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le, Ordinal.enumOrd_le_of_subset, bddAbove_range_pi, Fin.consOrderIso_symm_apply, CategoryTheory.ObjectProperty.le_colimitsClosure, CategoryTheory.ObjectProperty.retractClosure_le_iff, Set.indicator_le_self, OrderIso.funUnique_apply, SzemerediRegularity.le_stepBound, MeasurableSpace.le_def, CategoryTheory.ObjectProperty.unop_monotone_iff, gauge_mono, ConvexOn.univ_sSup_affine_eq, update_le_iff, Sum.elim_le_elim_iff, CategoryTheory.ObjectProperty.IsStableUnderShiftBy.le_shift, Part.Fix.le_f_of_mem_approx, BoxIntegral.Box.lower_le_upper, CategoryTheory.Triangulated.TStructure.le_zero_le, NonarchAddGroupNorm.coe_le_coe, CategoryTheory.ObjectProperty.le_def, le_of_strongLT, MeasureTheory.Measure.ae_le_pi, Fin.insertNthOrderIso_apply, Fin.consOrderIso_toEquiv, orderedSub, CategoryTheory.ObjectProperty.le_kernel_of_isoModSerre_isInvertedBy, IsWellFounded.exists_well_order_ge, Set.mulIndicator_le', Nucleus.coe_le_coe, single_nonneg, Fintype.exists_disjointed_le, CategoryTheory.exactFunctor_le_leftExactFunctor, Sum.const_le_elim_iff, GroupSeminorm.coe_le_coe, Set.indicator_le, Function.const_le_const, bddBelow_pi, AddGroupSeminorm.le_def, Ideal.coe_piOrderIso_symm_apply, GroupSeminorm.le_def, AEMeasurable.exists_measurable_nonneg, Function.const_nonneg, DFinsupp.coe_le_coe, Part.Fix.approx_mono', HasOuterApproxClosed.indicator_le_apprSeq, StrictMono.id_le, IsCompact.measure_eq_biInf_integral_hasCompactSupport, NonarchAddGroupSeminorm.le_def, CategoryTheory.ObjectProperty.le_isColocal_isColocal, HomotopicalAlgebra.bifibrantObjects_le_fibrantObject, Ordinal.id_le_enumOrd, conjneg_nonneg, Fin.snocOrderIso_toEquiv, AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le, MeasureTheory.exists_measurable_le_lintegral_eq, OrderIso.funUnique_symm_apply, Fin.le_cons, CategoryTheory.ObjectProperty.singleton_le_iff, Set.indicator_le', CategoryTheory.ObjectProperty.le_ind, le_partialSups, Set.le_piecewise, ValueDistribution.proximity_top_mul_le, le_def, existsAddOfLe, StrictMono.le_id, Fin.le_insertNth_iff, OrderHom.piIso_apply, update_le_self_iff, NonarchAddGroupSeminorm.coe_le_coe, MeasureTheory.exists_measurable_le_setLIntegral_eq_of_integrable, CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.limitsOfShape_le, CategoryTheory.ObjectProperty.limitsOfShape_le_of_initial, SimpleGraph.adj_le_reachable, CategoryTheory.Triangulated.TStructure.ge_one_le, CategoryTheory.ObjectProperty.strictColimitsOfShape_le_colimitsOfShape, ConvexOn.exists_affine_le_of_lt, BumpCovering.le_one', HomotopicalAlgebra.bifibrantObjects_le_cofibrantObject, CategoryTheory.rightExactFunctor_le_additiveFunctor, isLUB_pi, CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_iff, Fin.tuple0_le, InfHom.mk_le_mk, MeasurableSpace.DynkinSystem.le_def, MeasureTheory.exists_measurable_le_withDensity_eq, Set.mulIndicator_le, CategoryTheory.ObjectProperty.le_retractClosure, CategoryTheory.Pretopology.le_def, CategoryTheory.ObjectProperty.le_isLocal_W, CategoryTheory.exactFunctor_le_rightExactFunctor, Ideal.coe_piOrderIso_apply, single_le_single, ConvexOn.sSup_affine_eq, CategoryTheory.ObjectProperty.le_strictLimitsClosureIter, wellQuasiOrderedLE, SupHom.mk_le_mk, ConvexOn.real_sSup_affine_eq, Sum.elim_nonpos_iff, mulSingle_le_mulSingle, seminormFromConst_seq_nonneg, Part.Fix.approx_mono, CategoryTheory.ObjectProperty.le_colimitsCardinalClosure, MeasureTheory.GridLines.T_insert_le_T_lmarginal_singleton, DFinsupp.orderEmbeddingToFun_apply, CategoryTheory.ObjectProperty.le_shift, StrongLT.le, thickenedIndicator_mono, Set.mulIndicator_le_self, BoxIntegral.Prepartition.lower_le_lower
instCompl 📖	CompOp	31 math math: compl_le, isAntichain_union, MeasureTheory.ae_eq_set_compl, CategoryTheory.Limits.kernelForkBiproductToSubtype_cone, compl_def, Std.Irrefl.compl, CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype_isColimit, MeasureTheory.NullMeasurableSet.compl_toMeasurable_compl_ae_eq, Ordinal.cof_type, MeasureTheory.ae_eq_set_compl_compl, Std.Refl.compl, CategoryTheory.Limits.kernelBiproductToSubtypeIso_hom, Symmetric.compl, RelIso.compl_apply, antisymmRel_compl_apply, compl_ge, Relation.cutExpand_le_invImage_lex, CategoryTheory.Limits.cokernelBiproductFromSubtypeIso_hom, RelIso.compl_symm_apply, incompRel_compl_apply, SimpleGraph.cliqueFreeOn_two, antisymmRel_compl, Ne.instIsEquiv_compl, compl_lt, compl_apply, CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype_cocone, incompRel_compl, CategoryTheory.Limits.cokernelBiproductFromSubtypeIso_inv, compl_gt, CategoryTheory.Limits.kernelForkBiproductToSubtype_isLimit, CategoryTheory.Limits.kernelBiproductToSubtypeIso_inv
partialOrder 📖	CompOp	23 math math: isOrderedRing, ceilDiv_def, isOrderedCancelMonoid, isCoatomistic, CFC.nnrpow_map_pi, isOrderedAddCancelMonoid, isOrderedMonoid, CFC.rpow_eq_rpow_pi, floorDiv_def, codisjoint_iff, isCoatomic, CFC.nnrpow_eq_nnrpow_pi, isAtomistic, CFC.rpow_map_pi, CFC.sqrt_map_pi, isCompl_iff, disjoint_iff, floorDiv_apply, ceilDiv_apply, isOrderedAddMonoid, isAtomic, orderedSMul, instStarOrderedRing
preorder 📖	CompOp	259 math math: single_mono, pi_Iio_mem_nhds, MeasureTheory.Measure.univ_pi_Ioc_ae_eq_Icc, update_lt_update_iff, OrdinalApprox.lfpApprox_mono_mid, MeasureTheory.GridLines.T_lmarginal_antitone, MeasureTheory.hittingBtwn_mono_left, RootPairing.Base.not_nonneg_iff_neg_of_sum_mem_range_root, Fin.preimage_insertNth_Icc_of_mem, partialSups_mono, MeasureTheory.SimpleFunc.coe_lt_coe, Function.monotone_eval, wcovBy_iff, Part.Fix.exists_fix_le_approx, card_Ici, toColex_monotone, Function.update_mono, Function.update_strictMono, Set.IsPWO.pi, pi_Ioo_mem_nhds, Set.image_mulSingle_Ioo, Set.image_update_Ioo, BoxIntegral.Box.le_TFAE, DFinsupp.coe_mono, covBy_iff_exists_right_eq, instPosSMulStrictMono, OrderHom.piIso_symm_apply, pi_Ico_mem_nhds', Part.toUnitMono_coe, MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone, pi_Iic_mem_nhds', card_Iic, CategoryTheory.Localization.LeftBousfield.galoisConnection, IsClopen.upperClosure_pi, MeasureTheory.hittingAfter_mono, GroupSeminorm.lt_def, instIsOrderBornology, orderClosedTopology', Set.image_mulSingle_Icc_right, isPWO, IsClosed.lowerClosure_pi, Function.antitone_iterate_of_le_id, Part.Fix.approx_mem_approxChain, IsClopen.lowerClosure_pi, MeasureTheory.Measure.univ_pi_Ioo_ae_eq_Icc, Part.Fix.approx_le_fix, RootPairing.Base.pos_or_neg_of_sum_smul_root_mem, pi_Ico_mem_nhds, Set.image_mulSingle_Ioo_right, lt_def, Fintype.prod_mono', Fintype.one_lt_prod_iff_of_one_le, supConvergenceClass', Set.image_update_Icc, conjneg_pos, Real.volume_Icc_pi, Set.image_update_Ico_right, Fintype.sum_mono, Finset.piecewise_mem_Icc', CategoryTheory.Triangulated.TStructure.le_monotone, Set.image_single_Icc_left, lt_of_strongLT, Set.image_update_Icc_left, Function.const_strictMono, Set.pi_univ_Ioo_subset, Set.image_single_Ioc, Real.volume_Icc_pi_toReal, instNeBotNhdsWithinIoi, card_Ioc, card_Icc, instBoundedLENhdsClass, instNeBotNhdsWithinIio, covBy_iff_antisymmRel, Set.pi_univ_Iic, StrongLT.lt, AddGroupSeminorm.coe_lt_coe, ExpGrowth.expGrowthInf_monotone, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable_of_equiv, Set.image_mulSingle_Ioo_left, NonarchAddGroupSeminorm.lt_def, Set.image_mulSingle_Icc, closure_upperClosure_comm_pi, OrderHom.pi_coe, Set.Icc_diff_pi_univ_Ioc_subset, CircleDeg1Lift.iterate_monotone, NonarchAddGroupSeminorm.coe_lt_coe, covBy_iff, card_Iio, Function.one_lt_const, instPosSMulReflectLE, Set.Icc_diff_pi_univ_Ioo_subset, pi_Ioc_mem_nhds, CategoryTheory.ObjectProperty.galoisConnection_isColocal, Set.image_mulSingle_Icc_left, antitone_lam, wellFoundedLT, AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_mono, pi_Ici_mem_nhds', Finsupp.coe_strictMono, MeasureTheory.hittingBtwn_anti, Set.image_single_Ioo_left, Set.ordConnected_pi, MeasureTheory.Measure.univ_pi_Ico_ae_eq_Icc, lt_update_self_iff, Set.image_single_Ioo_right, pi_Ioi_mem_nhds', MeasureTheory.Measure.univ_pi_Ioi_ae_eq_Ici, ωScottContinuous_uncurry, Nucleus.coe_lt_coe, RootPairing.Base.not_nonpos_iff_pos_of_sum_mem_range_root, dist_mono_left_pi, BoxIntegral.Box.Icc_def, mem_parallelepiped_iff, GaloisConnection.dfun, Function.wellFoundedLT, instSMulPosReflectLT, Fin.preimage_insertNth_Icc_of_notMem, Fintype.sum_pos_iff_of_nonneg, instSMulPosStrictMono, Set.piecewise_mem_Icc, compact_Icc_space', BoxIntegral.Box.monotone_upper, wcovBy_iff_antisymmRel, Set.image_single_Ioo, instOrderClosedTopologyForall, OrdinalApprox.lfpApprox_mono_left, Set.image_update_Ioc_right, Fintype.sum_strictMono, Set.image_single_Icc_right, card_Ico, instPosSMulMono, isAtom_iff_eq_single, monotoneUncurry_coe, Part.fix_eq_ωSup, MeasureTheory.monotone_lintegral, instNoMaxOrderForallOfNonempty, pi_Iio_mem_nhds', CategoryTheory.Triangulated.TStructure.ge_antitone, wcovBy_iff_exists_left_eq, antitone_iff_apply₂, Set.pi_univ_Ioc_subset, isAtom_iff, Set.image_update_Ioc_left, Fintype.sum_neg_iff_of_nonpos, Set.image_mulSingle_Ico_left, tendstoIccClassNhdsPi, pi_Iic_mem_nhds, Part.ωScottContinuous_toUnitMono, OrdinalApprox.gfpApprox_mono_mid, GroupNorm.lt_def, Set.image_single_Ico_left, monotoneCurry_coe, RootPairing.Base.exists_root_eq_sum_int, Function.const_pos, Fin.insertNth_mem_Icc, toColex_strictMono, mulSingle_strictMono, Set.pi_univ_Ioi_subset, Function.const_mono, instBoundedGENhdsClass, instCompactIccSpaceForall, DFinsupp.coe_strictMono, MeasureTheory.Measure.univ_pi_Iio_ae_eq_Iic, Set.image_mulSingle_Ioc_right, monotone_iff_apply₂, Finsupp.coe_lt_coe, instSMulPosMono, infConvergenceClass, Function.const_lt_const, OrdinalApprox.gfpApprox_mono_left, covBy_iff_exists_left_eq, Monotone.of_apply₂, Set.image_single_Ico, NonarchAddGroupNorm.lt_def, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mono, dist_anti_right_pi, Set.image_update_Ico_left, Set.image_single_Icc, Part.Fix.approx_mono', instDenselyOrderedForall, OrderHom.coeFnHom_coe, Finset.piecewise_mem_Icc, Set.ordConnected_pi', GroupNorm.coe_lt_coe, Cycle.chain_mono, Set.image_single_Ioc_left, Set.pi_univ_Ici, Set.image_update_Ico, MeasureTheory.SimpleFunc.mk_lt_mk, Set.image_mulSingle_Ico_right, pi_Ici_mem_nhds, ωScottContinuous_curry, dist_mono_right_pi, wcovBy_iff_exists_right_eq, uncurry_curry_ωScottContinuous, pi_Ioc_mem_nhds', Part.Fix.mem_iff, infConvergenceClass', instSMulPosReflectLE, OrderHom.piIso_apply, update_lt_self_iff, AddGroupNorm.lt_def, evalOrderHom_coe, Function.monotone_iterate_of_id_le, pi_Icc_mem_nhds, Set.image_update_Ioc, Set.image_single_Ico_right, pi_Ioi_mem_nhds, Set.image_update_Ioo_left, CategoryTheory.ObjectProperty.galoisConnection_isLocal, single_strictMono, Set.image_single_Ioc_right, Fintype.prod_strictMono', TorusIntegrable.function_integrable, Seminorm.coe_lt_coe, Set.image_mulSingle_Ioc, IsClosed.upperClosure_pi, Finsupp.coe_mono, AddGroupNorm.coe_lt_coe, pi_Ioo_mem_nhds', Part.fix_eq_ωSup_of_ωScottContinuous, pi_Icc_mem_nhds', NonarchAddGroupNorm.coe_lt_coe, MeasureTheory.upcrossingsBefore_mono, Fintype.prod_lt_one_iff_of_le_one, supConvergenceClass, DFinsupp.coe_lt_coe, AlgebraicGeometry.Scheme.IdealSheafData.strictMono_ideal, Set.image_mulSingle_Ico, AddGroupSeminorm.lt_def, instNoMinOrderForallOfNonempty, Function.const_neg', MeasureTheory.hittingAfter_anti, Antitone.of_apply₂, Set.pi_univ_Iio_subset, closure_lowerClosure_comm_pi, mulSingle_mono, ExpGrowth.expGrowthSup_monotone, conjneg_neg', Function.const_lt_one, Set.image_mulSingle_Ioc_left, card_Ioo, card_Ioi, Set.image_update_Ioo_right, GroupSeminorm.coe_lt_coe, Icc_eq, OrderHom.partBind_coe, toLex_strictMono, Function.locallyFinsuppWithin.lt_def, monotone_lam, Set.image_update_Icc_right, Part.Fix.approx_mono, dist_anti_left_pi, Behrend.map_monotone, BoxIntegral.Box.antitone_lower, Set.pi_univ_Icc, isAtom_single, Set.pi_univ_Ico_subset, toLex_monotone
sdiff 📖	CompOp	7 math math: symmDiff_def, symmDiff_apply, sdiff_def, Set.sigma_diff_sigma, MeasureTheory.ae_eq_set_symmDiff, sdiff_apply, MeasureTheory.ae_eq_set_diff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compl_apply 📖	mathematical	—	Compl.compl instCompl	—	—
compl_def 📖	mathematical	—	Compl.compl instCompl	—	—
le_def 📖	mathematical	—	hasLe	—	—
lt_def 📖	mathematical	—	Preorder.toLT preorder hasLe Preorder.toLE	—	—
sdiff_apply 📖	mathematical	—	sdiff	—	—
sdiff_def 📖	mathematical	—	sdiff	—	—

Preorder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	toLE	—	—	toLE_injective LE.ext
toLE_injective 📖	mathematical	—	Preorder toLE	—	—
toLE_injective_iff 📖	mathematical	—	toLE	—	toLE_injective

Prod

Definitions

Name	Category	Theorems
instDecidableLE 📖	CompOp	11 math math: SchwartzMap.norm_toLp_le_seminorm, IncidenceAlgebra.eulerChar_prod, Int.card_box, IncidenceAlgebra.zeta_prod_apply, SchwartzMap.eLpNorm_le_seminorm, Int.existsUnique_mem_box, Int.mem_box, IncidenceAlgebra.mu_prod_mu, SchwartzMap.one_add_le_sup_seminorm_apply, IncidenceAlgebra.zeta_prod_mk, IncidenceAlgebra.zeta_prod_zeta
instLE_mathlib 📖	CompOp	114 math math: bddAbove_range_prod, GCongr.mk_le_mk, IncidenceAlgebra.prod_mk, LowerSet.inf_prod, LowerSet.sup_prod, IsLowerSet.prod, instCanonicallyOrderedMul, LowerSet.prod_mono, LowerSet.prod_self_lt_prod_self, OmegaCompletePartialOrder.Chain.pair_zip_pair, LowerSet.bot_prod, instZeroLEOneClass, OrderHom.prodIso_apply, OrderIso.prodAssoc_apply, Fin.insertNthOrderIso_symm_apply, NonemptyInterval.toDualProdHom_apply, Fin.insertNthOrderIso_toEquiv, UpperSet.prod_le_prod_iff, lowerClosure_prod, orderedSub, LowerSet.prod_mono_left, UpperSet.coe_prod, UpperSet.prod_top, UpperSet.top_prod, IsLUB.prod, bddAbove_prod, Filter.EventuallyLE.prodMap, swap_le_swap, UpperSet.Ici_prod_Ici, isTop_iff, UpperSet.prod_mono_left, isBot_iff, mk_le_swap, IsMax.prodMk, IncidenceAlgebra.prod_apply, IsMin.prodMk, instExistsMulOfLE, Sublattice.prodEquiv_toEquiv, bddBelow_prod, YoungDiagram.isLowerSet, IncidenceAlgebra.zeta_prod_apply, Sublattice.prodEquiv_apply, UpperSet.sup_prod, OrderIso.prodAssoc_symm_apply, LowerSet.disjoint_prod, Fin.snocOrderIso_apply, LowerSet.top_prod_top, isMax_iff, Ideal.idealProdEquiv_symm_apply, Fin.snocOrderIso_symm_apply, OrderIso.coe_prodComm, Filter.EventuallyLE.prodMap_nhds, LowerSet.coe_prod, Fin.consOrderIso_apply, lowerBounds_prod, isLUB_prod, upperClosure_prod, UpperSet.prod_inf, UpperSet.prod_mono, LowerSet.prod_mono_right, UpperSet.prod_self_le_prod_self, Fin.consOrderIso_symm_apply, Antisymmetrization.prodEquiv_symm_apply_mk, instExistsAddOfLE, UpperSet.prod_self_lt_prod_self, swap_le_mk, IncidenceAlgebra.one_prod_one, instCanonicallyOrderedAdd, LowerSet.prod_self_le_prod_self, LowerSet.prod_eq_bot, Finset.sumEquiv_apply_snd, Fin.insertNthOrderIso_apply, Fin.consOrderIso_toEquiv, LowerSet.prod_sup, LowerSet.prod_le_prod_iff, UpperSet.mem_prod, OrderIso.prodComm_symm, LowerSet.prod_bot, LowerSet.prod_inf_prod, IsGLB.prod, LowerSet.Iic_prod, upperBounds_prod, Fin.snocOrderIso_toEquiv, IsUpperSet.prod, UpperSet.bot_prod_bot, isMin_iff, isGLB_prod, Antisymmetrization.prodEquiv_apply_mk, LowerSet.prod_inf, OrderHom.prodIso_symm_apply, Finset.sumEquiv_apply_fst, IncidenceAlgebra.prod_mul_prod', UpperSet.prod_sup_prod, UpperSet.prod_mono_right, mk_le_mk, instWellQuasiOrderedLEProd, UpperSet.codisjoint_prod, LowerSet.mem_prod, UpperSet.inf_prod, IsTop.prodMk, le_def, mk_le_mk_iff_right, IncidenceAlgebra.prod_mul_prod, Sublattice.prodEquiv_symm_apply, IncidenceAlgebra.zeta_prod_mk, Finset.sumEquiv_symm_apply, UpperSet.prod_eq_top, IncidenceAlgebra.zeta_prod_zeta, UpperSet.Ici_prod, IsBot.prodMk, bddBelow_range_prod, mk_le_mk_iff_left, UpperSet.prod_sup, LowerSet.Ici_prod_Ici
instPartialOrder 📖	CompOp	19 math math: instIsOrderedRingProd, instStarOrderedRing, instIsOrderedMonoid, CFC.sqrt_map_prod, Int.card_box, codisjoint_iff, instOrderedSMulProd, CFC.rpow_map_prod, instIsOrderedCancelMonoid, instIsOrderedAddCancelMonoid, Int.existsUnique_mem_box, Int.mem_box, card_box_succ, CFC.nnrpow_eq_nnrpow_prod, disjoint_iff, instIsOrderedAddMonoid, isCompl_iff, CFC.rpow_eq_rpow_prod, CFC.nnrpow_map_prod
instPreorder 📖	CompOp	215 math math: SchwartzMap.norm_toLp_le_seminorm, NonemptyInterval.toDualProd_mono, OrderMonoidHom.inl_mul_inr_eq_mk, mk_lt_mk_of_le_of_lt, instCompactIccSpaceProd, monotone_fst, Finset.Ioo_map_sectR, Finset.Icc_map_sectL, MeasureTheory.Lp.cauchySeq_Lp_iff_cauchySeq_eLpNorm, ScottContinuous.prodMk, IncidenceAlgebra.eulerChar_prod, OrderAddMonoidHom.inl_apply, cauchySeq_iff', AddMonoidHom.inl_strictMono, cauchySeq_iff_tendsto_dist_atTop_0, Finset.card_Iic_prod, OmegaCompletePartialOrder.Chain.pair_zip_pair, Filter.Tendsto.prod_map_prod_atTop, OrderAddMonoidHom.fst_comp_inl, ScottContinuousOn.snd, SSet.prodStdSimplex.objEquiv_apply_fst, Lex.toLexOrderHom_coe, OrderHom.prodIso_apply, MonoidWithZeroHom.fst_mono, OrderHom.snd_coe, Set.Iic_prod_eq, lt_of_lt_of_le, Topology.instIsLowerProd, mk_wcovBy_mk_iff_right, monotone_prod_iff, MonoidHom.inr_mono, OmegaCompletePartialOrder.Chain.zip_coe, ScottContinuous.inf₂, instNeBotNhdsWithinIio, SSet.prodStdSimplex.strictMono_orderHomOfSimplex_iff, mk_covBy_mk_iff_right, Set.IsPWO.prod, CauchySeq.prodMap, SSet.prodStdSimplex.objEquiv_δ_apply, lowerClosure_prod, OrderAddMonoidHom.addCommute_inl_inr, SSet.prodStdSimplex.objEquiv_naturality, Submodule.strictMono_comap_prod_map, Monotone.prodMk, MonoidWithZeroHom.inl_strictMono, OrderHom.prodMap_coe, instNeBotNhdsWithinIoi, wellFoundedLT, OrderMonoidHom.commute_inl_inr, SimpleGraph.hasse_prod, StrictAnti.prodMap, SSet.prodStdSimplex.objEquiv_apply_snd, monotone_prodMk_iff, Filter.prod_map_atTop_eq, wellFoundedGT', Filter.tendsto_atTop_diagonal, QuotientAddGroup.strictMono_comap_prod_image, instDenselyOrderedProd, instBoundedLENhdsClass, ScottContinuousOn.sup₂, instPosSMulReflectLE, UpperSet.Ici_prod_Ici, lt_of_le_of_lt, NonemptyInterval.toDualProd_strictMono, Filter.tendsto_finset_prod_atTop, instIsOrderBornology, StrictMono.prodMap, ScottContinuous.fst, AddMonoidHom.snd_mono, OrderHom.prod_coe, noMinOrder_of_left, QuotientAddGroup.strictMono_comap_prod_map, ScottContinuousOn.fst, Finset.Ioc_map_sectL, swap_wcovBy_swap, antitone_prod_iff, OrderHom.comp_prod_comp_same, OrderHom.snd_comp_prod, AddMonoidHom.inr_mono, ScottContinuous.prod, covBy_iff, noMaxOrder_of_right, Filter.Tendsto.prod_atTop, Filter.tendsto_atBot_diagonal, ScottContinuous.fromProd, wcovBy_iff, MonoidHom.inl_mono, HasFPowerSeriesAt.tendsto_partialSum_prod_of_comp, OrderHom.prod_mono, Set.Ici_prod_eq, mk_covBy_mk_iff_left, MonoidWithZeroHom.inr_mono, swap_covBy_swap, AddMonoidHom.inl_mono, mk_lt_mk_of_lt_of_le, QuotientGroup.strictMono_comap_prod_image, Finset.Ioo_map_sectL, SchwartzMap.eLpNorm_le_seminorm, wellFoundedGT, OrderHom.curry_apply, instInfConvergenceClassProd, SSet.prodStdSimplex.objEquiv_map_apply, swap_lt_swap, upperClosure_prod, lt_iff, Finset.Ici_prod_def, ScottContinuousOn.prodMk, Filter.instIsCountablyGeneratedAtTopProd, Monotone.prodMap, Finset.Icc_prod_def, OrderAddMonoidHom.snd_comp_inr, Antisymmetrization.prodEquiv_symm_apply_mk, instSMulPosStrictMono, Nat.pow_monotoneOn, Finset.Ioc_map_sectR, IncidenceAlgebra.one_prod_one, MonoidWithZeroHom.snd_mono, instSMulPosReflectLE, Finset.Ici_product_Ici, MonoidHom.fst_mono, OrderMonoidHom.snd_comp_inl, mk_lt_mk_iff_right, noMaxOrder_of_left, OrderMonoidHom.snd_apply, OrderMonoidHom.inl_apply, AddMonoidHom.fst_mono, Lex.toLex_mono, Topology.instIsUpperProd, Set.Icc_prod_eq, ScottContinuous.sup₂, OrderHom.fst_prod_snd, OrderHom.diag_coe, OrderHom.fst_comp_prod, OrderAddMonoidHom.inr_apply, instPosSMulMono, MonoidHom.inl_strictMono, SSet.prodStdSimplex.nonDegenerate_iff_injective_objEquiv, OrderHom.fst_coe, mk_wcovBy_mk_iff, OrderMonoidHom.fst_apply, Filter.eventually_atBot_prod_self', OrderMonoidHom.snd_comp_inr, OrderHom.curry_symm_apply, OrderAddMonoidHom.fst_comp_inr, OrderHom.prodₘ_coe_coe_coe, ωSup_snd, MonoidHom.inr_strictMono, Lex.toLex_strictMono, mk_covBy_mk_iff, supConvergenceClass, monotone_snd, MonoidWithZeroHom.inr_strictMono, Finset.Ico_map_sectR, OrderAddMonoidHom.inl_add_inr_eq_mk, ωSupImpl_fst, Filter.prod_atTop_atTop_eq, noMinOrder_of_right, LowerSet.Iic_prod, OrderAddMonoidHom.snd_apply, SSet.prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv, swap_lt_mk, Antitone.prodMap, Filter.prod_atBot_atBot_eq, MonoidWithZeroHom.inl_mono, Finset.card_Ici_prod, CauchySeq.tendsto_uniformity, Finset.card_Icc_prod, Finset.Iic_product_Iic, Antisymmetrization.prodEquiv_apply_mk, OrderAddMonoidHom.snd_comp_inl, Filter.eventually_atTop_prod_self, OrderHom.prodIso_symm_apply, IncidenceAlgebra.prod_mul_prod', ScottContinuous.snd, mk_lt_mk_iff_left, Filter.prod_map_atBot_eq, cauchySeq_iff_tendsto, OrderMonoidHom.fst_comp_inr, Finset.Ico_map_sectL, instSMulPosReflectLT, Set.Ici_prod_Ici, Filter.instIsCountablyGeneratedAtBotProd, ScottContinuousOn.fromProd, ωSup_fst, mk_lt_mk, instOrderClosedTopologyProd, Filter.Tendsto.prod_atBot, OrderMonoidHom.inr_apply, IncidenceAlgebra.mu_prod_mu, Finset.Icc_product_Icc, Set.Icc_prod_Icc, OrderAddMonoidHom.fst_apply, strictMono_inf_prod_sup, OrderMonoidHom.fst_comp_inl, AddMonoidHom.inr_strictMono, Set.Iic_prod_Iic, Finset.Iic_prod_def, mk_lt_swap, QuotientGroup.strictMono_comap_prod_map, instBoundedGENhdsClass, wellFoundedLT', MonoidHom.snd_mono, ωSupImpl_snd, IncidenceAlgebra.prod_mul_prod, mk_wcovBy_mk_iff_left, SchwartzMap.one_add_le_sup_seminorm_apply, instSMulPosMono, FormalMultilinearSeries.compPartialSumTarget_tendsto_prod_atTop, Filter.eventually_atTop_prod_self', instPosSMulStrictMono, Finset.Icc_map_sectR, UpperSet.Ici_prod, Filter.Tendsto.prod_map_prod_atBot, Filter.eventually_atBot_prod_self, LowerSet.Ici_prod_Ici

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_def 📖	mathematical	—	instLE_mathlib	—	—
lt_iff 📖	mathematical	—	Preorder.toLT instPreorder Preorder.toLE	—	LE.le.lt_of_not_ge LT.lt.le LT.lt.not_ge
lt_of_le_of_lt 📖	mathematical	Preorder.toLE Preorder.toLT	instPreorder	—	—
lt_of_lt_of_le 📖	mathematical	Preorder.toLT Preorder.toLE	instPreorder	—	—
mk_le_mk 📖	mathematical	—	instLE_mathlib	—	—
mk_le_mk_iff_left 📖	mathematical	—	instLE_mathlib Preorder.toLE	—	le_rfl
mk_le_mk_iff_right 📖	mathematical	—	instLE_mathlib Preorder.toLE	—	le_rfl
mk_le_swap 📖	mathematical	—	instLE_mathlib	—	—
mk_lt_mk 📖	mathematical	—	Preorder.toLT instPreorder Preorder.toLE	—	lt_iff
mk_lt_mk_iff_left 📖	mathematical	—	Preorder.toLT instPreorder	—	lt_iff_lt_of_le_iff_le' mk_le_mk_iff_left
mk_lt_mk_iff_right 📖	mathematical	—	Preorder.toLT instPreorder	—	lt_iff_lt_of_le_iff_le' mk_le_mk_iff_right
mk_lt_mk_of_le_of_lt 📖	mathematical	Preorder.toLE Preorder.toLT	instPreorder	—	—
mk_lt_mk_of_lt_of_le 📖	mathematical	Preorder.toLT Preorder.toLE	instPreorder	—	—
mk_lt_swap 📖	mathematical	—	Preorder.toLT instPreorder	—	swap_lt_swap
swap_le_mk 📖	mathematical	—	instLE_mathlib	—	—
swap_le_swap 📖	mathematical	—	instLE_mathlib	—	—
swap_lt_mk 📖	mathematical	—	Preorder.toLT instPreorder	—	swap_lt_swap
swap_lt_swap 📖	mathematical	—	Preorder.toLT instPreorder	—	swap_le_swap

Prod.GCongr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_le_mk 📖	mathematical	—	Prod.instLE_mathlib	—	—

Prop

Definitions

Name	Category	Theorems
instCompl 📖	CompOp	31 math math: compl_le, isAntichain_union, MeasureTheory.ae_eq_set_compl, compl_iff_not, CategoryTheory.Limits.kernelForkBiproductToSubtype_cone, Std.Irrefl.compl, CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype_isColimit, MeasureTheory.NullMeasurableSet.compl_toMeasurable_compl_ae_eq, Ordinal.cof_type, MeasureTheory.ae_eq_set_compl_compl, Std.Refl.compl, CategoryTheory.Limits.kernelBiproductToSubtypeIso_hom, Symmetric.compl, RelIso.compl_apply, antisymmRel_compl_apply, compl_ge, Relation.cutExpand_le_invImage_lex, CategoryTheory.Limits.cokernelBiproductFromSubtypeIso_hom, RelIso.compl_symm_apply, incompRel_compl_apply, SimpleGraph.cliqueFreeOn_two, antisymmRel_compl, Ne.instIsEquiv_compl, compl_lt, CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype_cocone, incompRel_compl, Heyting.isRegular_of_decidable, CategoryTheory.Limits.cokernelBiproductFromSubtypeIso_inv, compl_gt, CategoryTheory.Limits.kernelForkBiproductToSubtype_isLimit, CategoryTheory.Limits.kernelBiproductToSubtypeIso_inv
le 📖	CompOp	84 math math: CategoryTheory.ObjectProperty.isoModSerre_isInvertedBy_iff, CategoryTheory.ObjectProperty.le_limitsClosure, le_total, Prod.rprod_le_transGen_gameAdd, CategoryTheory.ObjectProperty.le_shiftClosure, CategoryTheory.ObjectProperty.le_isoClosure, CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.colimitsOfShape_le, CategoryTheory.exactFunctor_le_additiveFunctor, SimpleGraph.Reachable.mono', CategoryTheory.IsCardinalLocallyPresentable.iff_exists_isStrongGenerator, Prod.gameAdd_le_lex, Filter.set_eventuallyLE_iff_inf_principal_le, Sym2.fromRel_mono_iff, MeasureTheory.union_ae_eq_left_iff_ae_subset, CategoryTheory.ObjectProperty.op_monotone_iff, AlgebraicGeometry.IsLocalIso.le_of_isZariskiLocalAtSource, bot_eq_false, CategoryTheory.ObjectProperty.colimitsOfShape_le_of_final, CategoryTheory.Localization.LeftBousfield.le_W_iff, TopologicalSpace.le_def, blimsup_cthickening_ae_le_of_eventually_mul_le_aux, Filter.set_eventuallyLE_iff_mem_inf_principal, CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le', MeasureTheory.vadd_set_ae_le, CategoryTheory.isCardinalPresentable_monotone, CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.le_isCardinalPresentable, blimsup_cthickening_ae_le_of_eventually_mul_le, CategoryTheory.ObjectProperty.strictLimitsOfShape_le_limitsOfShape, MeasureTheory.ae_le_toMeasurable, CategoryTheory.ObjectProperty.ofObj_le_iff, AlgebraicGeometry.IsLocalIso.le_of_isLocalAtSource, CategoryTheory.ObjectProperty.le_strictLimitsClosureStep, CategoryTheory.leftExactFunctor_le_additiveFunctor, CategoryTheory.ObjectProperty.strictLimitsClosureIter_le_limitsClosure, HasSubset.Subset.eventuallyLE, CategoryTheory.ObjectProperty.shiftClosure_le_iff, subrelation_iff_le, Set.setOf_bot, extend_partialOrder, Relation.cutExpand_le_invImage_lex, CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff, CategoryTheory.ObjectProperty.le_isLocal_iff, CategoryTheory.ObjectProperty.isoClosure_le_iff, CategoryTheory.ObjectProperty.strictMap_le_map, CategoryTheory.ObjectProperty.le_isLocal_isLocal, CategoryTheory.ObjectProperty.le_isColocal_iff, MeasureTheory.union_ae_eq_right_iff_ae_subset, CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le, CategoryTheory.ObjectProperty.le_colimitsClosure, CategoryTheory.ObjectProperty.retractClosure_le_iff, instIsSimpleOrderProp, MeasurableSpace.le_def, CategoryTheory.ObjectProperty.unop_monotone_iff, le_Prop_eq, CategoryTheory.ObjectProperty.IsStableUnderShiftBy.le_shift, CategoryTheory.Triangulated.TStructure.le_zero_le, CategoryTheory.ObjectProperty.le_def, CategoryTheory.ObjectProperty.le_kernel_of_isoModSerre_isInvertedBy, IsWellFounded.exists_well_order_ge, CategoryTheory.exactFunctor_le_leftExactFunctor, CategoryTheory.ObjectProperty.le_isColocal_isColocal, HomotopicalAlgebra.bifibrantObjects_le_fibrantObject, CategoryTheory.ObjectProperty.singleton_le_iff, CategoryTheory.ObjectProperty.le_ind, MeasureTheory.Measure.exists_ae_subset_biUnion_countable, MeasureTheory.smul_set_ae_le, CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.limitsOfShape_le, CategoryTheory.ObjectProperty.limitsOfShape_le_of_initial, SimpleGraph.adj_le_reachable, CategoryTheory.Triangulated.TStructure.ge_one_le, CategoryTheory.ObjectProperty.strictColimitsOfShape_le_colimitsOfShape, HomotopicalAlgebra.bifibrantObjects_le_cofibrantObject, CategoryTheory.rightExactFunctor_le_additiveFunctor, CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_iff, MeasurableSpace.DynkinSystem.le_def, CategoryTheory.ObjectProperty.le_retractClosure, CategoryTheory.ObjectProperty.le_isLocal_W, CategoryTheory.exactFunctor_le_rightExactFunctor, CategoryTheory.ObjectProperty.le_strictLimitsClosureIter, Set.setOf_top, MeasureTheory.ae_le_set, top_eq_true, CategoryTheory.ObjectProperty.le_colimitsCardinalClosure, CategoryTheory.ObjectProperty.le_shift
partialOrder 📖	CompOp	40 math math: antitone_continuousOn, codisjoint_iff, Topology.IsScott.isOpen_iff_scottContinuous_mem, CategoryTheory.Localization.LeftBousfield.galoisConnection, t2Space_antitone, isCoatom_iff, antitone_le, CategoryTheory.Triangulated.TStructure.le_monotone, Subalgebra.separatesPoints_monotone, Filter.monotone_mem, instIsUpperProp, t1Space_antitone, isCompl_iff, CategoryTheory.ObjectProperty.galoisConnection_isColocal, Set.monotone_mem, Set.antitone_bforall, Set.Ioi_True, disjoint_iff, isAtom_iff, instWellFoundedLT, isLowerSet_setOf, CategoryTheory.Triangulated.TStructure.ge_antitone, Algebra.Norm.Transitivity.mul_auxMat_blockTriangular, monotone_le, Set.Iic_False, Set.Iio_True, Set.antitone_mem, Set.Iic_True, isUpperSet_setOf, Set.Ioi_False, Set.Ici_False, Set.Ici_True, Cycle.chain_mono, antitone_lt, Set.Iio_False, monotone_lt, CategoryTheory.ObjectProperty.galoisConnection_isLocal, Algebra.Norm.Transitivity.auxMat_blockTriangular, instWellFoundedGT, Topology.IsUpperSet.instProp

Std.Irrefl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compl 📖	mathematical	—	Compl.compl Pi.instCompl Prop.instCompl	—	—

Std.Refl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compl 📖	mathematical	—	Compl.compl Pi.instCompl Prop.instCompl	—	—

StrongLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le 📖	mathematical	StrongLT Preorder.toLT	Pi.hasLe Preorder.toLE	—	le_of_strongLT
lt 📖	mathematical	StrongLT Preorder.toLT	Pi.preorder	—	lt_of_strongLT
trans_le 📖	—	StrongLT Preorder.toLT Pi.hasLe Preorder.toLE	—	—	strongLT_of_strongLT_of_le

Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDenselyOrdered 📖	mathematical	—	DenselyOrdered	—	LT.lt.trans_eq

Subtype

Definitions

Name	Category	Theorems
decidableLE 📖	CompOp	—
decidableLT 📖	CompOp	6 math math: HahnEmbedding.Partial.truncLT_mem_range_extendFun, HahnEmbedding.IsPartial.truncLT_mem_range, HahnEmbedding.Partial.truncLT_mem_range_sSupFun, HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding, HahnEmbedding.Partial.eval_eq_truncLT, HahnEmbedding.Partial.truncLT_eval_mem_range_extendFun
instLinearOrder 📖	CompOp	40 math math: HahnEmbedding.Seed.baseEmbedding_pos, SSet.horn₃₁.desc.multicofork_π_two, SSet.horn₃₂.desc.multicofork_π_one, CategoryTheory.TransfiniteCompositionOfShape.iic_isoBot, HahnEmbedding.Partial.archimedeanClassMk_eq_iff, HahnEmbedding.Seed.baseEmbedding_strictMono, HahnEmbedding.Partial.toOrderAddMonoidHom_apply, CategoryTheory.TransfiniteCompositionOfShape.ici_F, SSet.horn₃₁.desc.multicofork_pt, HahnEmbedding.Partial.extendFun_strictMono, CategoryTheory.Limits.instHasIterationOfShapeElemIic, CategoryTheory.TransfiniteCompositionOfShape.iic_isColimit, HahnEmbedding.IsPartial.strictMono, unitInterval.volume_uIoo, SSet.horn₃₁.desc.multicofork_π_two_assoc, SSet.horn₃₁.desc.multicofork_π_zero_assoc, Set.image_subtype_val_uIoo, Set.image_subtype_val_uIoc, CategoryTheory.TransfiniteCompositionOfShape.ici_isoBot, CategoryTheory.TransfiniteCompositionOfShape.iic_F, CategoryTheory.TransfiniteCompositionOfShape.ici_isColimit, SSet.horn₃₂.desc.multicofork_π_zero_assoc, hahnEmbedding_isOrderedModule_rat, SSet.horn₃₁.desc.multicofork_π_three_assoc, SSet.horn₃₁.desc.multicofork_π_zero, CategoryTheory.TransfiniteCompositionOfShape.iic_incl_app, HahnEmbedding.Partial.eval_lt, SSet.horn₃₂.desc.multicofork_π_three, SSet.horn₃₂.desc.multicofork_pt, HahnEmbedding.Partial.sSupFun_strictMono, unitInterval.volume_uIoc, SSet.horn₃₂.desc.multicofork_π_zero, SSet.horn₃₂.desc.multicofork_π_three_assoc, SSet.horn₃₂.desc.multicofork_π_one_assoc, CategoryTheory.TransfiniteCompositionOfShape.ici_incl, SSet.horn₃₁.desc.multicofork_π_three, hahnEmbedding_isOrderedAddMonoid, Set.image_subtype_val_uIcc, hahnEmbedding_isOrderedModule, HahnEmbedding.Partial.toOrderAddMonoidHom_injective
partialOrder 📖	CompOp	101 math math: AddSubmonoid.toIsOrderedCancelAddMonoid, HahnEmbedding.IsPartial.baseEmbedding_le, Submodule.toIsOrderedAddMonoid, MeasureTheory.Lp.instIsOrderedAddMonoid, Nonneg.isStrictOrderedRing, Set.Iic.isCompactElement, Subsemiring.toIsOrderedRing, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, SubmonoidClass.toIsOrderedMonoid, Module.End.invtSubmodule.disjoint_mk_iff, Nonneg.isOrderedRing, Subring.toIsOrderedRing, CategoryTheory.TransfiniteCompositionOfShape.iic_isoBot, HahnEmbedding.Partial.archimedeanClassMk_eq_iff, HahnEmbedding.Seed.baseEmbedding_strictMono, isAtomic_iff_forall_isAtomic_Iic, Set.Icc.disjoint_iff, Set.Iic.isCompl_inf_inf_of_isCompl_of_le, Nonneg.segment_eq_uIcc, HahnEmbedding.Partial.toOrderAddMonoidHom_apply, Set.Icc.codisjoint_iff, HahnEmbedding.Partial.orderTop_eq_iff, Subsemiring.toIsStrictOrderedRing, CategoryTheory.TransfiniteCompositionOfShape.iic_isColimit, HahnEmbedding.IsPartial.strictMono, CompleteLattice.Iic_coatomic_of_compact_element, Module.End.invtSubmodule.isCompl_iff, HahnEmbedding.IsPartial.truncLT_mem_range, Subring.toIsStrictOrderedRing, Complementeds.codisjoint_coe, IsAtomic.Set.Iic.isAtomic, AddSubmonoidClass.toIsOrderedCancelAddMonoid, isCoatomic_iff_forall_isCoatomic_Ici, CategoryTheory.Functor.IsWellOrderContinuous.nonempty_isColimit, CompleteSublattice.codisjoint_iff, Set.Iic.disjoint_iff, CategoryTheory.SmallObject.coconeOfLE_pt, CompleteSublattice.isCompl_iff, HahnEmbedding.Partial.eval_smul, Nonneg.instArchimedean, Set.Ici.disjoint_iff, Set.Ici.codisjoint_iff, AddSubgroup.toIsOrderedAddMonoid, Valued.integer.mulArchimedean_mrange_of_isCompact_integer, Subalgebra.toIsStrictOrderedRing, SubsemiringClass.toIsOrderedRing, IsCoatomic.Set.Ici.isCoatomic, CategoryTheory.TransfiniteCompositionOfShape.iic_F, Set.Icc.isCompl_iff, CategoryTheory.SmallObject.restrictionLE_map, Positive.isOrderedMonoid, CategoryTheory.Functor.IsWellOrderContinuous.restriction_setIci, HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk, Module.End.invtSubmodule.isCompl_mk_iff, Submonoid.toIsOrderedMonoid, AddSubmonoidClass.instAddArchimedean, SubmonoidClass.toIsOrderedCancelMonoid, hahnEmbedding_isOrderedModule_rat, Subgroup.toIsOrderedMonoid, Submodule.toIsOrderedCancelAddMonoid, Module.End.invtSubmodule.codisjoint_iff, AddSubmonoidClass.toIsOrderedAddMonoid, HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding, Positive.isOrderedCancelMonoid, HahnEmbedding.Partial.mem_domain, Set.Iic.codisjoint_iff, HahnEmbedding.Seed.mem_domain_baseEmbedding, AddSubmonoid.toIsOrderedAddMonoid, CategoryTheory.TransfiniteCompositionOfShape.iic_incl_app, SubmonoidClass.instMulArchimedean, HahnEmbedding.ArchimedeanStrata.archimedean_stratum, Nonneg.isOrderedAddMonoid, Subalgebra.toIsOrderedRing, Submonoid.toIsOrderedCancelMonoid, Nonneg.nat_ceil_coe, Set.Iic.isCompl_iff, Complementeds.isCompl_coe, Module.End.isSemisimple_iff', Set.Ici.isCompl_iff, Nonneg.Icc_subset_segment, CategoryTheory.SmallObject.restrictionLT_map, HahnEmbedding.Partial.eval_zero, CompleteSublattice.disjoint_iff, Nonneg.nat_floor_coe, SubsemiringClass.toIsStrictOrderedRing, CategoryTheory.SmallObject.coconeOfLE_ι_app, Nonneg.instMulArchimedean, HahnEmbedding.Partial.exists_domain_eq_top, Set.Ioc.codisjoint_iff, Module.End.invtSubmodule.codisjoint_mk_iff, HahnEmbedding.Partial.exists_isMax, Set.Ico.disjoint_iff, Module.End.invtSubmodule.disjoint_iff, HahnEmbedding.Seed.domain_baseEmbedding, Subfield.toIsStrictOrderedRing, Complementeds.disjoint_coe, hahnEmbedding_isOrderedAddMonoid, Nonneg.segment_eq_Icc, Nonneg.isOrderedCancelAddMonoid, hahnEmbedding_isOrderedModule, HahnEmbedding.Partial.toOrderAddMonoidHom_injective
preorder 📖	CompOp	327 math math: Submodule.FG.rTensor.directedSystem, Set.image_subtype_val_Ici_Ici, Subring.orderedSubtype_coe, Set.image_subtype_val_Ioi_Ioi, unitInterval.volume_Ioo, unitInterval.volume_Iic, CategoryTheory.SmallObject.SuccStruct.extendToSucc_map_le_succ, Set.preimage_subtype_val_Ioi, Filter.atTop_Ici_eq, SupConvergenceClass.tendsto_coe_atTop_isLUB, unitInterval.strictAnti_symm, comap_coe_Ioi_nhdsGT, ProbabilityTheory.unitInterval.cdf_eq_real, WithBot.subtypeOrderIso_symm_apply, exists_monotone_Icc_subset_open_cover_Icc, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, MeasureTheory.Measure.toSphere_apply_aux, Path.range_subpath_of_ge, Set.Iic.succ_eq_of_not_isMax, Finset.subtype_Ioc_eq, HasCardinalLT.Set.functor_obj, Set.image_subtype_val_Iio_subset, CategoryTheory.SmallObject.SuccStruct.extendToSucc.map_self_succ, Set.strictMonoOn_projIic, unitInterval.volume_Ico, CategoryTheory.SmallObject.SuccStruct.arrowMk_iterationFunctor_map, Submodule.FG.lTensor.directedSystem, covBy_iff_coatom_Iic, Finset.subtype_Ico_eq, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_comap_ideal, comap_coe_nhdsLT_of_Ioo_subset, unitInterval.sigmoid_strictMono, ringKrullDim_quotient, Submonoid.topOrderMonoidIso_symm_apply_coe, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem_obj, Filter.tendsto_Iic_atBot, idealFactorsFunOfQuotHom_comp, Set.image_subtype_val_Ico_subset, HasCardinalLT.Set.cocone_pt, HahnEmbedding.Seed.baseEmbedding_strictMono, CategoryTheory.SmallObject.SuccStruct.ofCocone_map_assoc, CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac_assoc, Set.monotone_projIic, Set.Ici.isAtom_iff, CategoryTheory.SmallObject.SuccStruct.arrowMap_refl, Tuple.monotone_proj, Set.antitoneOn_iff_antitone, OrderHom.Subtype.val_coe, HahnEmbedding.Partial.toOrderAddMonoidHom_apply, Matroid.isClosed_iff_isFlat, CategoryTheory.TransfiniteCompositionOfShape.ici_F, HahnEmbedding.Seed.strictMono_coeff, Set.image_subtype_val_Ico_Iio, SSet.stdSimplex.face_eq_ofSimplex, CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso_hom_naturality_assoc, Set.preimage_subtype_val_Iic, FiniteMulArchimedeanClass.withTopOrderIso_apply_coe, map_coe_Ioo_atBot, Set.image_subtype_val_Ioc_Ici, CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac, HahnEmbedding.Partial.extendFun_strictMono, tendsto_comp_coe_Iio_atTop, CategoryTheory.SmallObject.SuccStruct.restrictionLTOfCoconeIso_inv_app, CategoryTheory.SmallObject.SuccStruct.extendToSucc.map_eq, Filter.atTop_Ioi_eq, Finset.subtype_Iio_eq, Filter.tendsto_comp_val_Iic_atBot, tendsto_Ioi_atBot, CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso_hom_naturality, unitInterval.volume_Ici, Matroid.closure_eq_subtypeClosure, HahnEmbedding.IsPartial.strictMono, MulEquiv.strictMono_subsemigroupCongr, Irrational.instOrderTopologySubtypeReal, Set.image_subtype_val_Iio_Iio, Filter.map_val_Ici_atTop, FiniteArchimedeanClass.liftOrderHom_mk, CategoryTheory.SmallObject.SuccStruct.extendToSuccRestrictionLEIso_hom_app, Set.image_subtype_val_Ioo_Ioi, Set.image_subtype_val_Ici_Iio, CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq.w, CategoryTheory.SmallObject.SuccStruct.extendToSucc_obj_eq, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem_map, Set.monotoneOn_iff_monotone, CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso_hom_naturality, CategoryTheory.SmallObject.SuccStruct.Iteration.obj_bot, CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq.tgt, Set.image_subtype_val_Ioi_subset, Submodule.FG.lTensor.directLimit_apply', instIsStronglyCoatomicElemOfOrdConnected, CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso_hom_naturality_assoc, unitInterval.volume_Icc, unitInterval.range_sigmoid, Submodule.FG.rTensor.directLimit_apply, Set.image_subtype_val_Ico, CategoryTheory.SmallObject.SuccStruct.Iteration.congr_obj, FiniteMulArchimedeanClass.withTopOrderIso_symm_apply, PNat.equivNonZeroDivisorsNat_symm_apply_coe, FiniteMulArchimedeanClass.liftOrderHom_mk, WithTop.subtypeOrderIso_symm_apply, coe_pred_of_mem, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal, Finset.map_subtype_embedding_Ioi, covBy_iff_atom_Ici, CategoryTheory.SmallObject.coconeOfLE_pt, StrictMono.codRestrict, Subsemigroup.strictMono_topEquiv, Order.coheight_eq_krullDim_Ici, Filter.map_val_atTop_of_Ici_subset, mono_coe, Filter.atBot_Iic_eq, AddSubsemigroup.strictMono_topEquiv, IsAtom.Iic, exists_monotone_Icc_subset_open_cover_unitInterval_prod_self, Set.strictMonoOn_projIcc, Order.height_eq_krullDim_Iic, Filter.tendsto_Ioi_atTop, coe_succ_of_mem, AddEquiv.strictMono_subsemigroupCongr, CategoryTheory.SmallObject.SuccStruct.Iteration.obj_succ, CategoryTheory.TransfiniteCompositionOfShape.ici_isoBot, comap_coe_nhdsLT_eq_atTop_iff, CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj_eq, CategoryTheory.SmallObject.SuccStruct.restrictionLTOfCoconeIso_hom_app, Finset.map_subtype_embedding_Ioc, Filter.tendsto_Iio_atBot, CategoryTheory.SmallObject.SuccStruct.arrowι_def, Set.OrdConnected.isSuccArchimedean, Set.image_subtype_val_Iic_Iic, CategoryTheory.SmallObject.restrictionLE_map, CategoryTheory.SmallObject.SuccStruct.arrowMap_ofCocone_to_top, CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj_trans_assoc, map_coe_Ioo_atTop, map_coe_atBot_of_Ioo_subset, map_coe_Ioi_atBot, Set.OrdConnected.isStronglyAtomic, CategoryTheory.SmallObject.SuccStruct.extendToSuccRestrictionLEIso_inv_app, Set.image_subtype_val_Ico_Iic, AlgebraicGeometry.Scheme.IdealSheafData.isLocalization_away, Equiv.image_strictAnti, Set.preimage_subtype_val_Ico, Set.image_subtype_val_Ioc_Iio, Set.preimage_subtype_val_Ioo, CategoryTheory.TransfiniteCompositionOfShape.ici_isColimit, CategoryTheory.SmallObject.SuccStruct.Iteration.arrowSucc_eq, Set.Ici.coe_pred_of_not_isMin, CategoryTheory.SmallObject.SuccStruct.ofCocone_obj_eq_pt, Set.OrdConnected.restrict, CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj_refl, Set.image_subtype_val_Iic_Iio, tendsto_comp_coe_Ioo_atBot, Filter.tendsto_comp_val_Iio_atBot, StrictMonoOn.strictMono, CategoryTheory.SmallObject.SuccStruct.ofCocone_map_to_top, CategoryTheory.Functor.IsWellOrderContinuous.restriction_setIci, Set.strictMonoOn_projIci, Equiv.Set.Equiv.strictMono_setCongr, CategoryTheory.Limits.preservesColimitsOfShape_of_preservesWellOrderContinuousOfShape, Monotone.codRestrict, Set.image_subtype_val_Ioc_Ioi, Set.image_subtype_val_Ioo, Set.image_subtype_val_Iio_Iic, unitInterval.subtype_Ici_eq_Icc, Finset.map_subtype_embedding_Iio, CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq.src, unitInterval.subtype_Iio_eq_Ico, Set.image_subtype_val_Ioo_Ici, MonotoneOn.monotone, HasCardinalLT.Set.cocone_ι_app, hahnEmbedding_isOrderedModule_rat, CategoryTheory.SmallObject.SuccStruct.ofCocone_obj_eq, unitInterval.volume_Ioc, Set.monotone_projIcc, Flag.grade_coe, PNat.equivNonZeroDivisorsNat_apply_coe, Nonneg.instIsOrderedModule, Finset.map_subtype_embedding_Ici, Set.Iic.coe_succ_of_not_isMax, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.arrowMap_functor, Set.image_subtype_val_Iic_subset, FiniteArchimedeanClass.withTopOrderIso_symm_apply, CategoryTheory.SmallObject.SuccStruct.Iteration.obj_limit, Submodule.FG.directedSystem, CategoryTheory.SmallObject.SuccStruct.extendToSucc_map, strictMono_restrict, HasCardinalLT.Set.functor_map_coe, Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer, tendsto_comp_coe_Ioo_atTop, WithBot.subtypeOrderIso_apply_coe, Equiv.image_strictMono, Set.image_subtype_val_Icc_Ici, StrictMonoOn.restrict, instIsStronglyAtomicElemOfOrdConnected, Filter.map_val_Ioi_atTop, Submodule.FG.lTensor.directLimit_apply, Module.fgSystem.equiv_comp_of, Filter.tendsto_comp_val_Ici_atTop, tendsto_Ioo_atBot, Set.image_subtype_val_Ioi_Ici, CategoryTheory.SmallObject.SuccStruct.extendToSucc_obj_succ_eq, Set.Ici.pred_eq_of_not_isMin, Set.image_subtype_val_Ici_Iic, Set.image_subtype_val_Ioc, Tuple.eq_sort_iff', FiniteMulArchimedeanClass.ballSubgroup_strictAnti, idealFactorsFunOfQuotHom_id, Module.exists_ltSeries_support_isMaximal_last_of_ltSeries_support, Set.preimage_subtype_val_Ioc, HasCardinalLT.Set.instIsCardinalFiltered, Valuation.Integers.wellFounded_gt_on_v_iff_discrete_mrange, Set.Icc.monotone_addNSMul, CategoryTheory.SmallObject.SuccStruct.Iteration.congr_map, StrictAntiOn.strictAnti, instOrderClosedTopology, CategoryTheory.SmallObject.SuccStruct.arrowSucc_extendToSucc, MeasureTheory.Lp.instOrderClosedTopologySubtypeAEEqFunMemAddSubgroupOfClosedIciTopology, CategoryTheory.SmallObject.SuccStruct.arrowMap_ofCocone, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor_obj, unitInterval.sigmoid_monotone, Equiv.image_antitone, WithTop.subtypeOrderIso_apply_coe, Monotone.restrict, FiniteArchimedeanClass.ballAddSubgroup_strictAnti, CategoryTheory.Functor.WellOrderInductionData.map_lift, Set.image_subtype_val_Icc_Iio, CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.map_lift, Set.image_subtype_val_Ioc_subset, Matroid.isFlat_iff_isClosed, Set.image_subtype_val_Iio_Ioi, Set.image_subtype_val_Icc_Ioi, Filter.atBot_Iio_eq, Set.OrdConnected.isPredArchimedean, tendsto_Ioo_atTop, Set.image_subtype_val_Ioo_subset, CategoryTheory.SmallObject.restrictionLT_obj, CategoryTheory.Limits.HasIterationOfShape.hasColimitsOfShape_of_isSuccLimit, exists_monotone_Icc_subset_open_cover_unitInterval, CategoryTheory.SmallObject.restrictionLE_obj, Nonneg.Icc_subset_segment, idealFactorsFunOfQuotHom_coe_coe, MeasureTheory.Measure.volumeIoiPow_apply_Iio, Finset.map_subtype_embedding_Ico, FiniteArchimedeanClass.ball_strictAnti, CategoryTheory.SmallObject.restrictionLT_map, CategoryTheory.SmallObject.SuccStruct.ofCocone_map, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.arrowMap_functor_to_top, CategoryTheory.SmallObject.SuccStruct.iterationFunctor_obj, Finset.subtype_Iic_eq, Filter.map_val_Iio_atBot, Set.image_subtype_val_Ici_subset, unitInterval.univ_eq_Icc, comap_coe_Iio_nhdsLT, Finset.subtype_Ici_eq, AntitoneOn.monotone, unitInterval.subtype_Iic_eq_Icc, Set.image_subtype_val_Ioi_Iic, comap_coe_nhdsGT_of_Ioo_subset, Set.Ici.subtype_functor_final, Set.OrdConnected.isStronglyCoatomic, HahnEmbedding.Partial.sSupFun_strictMono, Filter.tendsto_comp_val_Ioi_atTop, CategoryTheory.Limits.PreservesWellOrderContinuousOfShape.preservesColimitsOfShape, CategoryTheory.SmallObject.coconeOfLE_ι_app, Set.image_subtype_val_Iic_Ici, Set.image_subtype_val_Iic_Ioi, HasCardinalLT.Set.instIsFilteredOfFactIsRegular, CategoryTheory.Functor.WellOrderInductionData.Extension.map_limit, Path.range_subpath_of_le, Module.fgSystem.instDirectedSystemSubtypeSubmoduleFGMemValCoeLinearMapId, Finset.map_subtype_embedding_Ioo, Submonoid.topOrderMonoidIso_apply, unitInterval.subtype_Ioi_eq_Ioc, Set.image_subtype_val_Iio_Ici, InfConvergenceClass.tendsto_coe_atBot_isGLB, closureOperator_gi_self, IsCoatom.Ici, Flag.coe_wcovBy_coe, Set.image_subtype_val_Ioi_Iio, Filter.tendsto_Ici_atTop, map_coe_atTop_of_Ioo_subset, Set.image_subtype_val_Ico_Ici, comap_coe_nhdsGT_eq_atBot_iff, Finset.subtype_Ioo_eq, CategoryTheory.SmallObject.SuccStruct.Iteration.prop_map_succ, Monotone.rangeFactorization, Equiv.image_monotone, CategoryTheory.TransfiniteCompositionOfShape.ici_incl, Submodule.FG.rTensor.directLimit_apply', Set.Iic.isCoatom_iff, HasCardinalLT.Set.isFiltered_of_aleph0_le, Finset.subtype_Icc_eq, Set.image_subtype_val_Ioc_Iic, Set.image_subtype_val_Icc_subset, orderTopology_of_ordConnected, Set.preimage_subtype_val_Icc, Set.image_subtype_val_Ici_Ioi, Set.strictAntiOn_iff_strictAnti, CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj_trans, Set.image_subtype_val_Icc_Iic, FiniteArchimedeanClass.withTopOrderIso_apply_coe, Finset.map_subtype_embedding_Iic, Set.preimage_subtype_val_Iio, Set.image_subtype_val_Icc, tendsto_comp_coe_Ioi_atBot, Finset.subtype_Ioi_eq, Set.image_subtype_val_Ioo_Iio, Filter.map_val_Iic_atBot, Set.monotone_projIci, Finset.map_subtype_embedding_Icc, Set.image_subtype_val_Ioo_Iic, Set.preimage_subtype_val_Ici, strictMono_coe, comap_coe_Ioo_nhdsGT, hahnEmbedding_isOrderedAddMonoid, CategoryTheory.SmallObject.SuccStruct.Iteration.arrow_mk_mapObj, unitInterval.volume_Iio, Nonneg.segment_eq_Icc, map_coe_Iio_atTop, tendsto_Iio_atTop, Nonneg.instIsStrictOrderedModule, hahnEmbedding_isOrderedModule, CategoryTheory.Limits.hasColimitsOfShape_of_isSuccLimit, Set.strictMonoOn_iff_strictMono, Set.image_subtype_val_Ico_Ioi, unitInterval.volume_Ioi, comap_coe_Ioo_nhdsLT, HahnEmbedding.Partial.toOrderAddMonoidHom_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_le_coe 📖	—	—	—	—	—
coe_lt_coe 📖	—	—	—	—	—
mk_le_mk 📖	—	—	—	—	—
mk_lt_mk 📖	—	—	—	—	—

Sum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_le_elim_iff 📖	mathematical	—	Pi.hasLe	—	elim_le_elim_iff
elim_le_const_iff 📖	mathematical	—	Pi.hasLe	—	elim_le_elim_iff
elim_le_elim_iff 📖	mathematical	—	Pi.hasLe	—	—

(root)

Definitions

Name	Category	Theorems
AsLinearOrder 📖	CompOp	—
StrongLT 📖	MathDef	1 math math: isWeakAntichain_insert
instInhabitedAsLinearOrder 📖	CompOp	—
instLinearOrderEmpty 📖	CompOp	—
instLinearOrderPEmpty 📖	CompOp	—
«term_⁻¹'o_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associative_of_commutative_of_le 📖	—	Preorder.toLE PartialOrder.toPreorder	—	—	le_antisymm
commutative_of_le 📖	—	Preorder.toLE PartialOrder.toPreorder	—	—	LE.le.antisymm
compare_of_injective_eq_compareOfLessAndEq 📖	mathematical	—	LinearOrder.toOrd Preorder.toLT PartialOrder.toPreorder PartialOrder.lift LinearOrder.toPartialOrder	—	LinearOrder.compare_eq_compareOfLessAndEq
compl_ge 📖	mathematical	—	Compl.compl Pi.instCompl Prop.instCompl Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder Preorder.toLT	—	—
compl_gt 📖	mathematical	—	Compl.compl Pi.instCompl Prop.instCompl Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder Preorder.toLE	—	—
compl_le 📖	mathematical	—	Compl.compl Pi.instCompl Prop.instCompl Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder Preorder.toLT	—	—
compl_lt 📖	mathematical	—	Compl.compl Pi.instCompl Prop.instCompl Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder Preorder.toLE	—	—
dense_or_discrete 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder Preorder.toLE	—	le_of_not_gt
dense_or_discrete' 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder Preorder.toLE	—	le_of_not_gt
eq_iff_eq_of_lt_iff_lt_of_gt_iff_gt 📖	—	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	—	—	—
eq_iff_ge_not_gt 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder Preorder.toLT	—	Decidable.eq_iff_ge_not_gt
eq_iff_le_not_lt 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder Preorder.toLT	—	Decidable.eq_iff_le_not_lt
eq_of_forall_ge_iff 📖	—	Preorder.toLE PartialOrder.toPreorder	—	—	LE.le.antisymm' le_rfl
eq_of_forall_gt_iff 📖	—	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	—	—	LE.le.antisymm' le_of_forall_gt
eq_of_forall_le_iff 📖	—	Preorder.toLE PartialOrder.toPreorder	—	—	LE.le.antisymm le_rfl
eq_of_forall_lt_iff 📖	—	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	—	—	LE.le.antisymm le_of_forall_lt
eq_of_le_of_forall_gt_imp_ge_of_dense 📖	—	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder	—	—	ge_antisymm le_of_forall_lt_imp_le_of_dense
eq_of_le_of_forall_lt_imp_le_of_dense 📖	—	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder	—	—	le_antisymm le_of_forall_gt_imp_ge_of_dense
eq_of_le_of_not_lt 📖	—	Preorder.toLE PartialOrder.toPreorder Preorder.toLT	—	—	LE.le.eq_or_lt
eq_of_le_of_not_lt' 📖	—	Preorder.toLE PartialOrder.toPreorder Preorder.toLT	—	—	LE.le.eq_or_lt'
eq_or_eq_or_eq_of_forall_not_lt_lt 📖	—	—	—	—	Ne.lt_or_gt
eq_or_lt_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	lt_or_eq_of_le
eq_or_lt_of_le' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	lt_or_eq_of_le'
exists_between 📖	—	—	—	—	DenselyOrdered.dense
exists_between' 📖	—	—	—	—	DenselyOrdered.dense'
exists_forall_ge_and 📖	—	—	—	—	exists_ge_of_linear LE.le.trans
exists_forall_le_and 📖	—	—	—	—	exists_le_of_linear LE.le.trans'
exists_ge_of_linear 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder	—	le_total le_rfl
exists_le_of_linear 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder	—	le_total le_rfl
forall_ge_iff_le 📖	mathematical	—	Preorder.toLE	—	le_of_forall_ge ge_trans
forall_ge_imp_ne_iff_lt 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	—	lt_of_forall_ge_imp_ne LT.lt.ne' LE.le.trans_lt'
forall_gt_iff_le 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder Preorder.toLE	—	le_of_forall_gt lt_of_lt_of_le'
forall_gt_imp_ge_iff_le_of_dense 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder	—	le_of_forall_gt_imp_ge_of_dense LE.le.trans LT.lt.le
forall_gt_imp_ne_iff_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder	—	le_of_forall_gt_imp_ne LT.lt.ne' LT.lt.trans_le'
forall_le_iff_le 📖	mathematical	—	Preorder.toLE	—	le_of_forall_le le_trans
forall_le_imp_ne_iff_lt 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	—	lt_of_forall_le_imp_ne LT.lt.ne LE.le.trans_lt
forall_lt_iff_le 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder Preorder.toLE	—	le_of_forall_lt lt_of_lt_of_le
forall_lt_imp_le_iff_le_of_dense 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder	—	le_of_forall_lt_imp_le_of_dense LE.le.trans' LT.lt.le
forall_lt_imp_ne_iff_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder	—	le_of_forall_lt_imp_ne LT.lt.ne LT.lt.trans_le
ge_trans' 📖	—	Preorder.toLE	—	—	le_trans
gt_trans' 📖	—	Preorder.toLT	—	—	lt_trans
instDenselyOrderedForall 📖	mathematical	DenselyOrdered Preorder.toLT	Pi.preorder	—	exists_between le_update_iff LT.lt.le le_rfl Function.update_self update_le_iff
instDenselyOrderedProd 📖	mathematical	—	DenselyOrdered Preorder.toLT Prod.instPreorder	—	exists_between le_rfl
le_Prop_eq 📖	mathematical	—	Prop.le	—	—
le_iff_eq_or_lt 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder Preorder.toLT	—	le_iff_lt_or_eq
le_iff_eq_or_lt' 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder Preorder.toLT	—	le_iff_lt_or_eq'
le_iff_le_iff_lt_iff_lt 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder Preorder.toLT	—	lt_iff_lt_of_le_iff_le not_lt
le_imp_eq_iff_le_imp_ge 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder	—	Eq.ge LE.le.antisymm
le_imp_eq_iff_le_imp_ge' 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder	—	Eq.le LE.le.antisymm'
le_imp_le_iff_lt_imp_lt 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder Preorder.toLT	—	lt_imp_lt_of_le_imp_le le_imp_le_of_lt_imp_lt
le_imp_le_of_le_of_le 📖	—	Preorder.toLE	—	—	LE.le.trans
le_of_eq_of_le' 📖	—	—	—	—	—
le_of_forall_ge 📖	—	Preorder.toLE	—	—	le_rfl
le_of_forall_gt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	Preorder.toLE	—	le_of_not_gt lt_irrefl
le_of_forall_gt_imp_ge_of_dense 📖	—	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder	—	—	le_of_not_gt exists_between lt_irrefl lt_of_lt_of_le
le_of_forall_gt_imp_ne 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder	—	le_of_not_gt
le_of_forall_le 📖	—	Preorder.toLE	—	—	le_rfl
le_of_forall_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	Preorder.toLE	—	le_of_not_gt lt_irrefl
le_of_forall_lt_imp_le_of_dense 📖	—	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder	—	—	le_of_not_gt exists_between' lt_irrefl lt_of_lt_of_le'
le_of_forall_lt_imp_ne 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder	—	le_of_not_gt
le_of_le_of_eq' 📖	—	—	—	—	—
le_of_strongLT 📖	mathematical	StrongLT Preorder.toLT	Pi.hasLe Preorder.toLE	—	LT.lt.le
le_of_subsingleton 📖	mathematical	—	Preorder.toLE	—	Eq.le
le_trans' 📖	—	Preorder.toLE	—	—	ge_trans
le_update_iff 📖	mathematical	—	Pi.hasLe Preorder.toLE Function.update	—	Function.forall_update_iff
le_update_self_iff 📖	mathematical	—	Pi.hasLe Preorder.toLE Function.update	—	—
lt_iff_le_and_ne 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder Preorder.toLE	—	le_of_lt ne_of_lt LE.le.lt_of_ne
lt_iff_le_and_ne' 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder Preorder.toLE	—	le_of_lt ne_of_gt LE.le.lt_of_ne'
lt_iff_lt_of_le_iff_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder	Preorder.toLT	—	not_le
lt_iff_lt_of_le_iff_le' 📖	mathematical	Preorder.toLE	Preorder.toLT	—	lt_iff_le_not_ge
lt_imp_lt_of_le_imp_le 📖	mathematical	Preorder.toLE Preorder.toLT	PartialOrder.toPreorder LinearOrder.toPartialOrder	—	lt_of_not_ge LE.le.not_gt
lt_imp_lt_of_le_of_le 📖	—	Preorder.toLE Preorder.toLT	—	—	LT.lt.trans_le LE.le.trans_lt
lt_of_eq_of_lt' 📖	—	—	—	—	—
lt_of_forall_ge_imp_ne 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	—	lt_of_not_ge
lt_of_forall_le_imp_ne 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	—	lt_of_not_ge
lt_of_lt_of_eq' 📖	—	—	—	—	—
lt_of_strongLT 📖	mathematical	StrongLT Preorder.toLT	Pi.preorder	—	Pi.lt_def le_of_strongLT
lt_or_gt_iff_ne' 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	—	ne_iff_gt_or_lt
lt_or_lt_iff_ne 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	—	ne_iff_lt_or_gt
lt_self_iff_false 📖	mathematical	—	Preorder.toLT	—	lt_irrefl
lt_trans' 📖	—	Preorder.toLT	—	—	gt_trans
lt_update_self_iff 📖	mathematical	—	Preorder.toLT Pi.preorder Function.update	—	—
max_def_lt 📖	mathematical	—	LinearOrder.toMax Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrder.toDecidableLT	—	max_comm max_def
max_def_lt' 📖	mathematical	—	LinearOrder.toMax Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrder.toDecidableLT	—	max_comm max_def' not_le
max_rec 📖	mathematical	—	LinearOrder.toMax	—	le_total max_eq_left max_eq_right
max_rec' 📖	mathematical	—	LinearOrder.toMax	—	—
min_def_lt 📖	mathematical	—	LinearOrder.toMin Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrder.toDecidableLT	—	min_comm min_def
min_def_lt' 📖	mathematical	—	LinearOrder.toMin Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrder.toDecidableLT	—	min_comm min_def' not_le
min_rec 📖	mathematical	—	LinearOrder.toMin	—	le_total min_eq_left min_eq_right
min_rec' 📖	mathematical	—	LinearOrder.toMin	—	—
ne_iff_gt_iff_ge 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder Preorder.toLE	—	Decidable.ne_iff_gt_iff_ge
ne_iff_lt_iff_le 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder Preorder.toLE	—	Decidable.ne_iff_lt_iff_le
ne_of_not_ge 📖	—	Preorder.toLE	—	—	ge_of_eq
ne_of_not_le 📖	—	Preorder.toLE	—	—	le_of_eq
not_lt_iff_eq_or_lt 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	—	not_lt Decidable.le_iff_eq_or_lt
not_lt_iff_eq_or_lt' 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	—	not_lt Decidable.le_iff_eq_or_lt'
not_lt_iff_le_imp_ge 📖	mathematical	—	Preorder.toLT Preorder.toLE	—	—
not_lt_iff_not_le_or_ge 📖	mathematical	—	Preorder.toLT Preorder.toLE	—	lt_iff_le_not_ge
not_lt_of_subsingleton 📖	mathematical	—	Preorder.toLT	—	Eq.not_lt
rel_imp_eq_of_rel_imp_le 📖	—	Preorder.toLE PartialOrder.toPreorder	—	—	le_antisymm symm
strongLT_of_le_of_strongLT 📖	—	Pi.hasLe Preorder.toLE StrongLT Preorder.toLT	—	—	LT.lt.trans_le'
strongLT_of_strongLT_of_le 📖	—	StrongLT Preorder.toLT Pi.hasLe Preorder.toLE	—	—	LT.lt.trans_le
subrelation_iff_le 📖	mathematical	—	Pi.hasLe Prop.le	—	—
update_le_iff 📖	mathematical	—	Pi.hasLe Preorder.toLE Function.update	—	Function.forall_update_iff
update_le_self_iff 📖	mathematical	—	Pi.hasLe Preorder.toLE Function.update	—	update_le_iff le_refl
update_le_update_iff 📖	mathematical	—	Pi.hasLe Preorder.toLE Function.update	—	Function.update_self Function.update_of_ne
update_le_update_iff' 📖	mathematical	—	Pi.hasLe Preorder.toLE Function.update	—	—
update_lt_self_iff 📖	mathematical	—	Preorder.toLT Pi.preorder Function.update	—	lt_iff_le_not_ge update_le_self_iff le_update_self_iff
update_lt_update_iff 📖	mathematical	—	Preorder.toLT Pi.preorder Function.update	—	lt_iff_lt_of_le_iff_le' update_le_update_iff'

---

← Back to Index