Synonym

📁 Source: Mathlib/Order/Synonym.lean

Statistics

Metric	Count
Definitions rec, rec, instUnique, ofDual, rec, toDual, instBEqColex, instBEqLex, instCoeFunColex, instCoeFunLex, instDecidableEqColex, instDecidableEqLex, instInhabitedColex, instInhabitedLex, instUniqueColex, instUniqueLex, ofColex, ofLex, toColex, toLex	20
Theorems exists, forall, dual, ofDual, dual, ofDual, exists, forall, exists, ext, ext_iff, forall, instNontrivial, le_toDual, lt_toDual, ofDual_comp_toDual, ofDual_inj, ofDual_le_ofDual, ofDual_lt_ofDual, ofDual_symm_eq, ofDual_toDual, ofDual_trans_toDual, toDual_comp_ofDual, toDual_inj, toDual_le, toDual_le_toDual, toDual_lt, toDual_lt_toDual, toDual_ofDual, toDual_symm_eq, toDual_trans_ofDual, instLawfulBEqColex, instLawfulBEqLex, instNonemptyColex, instNonemptyLex, instNontrivialColex, instNontrivialLex, ofColex_inj, ofColex_symm_eq, ofColex_toColex, ofLex_inj, ofLex_symm_eq, ofLex_toLex, toColex_inj, toColex_ofColex, toColex_symm_eq, toLex_inj, toLex_ofLex, toLex_symm_eq	49
Total	69

Colex

Definitions

Name	Category	Theorems
rec 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists 📖	mathematical	—	DFunLike.coe Equiv Colex EquivLike.toFunLike Equiv.instEquivLike toColex	—	—
forall 📖	mathematical	—	DFunLike.coe Equiv Colex EquivLike.toFunLike Equiv.instEquivLike toColex	—	—

LE.le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dual 📖	mathematical	—	OrderDual OrderDual.instLE DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual	—	OrderDual.toDual_le_toDual
ofDual 📖	mathematical	OrderDual OrderDual.instLE	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual	—	OrderDual.ofDual_le_ofDual

LT.lt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dual 📖	mathematical	—	OrderDual OrderDual.instLT DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual	—	OrderDual.toDual_lt_toDual
ofDual 📖	mathematical	OrderDual OrderDual.instLT	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual	—	OrderDual.ofDual_lt_ofDual

Lex

Definitions

Name	Category	Theorems
rec 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists 📖	mathematical	—	DFunLike.coe Equiv Lex EquivLike.toFunLike Equiv.instEquivLike toLex	—	—
forall 📖	mathematical	—	DFunLike.coe Equiv Lex EquivLike.toFunLike Equiv.instEquivLike toLex	—	—

OrderDual

Definitions

Name	Category	Theorems
instUnique 📖	CompOp	—
ofDual 📖	CompOp	292 math math: pow_ofDual, WithBot.ofDual_map, WithTop.map_ofDual, isSublattice_preimage_ofDual, ofDual_toAdd_zero, ofDual_le_ofDual, Set.dual_ordConnectedComponent, Order.height_ofDual, ofDual_max, LeftOrdContinuous.rightOrdContinuous_dual, MonotoneOn.dual_left, OrderIso.coe_dualDual_symm, Set.Ioi_ofDual, StrictAntiOn.dual_left, supClosed_preimage_ofDual, List.sortedGT_map_ofDual, CompleteLatticeHom.dual_symm_apply_toFun, TopologicalSpace.Closeds.complOrderIso_symm_apply, isBot_ofDual_iff, strictAntiOn_comp_ofDual_iff, strictMono_dual_iff, toDual_symm_eq, ofDual_bot, Set.dual_ordConnectedSection, SupIrred.ofDual, Set.Ioc_ofDual, OrderIso.invENNReal_symm_apply, supIrred_ofDual, ofDual_inf, isCompl_ofDual_iff, StrictAntiOn.dual, List.SortedLT.of_map_ofDual, Finset.map_ofDual_max, ofDual_iInf, CategoryTheory.Localization.LeftBousfield.galoisConnection, toDual_sInf, Finset.ofDual_inf, ofDual_min, monotoneOn_comp_ofDual_iff, OrderIso.inv_symm_apply, NonemptyInterval.coe_dual, Maximal.dual, ofDual_ofNat, IsLeast.dual, monotone_dual_iff, isBounded_preimage_ofDual, TopologicalSpace.Opens.complOrderIso_symm_apply, Finset.Ioc_ofDual, ofDual_hnot, SimpleGraph.hasseDualIso_apply, toDual_sSup, WithBot.map_ofDual, ofDual_preimage_latticeClosure, StrictMonoOn.dual_left, ofDual_smul, Fin.revOrderIso_apply, isAddLeftRegular_ofDual, strictMonoOn_dual_iff, dist_ofDual, Finset.Ioo_orderDual_def, edist_ofDual, OrderIso.dual_apply, gc_upperPolar_lowerPolar, gc_upperBounds_lowerBounds, ofDual_himp, norm_ofDual, WithBot.ofDual_apply_coe, Finset.Ioo_ofDual, infPrime_ofDual, GaloisConnection.dual, fixingAddSubmonoid_fixedPoints_gc, ofDual_pow, Interval.coe_dual, Set.Iio_toDual, WithBot.toDual_map, IsBot.ofDual, isMax_ofDual_iff, Set.Ici_ofDual, continuous_ofDual, Iio_orderDual_def, strictMono_comp_ofDual_iff, IncidenceAlgebra.mu_ofDual, IsGreatest.dual, List.sortedGE_map_ofDual, ValuationSubring.primeSpectrumOrderEquiv_apply_coe_carrier, Set.uIoo_toDual, PrimitiveSpectrum.gc_closureOperator, SupClosed.dual, ofDual_compares_ofDual, isAddRightRegular_ofDual, ext_iff, minimal_toDual, disjoint_ofDual_iff, Valuation.ofAddValuation_apply, Set.dual_ordConnected, sSupHom.dual_symm_apply_toFun, cmpLE_ofDual, sInfHom.dual_apply_toFun, NonemptyInterval.dual_map₂, ofDual_sInf, Finset.ofDual_sup', sSupHom.dual_apply_toFun, isClosedMap_ofDual, Monotone.dual_left, CategoryTheory.ObjectProperty.galoisConnection_isColocal, Set.uIcc_ofDual, CategoryTheory.MorphismProperty.gc_llp_rlp, RightOrdContinuous.orderDual, isLowerSet_preimage_ofDual_iff, OrderIso.compl_symm_apply, Ioi_orderDual_def, StrictAnti.dual_left, Finset.Icc_orderDual_def, Concept.swapEquiv_apply, Set.Ico_toDual, ofDual_eq_one, ofDual_compl, IsTop.ofDual, codisjoint_ofDual_iff, Set.Icc_ofDual, ofDual_neg, IsGaloisGroup.ofDual_intermediateFieldEquivSubgroup_apply, Set.Ioo_ofDual, List.SortedGT.of_map_ofDual, IsGLB.dual, Antitone.dual, Fin.revOrderIso_toEquiv, ofDual_ratCast, Set.uIcc_toDual, StrictMono.dual_left, WithTop.ofDual_apply_coe, Set.Ioc_toDual, Iic_orderDual_def, maximal_toDual, gc_Ici_sInf, IsMin.ofDual, LinearMap.polar_gc, Finset.Ico_ofDual, Finset.Ioc_orderDual_def, Order.PFilter.sInf_gc, List.sortedLT_map_ofDual, antitoneOn_comp_ofDual_iff, toDual_le, WCovBy.ofDual, antitone_dual_iff, AntitoneOn.dual_left, ofDual_one, Set.Iic_toDual, ofDual_iSup, Set.dual_ordSeparatingSet, InfPrime.ofDual, gc_upperClosure_coe, WithTop.ofDual_map, isLeftRegular_ofDual, List.SortedLE.of_map_ofDual, IsGalois.intermediateFieldEquivSubgroup_symm_apply, Finset.Ioi_ofDual, Submodule.dualAnnihilator_gc, bddBelow_preimage_ofDual, BddBelow.dual, OrderIso.neg_symm_apply, MonotoneOn.dual, infClosed_preimage_ofDual, Monotone.dual, Antitone.dual_left, sInfHom.dual_symm_apply_toFun, LE.le.ofDual, Matrix.blockTriangular_transpose_iff, Set.Iic_ofDual, nhds_ofDual, Set.Ioo_toDual, ofDual_natCast, ofDual_intCast, strictAnti_dual_iff, Set.Iio_ofDual, CategoryTheory.orderDualEquivalence_counitIso, Finset.Icc_ofDual, Set.ordConnected_dual, CategoryTheory.orderDualEquivalence_functor_obj, isUpperSet_preimage_ofDual_iff, Finset.ofDual_min', IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply, StrictAnti.dual, IsLUB.dual, Finset.Iic_ofDual, BddAbove.dual, List.SortedGE.of_map_ofDual, Submodule.torsion_gc, IsCompl.ofDual, fixingSubmonoid_fixedPoints_gc, lt_toDual, isAddRegular_ofDual, ofDual_wcovBy_ofDual_iff, ofDual_toAdd_eq_top_iff, Set.Ioi_toDual, isOpenMap_ofDual, StrictMono.dual, eVariationOn.comp_ofDual, antitoneOn_dual_iff, infIrred_ofDual, isRightRegular_ofDual, toDual_trans_ofDual, Set.OrdConnected.dual, nnnorm_ofDual, TopologicalSpace.gc_generateFrom, le_toDual, toDual_lt, SetRel.gc_leftDual_rightDual, toDual_comp_ofDual, ofDual_sup, ofDual_sub, ofDual_symm_eq, fixingAddSubgroup_fixedPoints_gc, Finset.Ico_orderDual_def, Set.uIoo_ofDual, OrderIso.subLeft_symm_apply, bddAbove_preimage_ofDual, ofDual_symmDiff, ofDual_inv, fixingSubgroup_fixedPoints_gc, Finset.ofDual_inf', IsLowerSet.toDual, List.sortedLE_map_ofDual, OrderHom.dual_apply_coe, grade_ofDual, CompleteLatticeHom.dual_apply_toFun, IsUpperSet.toDual, Set.dual_ordConnected_iff, ofDual_toDual, OrderHom.dual_symm_apply_coe, OrderIso.smulRightDual_symm_apply, antitone_comp_ofDual_iff, Ici_orderDual_def, WithTop.toDual_map, InfClosed.dual, isTop_ofDual_iff, isMin_ofDual_iff, IsSublattice.dual, ofDual_bihimp, Finset.map_ofDual_min, OrderIso.divLeft_symm_apply, isCobounded_preimage_ofDual, ofDual_add, supPrime_ofDual, monotone_comp_ofDual_iff, ofDual_sSup, ofDual_trans_toDual, ofDual_vadd', CategoryTheory.ObjectProperty.galoisConnection_isLocal, isRegular_ofDual, ofDual_lt_ofDual, ofDual_comp_toDual, monotoneOn_dual_iff, ofDual_mul, Set.Ici_toDual, Set.Icc_toDual, Dense.orderDual, ofDual_inj, strictMonoOn_comp_ofDual_iff, StrictMonoOn.dual, ofDual_eq_top, CovBy.ofDual, ofDual_vadd, LT.lt.ofDual, Finset.ofDual_max', OrderIso.dual_symm_apply, AddValuation.ofValuation_apply, ofDual_covBy_ofDual_iff, ofDual_div, Order.coheight_ofDual, Finset.ofDual_sup, PrimitiveSpectrum.gc, IsMax.ofDual, ofDual_zero, SupPrime.ofDual, ofDual_eq_zero, strictAntiOn_dual_iff, cmp_ofDual, strictAnti_comp_ofDual_iff, Minimal.dual, toDual_ofDual, Finset.Iio_ofDual, Finset.Ici_ofDual, InfIrred.ofDual, ofDual_smul', Set.Ico_ofDual, nndist_ofDual, ofDual_top, IsGalois.ofDual_intermediateFieldEquivSubgroup_apply, OrderIso.dualDual_symm_apply, AntitoneOn.dual, ofDual_eq_bot
rec 📖	CompOp	—
toDual 📖	CompOp	356 math math: isBounded_preimage_toDual, isCompl_toDual_iff, WithBot.coe_toDualTopEquiv_eq, WithBot.ofDual_map, IsUpperSet.ofDual, Order.IsSuccPrelimit.dual, WithTop.toDualBotEquiv_coe, IsLowerSet.ofDual, Set.dual_ordConnectedComponent, strictAntiOn_toDual_comp_iff, isMin_toDual_iff, LeftOrdContinuous.rightOrdContinuous_dual, Set.Ioi_ofDual, Finset.uIcc_toDual, CompleteLatticeHom.dual_symm_apply_toFun, toDual_pow, Finset.Ioi_toDual, AntivaryOn.dual, isTop_toDual_iff, dist_toDual, instNeBotNhdsWithinIio, Disjoint.dual, strictMono_dual_iff, toDual_symm_eq, IsMinFilter.dual, Set.Ioc_ofDual, OrderIso.neg_apply, StrictAntiOn.dual, toDual_vadd', isUpperSet_preimage_toDual_iff, Codisjoint.dual, Antitone.dual_right, isMinOn_dual_iff, toDual_le_toDual, CategoryTheory.Localization.LeftBousfield.galoisConnection, OrderIso.subLeft_apply, toDual_sInf, OrderIso.dualAntisymmetrization_symm_apply, WCovBy.toDual, IsBot.toDual, Matrix.blockTriangular_transvection', TopologicalSpace.Opens.complOrderIso_apply, toDual_smul', Maximal.dual, Monovary.dual_left, IsLeast.dual, monotone_dual_iff, toDual_zero, isExtrFilter_dual_iff, antivaryOn_toDual_left, toDual_sSup, QuasilinearOn.dual, StrictMono.dual_right, nndist_toDual, toDual_eq_zero, AntivaryOn.dual_right, OrderIso.smulRightDual_apply, strictMonoOn_dual_iff, OrderIso.dualDual_apply, isLowerSet_preimage_toDual_iff, supPrime_toDual, Finset.toDual_min', toDual_compares_toDual, Finset.Ioo_orderDual_def, OrderIso.dual_apply, gc_upperPolar_lowerPolar, disjoint_toDual_iff, gc_upperBounds_lowerBounds, infClosed_preimage_toDual, toDual_sdiff, MonovaryOn.dual_left, toDual_inj, pow_toDual, monovary_toDual_right, IsSublattice.of_dual, IsGalois.intermediateFieldEquivSubgroup_apply, NonemptyInterval.dual_pure, OrderIso.coe_dualDual, toDual_wcovBy_toDual_iff, GaloisConnection.dual, fixingAddSubmonoid_fixedPoints_gc, Order.isPredPrelimit_toDual_iff, toDual_vadd, NonemptyInterval.fst_dual, Set.Iio_toDual, OrderIso.divLeft_apply, antitone_toDual_comp_iff, InfPrime.dual, WithBot.toDual_map, toDual_max, toDual_inv, bddBelow_preimage_toDual, Set.Ici_ofDual, Iio_orderDual_def, TopologicalSpace.Closeds.complOrderIso_apply, Antivary.dual_left, IsMax.toDual, Finset.map_toDual_max, cmp_toDual, IsGreatest.dual, antitoneOn_toDual_comp_iff, Set.uIoo_toDual, PrimitiveSpectrum.gc_closureOperator, supIrred_toDual, CategoryTheory.ComposableArrows.opEquivalence_functor_obj_map, OrderIso.sumDualDistrib_symm_inl, isClosedMap_toDual, minimal_toDual, toDual_intCast, toDual_mul, sSupHom.dual_symm_apply_toFun, monotone_toDual_comp_iff, strictAnti_toDual_comp_iff, sInfHom.dual_apply_toFun, CovBy.toDual, NonemptyInterval.dual_map₂, ofDual_sInf, Finset.toDual_inf', toDual_compl, toDual_lt_toDual, Valuation.toAddValuation_apply, IsMaxOn.dual, sSupHom.dual_apply_toFun, CategoryTheory.ObjectProperty.galoisConnection_isColocal, Set.uIcc_ofDual, CategoryTheory.MorphismProperty.gc_llp_rlp, RightOrdContinuous.orderDual, AntitoneOn.dual_right, Ioi_orderDual_def, MonovaryOn.dual_right, monovaryOn_toDual_right, antivary_toDual_right, toDual_min, Finset.Icc_orderDual_def, Finset.Ioo_toDual, Set.Ico_toDual, Finset.map_toDual_min, WithBot.toDualTopEquiv_coe, Set.Icc_ofDual, isMax_toDual_iff, isAtom_dual_iff_isCoatom, Set.Ioo_ofDual, Order.IsSuccLimit.dual, IsGalois.intermediateFieldEquivSubgroup_symm_apply_toDual, strictMonoOn_toDual_comp_iff, isRightRegular_toDual, IsGLB.dual, Antitone.dual, isExtrOn_dual_iff, InfIrred.dual, toDual_hnot, Set.uIcc_toDual, Set.Ioc_toDual, Iic_orderDual_def, nnnorm_toDual, maximal_toDual, List.sortedLE_map_toDual, Order.IsPredLimit.dual, gc_Ici_sInf, LinearMap.polar_gc, LE.le.dual, Interval.dual_pure, WithBot.toDual_apply_coe, Finset.toDual_inf, Finset.Ioc_orderDual_def, Finset.toDual_max', Order.PFilter.sInf_gc, OrderIso.dualAntisymmetrization_apply, toDual_le, codisjoint_toDual_iff, antitone_dual_iff, Finset.Ioc_toDual, Set.Iic_toDual, ConvexOn.dual, Monotone.dual_right, Finset.Icc_toDual, Monovary.dual_right, isAddRightRegular_toDual, gc_upperClosure_coe, WithTop.ofDual_map, WithTop.map_toDual, List.SortedGT.of_map_toDual, List.SortedLT.of_map_toDual, Matrix.BlockTriangular.transpose, Submodule.dualAnnihilator_gc, Order.isPredLimit_toDual_iff, MonotoneOn.dual, toDual_sub, continuous_toDual, Monotone.dual, sInfHom.dual_symm_apply_toFun, WithBot.toDualTopEquiv_symm_coe, OrderIso.sumDualDistrib_inl, Finset.Ici_toDual, toDual_top, OrderIso.invENNReal_apply, isBot_toDual_iff, Order.PFilter.mem_mk, SupPrime.dual, Set.Iic_ofDual, Order.IsPredPrelimit.dual, Order.isSuccLimit_toDual_iff, QuasiconvexOn.dual, Set.Ioo_toDual, IsAtom.dual, exists, isAddLeftRegular_toDual, strictAnti_dual_iff, Set.Iio_ofDual, CategoryTheory.orderDualEquivalence_counitIso, OrderIso.sumDualDistrib_symm_inr, infPrime_toDual, Fin.revOrderIso_symm_apply, Finset.Iio_toDual, toDual_neg, monotoneOn_toDual_comp_iff, forall, StrictAnti.dual, IsLUB.dual, Finset.toDual_sup, fixingSubmonoid_fixedPoints_gc, WithTop.toDualBotEquiv_symm_coe, lt_toDual, StrictAnti.dual_right, infIrred_toDual, Set.Ioi_toDual, List.sortedGT_map_toDual, StrictMono.dual, antitoneOn_dual_iff, OrderIso.sumLexDualAntidistrib_symm_inl, toDual_trans_ofDual, AddValuation.toValuation_apply, instNeBotNhdsWithinIoi, List.sortedLT_map_toDual, supClosed_preimage_toDual, toDual_eq_top, TopologicalSpace.gc_generateFrom, le_toDual, toDual_lt, IsExtrFilter.dual, SetRel.gc_leftDual_rightDual, List.SortedLE.of_map_toDual, toDual_comp_ofDual, AntivaryOn.dual_left, OrderIso.inv_apply, IsGaloisGroup.intermediateFieldEquivSubgroup_apply, ofDual_symm_eq, fixingAddSubgroup_fixedPoints_gc, Finset.Ico_orderDual_def, monovary_toDual_left, OrderIso.compl_apply, Set.uIoo_ofDual, toDual_bihimp, List.sortedGE_map_toDual, norm_toDual, isMaxFilter_dual_iff, isLeftRegular_toDual, fixingSubgroup_fixedPoints_gc, antivaryOn_toDual_right, MonotoneOn.dual_right, toDual_bot, isRegular_toDual, LT.lt.dual, OrderHom.dual_apply_coe, StrictConvexOn.dual, OrderIso.sumDualDistrib_inr, CompleteLatticeHom.dual_apply_toFun, IsExtrOn.dual, antivary_toDual_left, toDual_eq_bot, Order.isSuccPrelimit_toDual_iff, Antivary.dual_right, ofDual_toDual, OrderHom.dual_symm_apply_coe, Finset.Iic_toDual, Monovary.dual, Ici_orderDual_def, QuasiconcaveOn.dual, WithTop.toDual_map, isMaxOn_dual_iff, IsCoatom.dual, IsCompl.dual, isMinFilter_dual_iff, isSublattice_preimage_toDual, SupIrred.dual, toDual_eq_one, SimpleGraph.hasseDualIso_symm_apply, toDual_symmDiff, StrictConcaveOn.dual, toDual_smul, ofDual_sSup, isAddRegular_toDual, IsMin.toDual, ofDual_trans_toDual, CategoryTheory.ObjectProperty.galoisConnection_isLocal, CategoryTheory.orderDualEquivalence_inverse_obj, edist_toDual, toDual_iInf, ofDual_comp_toDual, monotoneOn_dual_iff, toDual_sup, toDual_iSup, IsTop.toDual, toDual_ofNat, toDual_div, NonemptyInterval.snd_dual, Concept.swapEquiv_symm_apply, Set.Ici_toDual, Set.Icc_toDual, isCobounded_preimage_toDual, OrderIso.sumLexDualAntidistrib_symm_inr, IncidenceAlgebra.mu_toDual, nhds_toDual, StrictMonoOn.dual_right, OrderIso.sumLexDualAntidistrib_inr, NonemptyInterval.toDualProd_apply, toDual_ratCast, grade_toDual, StrictMonoOn.dual, ofAdd_toDual_eq_zero_iff, isCoatom_dual_iff_isAtom, toDual_natCast, strictMono_toDual_comp_iff, toDual_add, OrderIso.dual_symm_apply, bddAbove_preimage_toDual, Matrix.blockTriangular_single', OrderIso.sumLexDualAntidistrib_inl, MonovaryOn.dual, IsMinOn.dual, cmpLE_toDual, PrimitiveSpectrum.gc, toDual_covBy_toDual_iff, List.SortedGE.of_map_toDual, toDual_inf, strictAntiOn_dual_iff, monovaryOn_toDual_left, CategoryTheory.orderDualEquivalence_inverse_map, Order.height_toDual, WithTop.toDual_apply_coe, Finset.Ico_toDual, Antivary.dual, ConcaveOn.dual, WithTop.coe_toDualBotEquiv, WithBot.map_toDual, Minimal.dual, StrictAntiOn.dual_right, isOpenMap_toDual, IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply_toDual, toDual_ofDual, toDual_one, Order.coheight_toDual, IsMaxFilter.dual, Set.Ico_ofDual, Finset.toDual_sup', AntitoneOn.dual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike toDual	—	—
ext 📖	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual	—	—	—
ext_iff 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual	—	ext
forall 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike toDual	—	—
instNontrivial 📖	mathematical	—	Nontrivial OrderDual	—	—
le_toDual 📖	mathematical	—	OrderDual instLE DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toDual ofDual	—	—
lt_toDual 📖	mathematical	—	OrderDual instLT DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toDual ofDual	—	—
ofDual_comp_toDual 📖	mathematical	—	OrderDual DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofDual toDual	—	—
ofDual_inj 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual	—	EquivLike.toEmbeddingLike
ofDual_le_ofDual 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual instLE	—	—
ofDual_lt_ofDual 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual instLT	—	—
ofDual_symm_eq 📖	mathematical	—	Equiv.symm OrderDual ofDual toDual	—	—
ofDual_toDual 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual toDual	—	—
ofDual_trans_toDual 📖	mathematical	—	Equiv.trans OrderDual ofDual toDual Equiv.refl	—	—
toDual_comp_ofDual 📖	mathematical	—	OrderDual DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toDual ofDual	—	—
toDual_inj 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike toDual	—	EquivLike.toEmbeddingLike
toDual_le 📖	mathematical	—	OrderDual instLE DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toDual ofDual	—	—
toDual_le_toDual 📖	mathematical	—	OrderDual instLE DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toDual	—	—
toDual_lt 📖	mathematical	—	OrderDual instLT DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toDual ofDual	—	—
toDual_lt_toDual 📖	mathematical	—	OrderDual instLT DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toDual	—	—
toDual_ofDual 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike toDual ofDual	—	—
toDual_symm_eq 📖	mathematical	—	Equiv.symm OrderDual toDual ofDual	—	—
toDual_trans_ofDual 📖	mathematical	—	Equiv.trans OrderDual toDual ofDual Equiv.refl	—	—

(root)

Definitions

Name	Category	Theorems
instBEqColex 📖	CompOp	1 math math: instLawfulBEqColex
instBEqLex 📖	CompOp	1 math math: instLawfulBEqLex
instCoeFunColex 📖	CompOp	—
instCoeFunLex 📖	CompOp	—
instDecidableEqColex 📖	CompOp	—
instDecidableEqLex 📖	CompOp	—
instInhabitedColex 📖	CompOp	—
instInhabitedLex 📖	CompOp	—
instUniqueColex 📖	CompOp	—
instUniqueLex 📖	CompOp	—
ofColex 📖	CompOp	44 math math: toColex_symm_eq, isLeftRegular_ofColex, toColex_ofColex, ofColex_one, Finset.Colex.le_iff_max'_mem, ofColex_div, ofColex_add, Finset.Colex.lt_iff_exists_forall_lt, isAddLeftRegular_ofColex, ofColex_vadd', pow_ofColex, ofColex_smul', isAddRegular_ofColex, Pi.ofColex_apply, DFinsupp.colex_lt_iff_of_unique, Finset.geomSum_ofColex_strictMono, ofColex_mul, ofColex_eq_zero, ofColex_inv, DFinsupp.Colex.le_iff_of_unique, Finset.Colex.ofColex_top, DFinsupp.Colex.lt_iff, Finsupp.Colex.le_iff_of_unique, ofColex_inj, ofColex_smul, Finsupp.Colex.lt_iff, ofColex_symm_eq, ofColex_vadd, isAddRightRegular_ofColex, Finset.Colex.le_def, ofColex_pow, Finset.Colex.lt_iff_max'_mem, isRightRegular_ofColex, ofColex_eq_one, Finset.Colex.toColex_image_ofColex_strictMono, ofColex_sub, Finset.Colex.le_iff_sdiff_subset_lowerClosure, ofColex_neg, ofColex_toColex, Finset.orderIsoColex_symm_apply, Finsupp.Colex.lt_iff_of_unique, ofColex_zero, Finset.Colex.ofColex_bot, isRegular_ofColex
ofLex 📖	CompOp	111 math math: DFinsupp.lex_lt_iff_of_unique, Prod.Lex.lt_iff', ofLex_symm_eq, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, Prod.Lex.compare_def, Prod.Lex.monotone_fst, ofLex_add, isRightRegular_ofLex, ofLex_ratCast, Pi.ofLex_apply, ofLex_sub, MvPolynomial.supDegree_esymmAlgHomMonomial, ofLex_intCast, Prod.Lex.monotone_fst_ofLex, HahnSeries.support_abs, HahnEmbedding.Partial.truncLT_mem_range_extendFun, Prod.Lex.prodLexAssoc_symm_apply, ofLex_vadd, DFinsupp.lex_lt_iff, HahnEmbedding.Partial.orderTop_eq_iff, ofLex_pow, HahnEmbedding.Partial.coeff_eq_of_mem, Set.PartiallyWellOrderedOn.imageProdLex, Prod.Lex.sumLexProdLexDistrib_symm_apply, ofLex_eq_one, DFinsupp.Lex.le_iff_of_unique, HahnSeries.embDomainOrderEmbedding_apply, Prod.Lex.le_iff, HahnEmbedding.IsPartial.truncLT_mem_range, toLex_ofLex, HahnSeries.order_abs, ofLex_neg, ofLex_natCast, HahnEmbedding.Partial.truncLT_mem_range_sSupFun, coe_ofLexMulEquiv, Sum.Lex.toLexRelIsoLE_symm_coe, HahnSeries.archimedeanClassMk_eq_archimedeanClassMk_iff, Prod.Lex.sumLexProdLexDistrib_apply, ofLex_toLex, HahnSeries.leadingCoeff_pos_iff, Prod.Lex.uniqueProd_apply, OrderIso.sumLexCongr_apply, MvPolynomial.supDegree_esymm, Prod.Lex.covBy_iff, HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_snd, Finsupp.Lex.le_iff_of_unique, HahnEmbedding.Seed.coeff_baseEmbedding, Finsupp.lex_lt_iff_of_unique, ofLex_one, toLex_symm_eq, DFinsupp.Lex.lt_iff_of_unique, HahnSeries.archimedeanClassOrderIsoWithTop_apply, OrderMonoidHom.fstₗ_apply, Sum.Lex.lt_def, isAddRightRegular_ofLex, ofLex_inj, ofLex_inv, HahnEmbedding.Partial.coeff_eq_zero_of_mem, coe_ofLexAddEquiv, DFinsupp.lex_le_iff_of_unique, HahnSeries.leadingCoeff_nonneg_iff, toEquiv_ofLexMulEquiv, HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk, hahnEmbedding_isOrderedModule_rat, ofLex_ofNat, HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding, Finsupp.lex_le_iff_of_unique, ofLex_smul', HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff, pow_ofLex, ofLex_vadd', ofLex_smul, HahnSeries.lt_iff, Finsupp.lex_lt_iff, OrderAddMonoidHom.fstₗ_apply, isAddRegular_ofLex, HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_fst, HahnSeries.orderTop_abs, HVertexOperator.coeff_comp, ofLex_mul, Sum.Lex.le_def, HahnEmbedding.Partial.eval_eq_truncLT, HahnSeries.finiteArchimedeanClassOrderIso_apply, Prod.Lex.prodUnique_apply, isAddLeftRegular_ofLex, HahnEmbedding.Partial.evalCoeff_eq, MvPolynomial.IsSymmetric.antitone_supDegree, isLeftRegular_ofLex, MvPolynomial.leadingCoeff_toLex, HahnSeries.leadingCoeff_neg_iff, Sum.Lex.toLexRelIsoLT_symm_coe, ofLex_div, Prod.Lex.prodLexCongr_apply, Finsupp.Lex.lt_iff, HahnEmbedding.Partial.truncLT_eval_mem_range_extendFun, isRegular_ofLex, ofLex_eq_zero, Prod.Lex.lt_iff, Prod.Lex.prodLexAssoc_apply, HahnSeries.leadingCoeff_nonpos_iff, WCovBy.fst_ofLex, Finsupp.Lex.lt_iff_of_unique, ofLex_zero, toEquiv_ofLexAddEquiv, hahnEmbedding_isOrderedAddMonoid, DFinsupp.Lex.lt_iff, HahnSeries.leadingCoeff_abs, coe_ofLexLinearEquiv, Set.PartiallyWellOrderedOn.ProdLex_iff, Prod.Lex.le_iff', hahnEmbedding_isOrderedModule
toColex 📖	CompOp	77 math math: toColex_symm_eq, Finset.Colex.toColex_le_singleton, Finset.geomSum_lt_geomSum_iff_toColex_lt_toColex, toColex_ofColex, toColex_sub, Finset.Colex.toColex_univ, Finsupp.toColex_monotone, pow_toColex, Pi.toColex_monotone, Pi.colex_asc, toColex_vadd, toColex_inv, toColex_add, Finset.Colex.toColex_lt_toColex_iff_max'_mem, Finset.Colex.cons_lt_cons, Finset.Colex.toColex_sdiff_le_toColex_sdiff', Colex.forall, Finset.Colex.toColex_strictMono, isAddRightRegular_toColex, Finset.Colex.mem_initSeg, Finset.geomSum_le_geomSum_iff_toColex_le_toColex, Finset.Colex.erase_lt_erase, Finset.Colex.erase_le_erase, Finset.Colex.toColex_le_toColex_iff_max'_mem, Finset.Colex.singleton_le_toColex, Finset.Colex.toColex_image_lt_toColex_image, toColex_eq_zero, Finset.Colex.toColex_sdiff_lt_toColex_sdiff, Finset.Colex.toColex_sdiff_le_toColex_sdiff, isRightRegular_toColex, toColex_one, Finset.Colex.lt_iff_exists_filter_lt, Finset.Colex.toColex_le_toColex, Finset.Colex.toColex_lt_singleton, Finset.Colex.singleton_lt_singleton, Pi.lt_toColex_update_self_iff, toColex_neg, toColex_smul, toColex_vadd', Finset.Colex.toColex_lt_toColex_iff_exists_forall_lt, Finset.Colex.insert_le_insert, Finset.Colex.toColex_mono, toColex_inj, Pi.toColex_apply, ofColex_symm_eq, Finset.UV.toColex_compress_lt_toColex, toColex_mul, Pi.toColex_strictMono, Pi.toColex_update_le_self_iff, Finset.Colex.toColex_lt_toColex_of_ssubset, Colex.exists, Finset.Colex.toColex_image_ofColex_strictMono, DFinsupp.toColex_monotone, isAddRegular_toColex, Finset.Colex.singleton_le_singleton, Finset.Colex.toColex_lt_toColex, Finset.Colex.toColex_image_le_toColex_image, Finset.Colex.toColex_sdiff_lt_toColex_sdiff', Finset.Colex.toColex_empty, Finsupp.Colex.single_le_iff, Finset.Colex.cons_le_cons, toColex_zero, toColex_div, Pi.le_toColex_update_self_iff, toColex_pow, isAddLeftRegular_toColex, Finsupp.Colex.single_lt_iff, ofColex_toColex, isRegular_toColex, toColex_eq_one, Finset.Colex.toColex_le_toColex_of_subset, Finset.orderIsoColex_apply, Finset.Colex.insert_lt_insert, toColex_smul', Finsupp.Colex.single_strictMono, Pi.toColex_update_lt_self_iff, isLeftRegular_toColex
toLex 📖	CompOp	166 math math: Prod.Lex.toLex_lt_toLex', toLex_sub, toLex_mul, Lex.forall, Sum.Lex.Icc_inr_inr, WithBot.orderIsoPUnitSumLex_symm_inl, isLeftRegular_toLex, Lex.exists, OrderIso.sumLexIicIoi_symm_apply_of_lt, toLex_inj, ofLex_symm_eq, Sum.Lex.Ico_inl_inl, Sum.Lex.Ico_inr_inr, MvPowerSeries.exists_finsupp_eq_lexOrder_of_ne_zero, pow_toLex, toLex_ofNat, Sum.Lex.Ioo_inl_inr, LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex, toEquiv_toLexMulEquiv, DFinsupp.toLex_monotone, toLex_eq_one, Sum.Lex.inr_le_inr_iff, WithBot.orderIsoPUnitSumLex_symm_inr, OrderIso.sumLexIioIci_symm_apply_Ici, Finsupp.Lex.single_strictAnti, Sum.Lex.Iic_inr, NonemptyInterval.toLex_strictMono, MvPolynomial.supDegree_esymmAlgHomMonomial, isRegular_toLex, Sum.Lex.inr_strictMono, Prod.Lex.toLexOrderHom_coe, Prod.Lex.toLex_le_toLex', HahnEmbedding.Partial.truncLT_mem_range_extendFun, Sum.Lex.Ioo_inr_inr, toLex_vadd', Sum.Lex.inl_bot, Prod.Lex.prodLexAssoc_symm_apply, MvPowerSeries.lexOrder_def_of_ne_zero, Pi.toLex_update_le_self_iff, Sum.Lex.toLex_lt_toLex, Pi.toLex_update_lt_self_iff, OrderIso.sumLexIicIoi_symm_apply_of_le, Sum.Lex.Icc_inl_inl, Pi.le_toLex_update_self_iff, WithTop.orderIsoSumLexPUnit_toLex, Sum.Lex.inl_mono, MvPolynomial.leadingCoeff_esymmAlgHomMonomial, Prod.Lex.sumLexProdLexDistrib_symm_apply, Sum.Lex.toLexRelIsoLE_coe, WithTop.orderIsoSumLexPUnit_symm_inl, Sum.Lex.Ioi_inr, HahnSeries.embDomainOrderEmbedding_apply, OrderIso.sumLexIioIci_symm_apply_Iio, HahnEmbedding.IsPartial.truncLT_mem_range, toLex_ofLex, Sum.Lex.Ici_inl, Sum.Lex.Ioc_inl_inl, coe_toLexLinearEquiv, toLex_add, isAddLeftRegular_toLex, OrderMonoidHom.inrₗ_apply, Pi.lex_desc, HahnEmbedding.Partial.truncLT_mem_range_sSupFun, Sum.Lex.toLex_le_toLex, toLex_pow, Finsupp.Lex.single_lt_iff, OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex, toLex_ratCast, Sum.Lex.Ioc_inl_inr, Sum.Lex.Iio_inl, toLex_intCast, Prod.Lex.sumLexProdLexDistrib_apply, isAddRightRegular_toLex, ofLex_toLex, WithTop.orderIsoSumLexPUnit_top, toLex_zero, OrderIso.sumLexCongr_apply, MvPolynomial.supDegree_esymm, Prod.Lex.toLex_lt_toLex, Sum.Lex.Ioc_inr_inr, Finsupp.DegLex.lt_iff, MvPolynomial.leadingCoeff_toLex_C, Sum.Lex.Ioi_inl, Sum.Lex.Ioo_inl_inl, MvPolynomial.monic_esymm, isAddRegular_toLex, OrderIso.sumLexIicIoi_apply_inr, Set.PartiallyWellOrderedOn.fiberProdLex, toLex_natCast, Sum.Lex.Iic_inl, Sum.Lex.inl_strictMono, toLex_symm_eq, MvPolynomial.supDegree_toLex_C, isRightRegular_toLex, toLex_inv, OrderMonoidHom.inlₗ_apply, Sum.Lex.Ici_inr, Sum.Lex.inl_lt_inl_iff, OrderIso.sumLexAssoc_apply_inl_inl, toLex_vadd, OrderAddMonoidHom.inlₗ_apply, OrderIso.sumLexEmpty_apply_inl, OrderIso.sumLexIicIoi_apply_inl, Sum.Lex.Ico_inl_inr, Sum.Lex.Iio_inr, Sum.Lex.toLexRelIsoLT_coe, Pi.toLex_apply, OrderAddMonoidHom.inlₗ_add_inrₗ_eq_toLex, Pi.lt_toLex_update_self_iff, WithBot.orderIsoPUnitSumLex_toLex, HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding, toLex_smul', Prod.Lex.toLex_mono, OrderIso.emptySumLex_apply_inr, Sum.Lex.inl_lt_inr, Finsupp.Lex.single_antitone, OrderIso.sumLexIioIci_symm_apply_of_ge, Prod.Lex.toLex_covBy_toLex_iff, coe_toLexMulEquiv, Prod.Lex.toLex_strictMono, NonemptyInterval.toLex_mono, MonomialOrder.lex_lt_iff, OrderIso.sumLexIioIci_apply_inl, Sum.Lex.inr_mono, WithTop.orderIsoSumLexPUnit_symm_inr, OrderIso.sumLexAssoc_apply_inr, NonemptyInterval.toLex_lt_toLex, Sum.Lex.not_inr_le_inl, Finsupp.DegLex.le_iff, HahnEmbedding.Partial.eval_eq_truncLT, toEquiv_toLexAddEquiv, toLex_eq_zero, MonomialOrder.lex_le_iff, toLex_div, MvPolynomial.IsSymmetric.antitone_supDegree, Sum.Lex.inr_top, MvPolynomial.leadingCoeff_toLex, Prod.Lex.toLex_le_toLex, MvPowerSeries.lexOrder_le_of_coeff_ne_zero, Finsupp.toLex_monotone, Sum.Lex.toLex_strictMono, Prod.Lex.prodLexCongr_apply, Sum.Lex.inr_lt_inr_iff, Finsupp.Lex.single_le_iff, HahnEmbedding.Partial.truncLT_eval_mem_range_extendFun, OrderAddMonoidHom.inrₗ_apply, Finsupp.DegLex.lt_def, Prod.Lex.prodLexAssoc_apply, Sum.Lex.Icc_inl_inr, HahnEmbedding.Partial.apply_of_mem_stratum, toLex_smul, toLex_one, coe_toLexAddEquiv, OrderIso.sumLexIioIci_apply_inr, OrderIso.sumLexIioIci_symm_apply_of_lt, OrderIso.sumLexAssoc_apply_inl_inr, Sum.Lex.toLex_mono, Pi.toLex_strictMono, NonemptyInterval.toLex_le_toLex, toLex_neg, Sum.Lex.not_inr_lt_inl, WithBot.orderIsoPUnitSumLex_bot, Set.PartiallyWellOrderedOn.ProdLex_iff, Sum.Lex.inl_le_inr, Sum.Lex.inl_le_inl_iff, Pi.toLex_monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLawfulBEqColex 📖	mathematical	—	Colex instBEqColex	—	—
instLawfulBEqLex 📖	mathematical	—	Lex instBEqLex	—	—
instNonemptyColex 📖	mathematical	—	Colex	—	—
instNonemptyLex 📖	mathematical	—	Lex	—	—
instNontrivialColex 📖	mathematical	—	Nontrivial Colex	—	—
instNontrivialLex 📖	mathematical	—	Nontrivial Lex	—	—
ofColex_inj 📖	mathematical	—	DFunLike.coe Equiv Colex EquivLike.toFunLike Equiv.instEquivLike ofColex	—	EquivLike.toEmbeddingLike
ofColex_symm_eq 📖	mathematical	—	Equiv.symm Colex ofColex toColex	—	—
ofColex_toColex 📖	mathematical	—	DFunLike.coe Equiv Colex EquivLike.toFunLike Equiv.instEquivLike ofColex toColex	—	—
ofLex_inj 📖	mathematical	—	DFunLike.coe Equiv Lex EquivLike.toFunLike Equiv.instEquivLike ofLex	—	EquivLike.toEmbeddingLike
ofLex_symm_eq 📖	mathematical	—	Equiv.symm Lex ofLex toLex	—	—
ofLex_toLex 📖	mathematical	—	DFunLike.coe Equiv Lex EquivLike.toFunLike Equiv.instEquivLike ofLex toLex	—	—
toColex_inj 📖	mathematical	—	DFunLike.coe Equiv Colex EquivLike.toFunLike Equiv.instEquivLike toColex	—	EquivLike.toEmbeddingLike
toColex_ofColex 📖	mathematical	—	DFunLike.coe Equiv Colex EquivLike.toFunLike Equiv.instEquivLike toColex ofColex	—	—
toColex_symm_eq 📖	mathematical	—	Equiv.symm Colex toColex ofColex	—	—
toLex_inj 📖	mathematical	—	DFunLike.coe Equiv Lex EquivLike.toFunLike Equiv.instEquivLike toLex	—	EquivLike.toEmbeddingLike
toLex_ofLex 📖	mathematical	—	DFunLike.coe Equiv Lex EquivLike.toFunLike Equiv.instEquivLike toLex ofLex	—	—
toLex_symm_eq 📖	mathematical	—	Equiv.symm Lex toLex ofLex	—	—

---

← Back to Index