OrderDual 📖 | CompOp | 918 mathmath: OrderDual.isBounded_preimage_toDual, NonemptyInterval.toDualProd_mono, pow_ofDual, isCompl_toDual_iff, WithBot.coe_toDualTopEquiv_eq, WithBot.ofDual_map, OrderDual.instMeasurableSup₂, SupBotHom.dual_comp, WithTop.map_ofDual, Ordnode.Valid.dual_iff, CategoryTheory.ComposableArrows.opEquivalence_counitIso_inv_app_app, IsUpperSet.ofDual, eVariationOn.boundedVariation_ofDual, isSublattice_preimage_ofDual, OrderDual.instIsRightCancelMulZero, Order.IsSuccPrelimit.dual, ofDual_toAdd_zero, NonemptyInterval.dual_map, LinearMap.iterateRange_succ, OrderDual.ofDual_le_ofDual, WithBot.lt_ofDual_iff, InfTopHom.symm_dual_id, instIsWeakLowerModularLatticeOrderDual, WithTop.toDualBotEquiv_coe, IsLowerSet.ofDual, Set.dual_ordConnectedComponent, Order.height_ofDual, strictAntiOn_toDual_comp_iff, OrderDual.instPosSMulMono, ofDual_max, wellFoundedLT_dual_iff, isMin_toDual_iff, LeftOrdContinuous.rightOrdContinuous_dual, MonotoneOn.dual_left, OrderDual.continuousConstSMul', OrderIso.coe_dualDual_symm, Set.Ioi_ofDual, StrictAntiOn.dual_left, WithTop.toDual_top, supClosed_preimage_ofDual, Finset.uIcc_toDual, CategoryTheory.orderDualEquivalence_unitIso, SupBotHom.symm_dual_comp, OrderDual.instIsRightCancelAdd, TopHom.symm_dual_id, OrderDual.instIsLeftCancelAdd, OrderDual.instNonempty, Topology.isUpper_orderDual, OrderDual.instIsTopologicalGroup, sSupHom.symm_dual_id, List.sortedGT_map_ofDual, InfHom.symm_dual_comp, CompleteLatticeHom.dual_symm_apply_toFun, TopologicalSpace.Closeds.complOrderIso_symm_apply, isStronglyCoatomic_dual_iff_is_stronglyAtomic, OrderHom.dual_id, isBot_ofDual_iff, toDual_pow, WithTop.ofDual_symm, sInfHom.dual_id, instIsModularLatticeOrderDual, Finset.Ioi_toDual, AntivaryOn.dual, ProjectiveSpectrum.gc_homogeneousIdeal, OrderDual.addRightMono, SupHom.dual_id, instIsUpperModularLatticeOrderDual, isTop_toDual_iff, dist_toDual, OrderDual.instNeBotNhdsWithinIio, isCoatomic_dual_iff_isAtomic, Disjoint.dual, strictAntiOn_comp_ofDual_iff, ClosedSubmodule.orthogonal_gc, strictMono_dual_iff, OrderDual.mulLeftReflectLT, OrderDual.toDual_symm_eq, OrderDual.ofDual_bot, IsMinFilter.dual, Set.dual_ordConnectedSection, SupIrred.ofDual, Set.Ioc_ofDual, OrderIso.invENNReal_symm_apply, supIrred_ofDual, ofDual_inf, AlgebraicGeometry.Scheme.IdealSheafData.gc, WithTop.lt_toDual_iff, OrderDual.instIsDomain, isCompl_ofDual_iff, PrimeSpectrum.gc, OrderIso.neg_apply, BoundedLatticeHom.dual_id, BoundedOrderHom.symm_dual_id, StrictAntiOn.dual, toDual_vadd', OrderDual.Preorder.dual_dual, OrderDual.instIsScalarTower_1, WithTop.le_toDual_iff, isUpperSet_preimage_toDual_iff, IsArtinian.eventuallyConst_of_isArtinian, Codisjoint.dual, Antitone.dual_right, OrderDual.instIsUpper, isMinOn_dual_iff, List.SortedLT.of_map_ofDual, WithBot.ofDual_le_iff, ArchimedeanClass.FiniteResidueField.mk_eq_zero, Finset.map_ofDual_max, Lat.dual_map, ofDual_iInf, InfTopHom.symm_dual_comp, OrderDual.toDual_le_toDual, CategoryTheory.Localization.LeftBousfield.galoisConnection, OrderIso.subLeft_apply, toDual_sInf, OrderDual.instPartialOrder.dual_dual, LinOrd.dual_map, Finset.ofDual_inf, OrderIso.dualAntisymmetrization_symm_apply, instSeparableSpaceOrderDual, DistLat.dual_map, WCovBy.toDual, IsBot.toDual, Matrix.blockTriangular_transvection', BotHom.dual_apply_apply, OrderDual.instVAddCommClass_1, ofDual_min, TopologicalSpace.Opens.complOrderIso_apply, monotoneOn_comp_ofDual_iff, OrderIso.inv_symm_apply, CompleteLatticeHom.dual_id, toDual_smul', NonemptyInterval.coe_dual, OrderDual.instIsStrictOrderedModule, OrderDual.instMeasurableSup, Maximal.dual, OrderDual.borelSpace, ofDual_ofNat, instIsPredArchimedeanOrderDualOfIsSuccArchimedean, Monovary.dual_left, OrderDual.instMulArchimedean, IsLeast.dual, monotone_dual_iff, OrderDual.isBounded_preimage_ofDual, OrderDual.instIsCoatomistic, toDual_zero, NonemptyInterval.dual_top, BoundedLatticeHom.symm_dual_comp, TopologicalSpace.Opens.complOrderIso_symm_apply, isExtrFilter_dual_iff, antivaryOn_toDual_left, Finset.Ioc_ofDual, InfTopHom.dual_id, ofDual_hnot, SimpleGraph.hasseDualIso_apply, toDual_sSup, QuasilinearOn.dual, LatticeHom.dual_symm_apply_toFun, StrictMono.dual_right, OrderDual.supConvergenceClass, instFirstCountableTopologyOrderDual, nndist_toDual, OrderDual.instIsLower, instCompactIccSpaceOrderDual, toDual_eq_zero, WithBot.map_ofDual, ofDual_preimage_latticeClosure, StrictMonoOn.dual_left, ofDual_smul, AntivaryOn.dual_right, instSeparatelyContinuousMulOrderDual, OrderIso.smulRightDual_apply, Fin.revOrderIso_apply, isAddLeftRegular_ofDual, strictMonoOn_dual_iff, SupHom.symm_dual_comp, OrderIso.dualDual_apply, isLowerSet_preimage_toDual_iff, OrderDual.instIsAtomic, supPrime_toDual, dist_ofDual, NonemptyInterval.toDualProdHom_apply, Finset.toDual_min', toDual_compares_toDual, ArchimedeanClass.FiniteElement.val_add, Finset.Ioo_orderDual_def, Ordnode.Bounded.dual, OrderDual.denselyOrdered, edist_ofDual, OrderIso.dual_apply, gc_upperPolar_lowerPolar, OrderDual.isDirected_le, disjoint_toDual_iff, BoundedOrderHom.dual_apply_toOrderHom, instContinuousAddOrderDual, OrderDual.instPosSMulReflectLE, gc_upperBounds_lowerBounds, SemilatInfCat.dual_obj_X, infClosed_preimage_toDual, OrderDual.instIsLowerSet, toDual_sdiff, MonovaryOn.dual_left, PartOrd.dual_map, OrderDual.instSMulPosStrictMono, ofDual_himp, norm_ofDual, OrderDual.instMeasurableInf₂, OrderDual.toDual_inj, OrderDual.instPosSMulReflectLT, pow_toDual, monovary_toDual_right, WithBot.ofDual_apply_coe, List.SortedGE.map_ofDual, IsSublattice.of_dual, AddValuation.toValuation_ofValuation, InfHom.dual_apply_toFun, IsGalois.intermediateFieldEquivSubgroup_apply, OrderDual.instIsScalarTower_2, IsAntichain.to_dual_iff, CategoryTheory.ComposableArrows.opEquivalence_unitIso_inv_app, OrderDual.instHasSolidNorm, TopHom.dual_symm_apply_apply, NonemptyInterval.dual_pure, ArchimedeanClass.FiniteElement.not_isUnit_iff_mk_pos, CategoryTheory.Abelian.subobjectIsoSubobjectOp_apply, Finset.Ioo_ofDual, OrderIso.coe_dualDual, toDual_wcovBy_toDual_iff, infPrime_ofDual, GaloisConnection.dual, OrderDual.instIsCountablyGeneratedAtBot, fixingAddSubmonoid_fixedPoints_gc, LatticeHom.dual_apply_toFun, Order.isPredPrelimit_toDual_iff, toDual_vadd, BoundedVariationOn.ofDual, ofDual_pow, isStronglyAtomic_dual_iff_is_stronglyCoatomic, InfHom.dual_id, WithTop.ofDual_apply_top, Interval.coe_dual, NonemptyInterval.fst_dual, LatticeHom.symm_dual_id, OrderDual.instIsRightCancelMul, OrderDual.instMeasurableInf, BddOrd.dual_map, OrderDual.instVAddAssocClass_1, Ordnode.Valid.dual, Set.Iio_toDual, ofAdd_bot, OrderIso.divLeft_apply, antitone_toDual_comp_iff, InfPrime.dual, WithBot.toDual_map, toDual_max, IsBot.ofDual, isMax_ofDual_iff, toDual_inv, SemilatticeInf.dual_dual, bddBelow_preimage_toDual, OrderDual.instAddArchimedean, Set.Ici_ofDual, OrderDual.mulLeftReflectLE, continuous_ofDual, OrderDual.instIsAtomistic, Iio_orderDual_def, Topology.isUpperSet_orderDual, instIsWeakUpperModularLatticeOrderDual, TopologicalSpace.Closeds.complOrderIso_apply, Antivary.dual_left, strictMono_comp_ofDual_iff, IsMax.toDual, Finset.map_toDual_max, ArchimedeanClass.FiniteElement.val_mul, WithBot.le_toDual_iff, instLipschitzAddOrderDual, OrderDual.instIsTransLt, IncidenceAlgebra.mu_ofDual, Interval.dual_top, InfHom.dual_symm_apply_toFun, cmp_toDual, WithTop.ofDual_lt_ofDual_iff, IsGreatest.dual, OrderDual.total_le, CommGroup.mem_subgroupOrderIsoSubgroupMonoidHom_iff, antitoneOn_toDual_comp_iff, WithBot.toDual_bot, BoundedOrderHom.dual_id, List.sortedGE_map_ofDual, ValuationSubring.primeSpectrumOrderEquiv_apply_coe_carrier, WithTop.toDualBotEquiv_symm_top, Set.uIoo_toDual, instClosedIciTopologyOrderDual, PrimitiveSpectrum.gc_closureOperator, CommGroup.mem_subgroupOrderIsoSubgroupMonoidHom_symm_iff, OrderHom.symm_dual_id, SupClosed.dual, SupHom.dual_comp, supIrred_toDual, OrderDual.instIsCountablyGeneratedAtTop, CategoryTheory.ComposableArrows.opEquivalence_functor_obj_map, OrderIso.sumDualDistrib_symm_inl, OrderDual.instSMulCommClass_2, ofDual_compares_ofDual, isAddRightRegular_ofDual, WithTop.toDual_lt_iff, OrderDual.ext_iff, isClosedMap_toDual, minimal_toDual, NonemptyInterval.toDualProd_strictMono, disjoint_ofDual_iff, toDual_intCast, Valuation.ofAddValuation_apply, instBoundedGENhdsClassOrderDual, BoundedOrderHom.symm_dual_comp, Set.dual_ordConnected, toDual_mul, sSupHom.dual_symm_apply_toFun, cmpLE_ofDual, OrderDual.instSMulPosReflectLE, monotone_toDual_comp_iff, strictAnti_toDual_comp_iff, sInfHom.dual_apply_toFun, OrderDual.instContinuousNeg, Interval.dual_bot, CovBy.toDual, NonemptyInterval.dual_map₂, InfHom.dual_comp, ofDual_sInf, Finset.toDual_inf', ProjectiveSpectrum.gc_set, toDual_compl, ArchimedeanClass.FiniteElement.val_sub, OrderDual.addLeftMono, OrderDual.toDual_lt_toDual, Valuation.toAddValuation_apply, SemilatSupCat.dual_map, IsArtinian.monotone_stabilizes, Submodule.orthogonal_gc, Finset.ofDual_sup', isAtomistic_dual_iff_isCoatomistic, IsMaxOn.dual, sSupHom.dual_apply_toFun, isClosedMap_ofDual, CategoryTheory.ComposableArrows.opEquivalence_functor_map_app, Monotone.dual_left, CategoryTheory.ObjectProperty.galoisConnection_isColocal, OrderDual.mulLeftStrictMono, PartOrdEmb.dual_map, BoundedLatticeHom.dual_symm_apply_toFun, WithBot.toDual_apply_bot, CategoryTheory.ComposableArrows.opEquivalence_inverse_obj, Set.uIcc_ofDual, CategoryTheory.MorphismProperty.gc_llp_rlp, RightOrdContinuous.orderDual, AntitoneOn.dual_right, OrderDual.instIsOrderBornology, isLowerSet_preimage_ofDual_iff, OrderIso.compl_symm_apply, Ioi_orderDual_def, MonovaryOn.dual_right, monovaryOn_toDual_right, antivary_toDual_right, toDual_min, CompleteLatticeHom.symm_dual_id, StrictAnti.dual_left, Finset.Icc_orderDual_def, Finset.Ioo_toDual, Concept.swapEquiv_apply, Set.Ico_toDual, Finset.map_toDual_min, WithBot.toDualTopEquiv_coe, ofDual_eq_one, ofDual_compl, IsTop.ofDual, codisjoint_ofDual_iff, Set.Icc_ofDual, ofDual_neg, isMax_toDual_iff, IsGaloisGroup.ofDual_intermediateFieldEquivSubgroup_apply, isAtom_dual_iff_isCoatom, isSimpleOrder_iff_isSimpleOrder_orderDual, Set.Ioo_ofDual, CategoryTheory.antitone_chain_condition_of_isArtinianObject, instBoundedLENhdsClassOrderDual, Order.IsSuccLimit.dual, CategoryTheory.Limits.kernelOrderHom_coe, OrderDual.instIsCancelMul, IsGalois.intermediateFieldEquivSubgroup_symm_apply_toDual, strictMonoOn_toDual_comp_iff, isRightRegular_toDual, List.SortedGT.of_map_ofDual, IsGLB.dual, LatticeHom.dual_id, Antitone.dual, Fin.revOrderIso_toEquiv, CategoryTheory.ComposableArrows.opEquivalence_unitIso_hom_app, isExtrOn_dual_iff, InfIrred.dual, toDual_hnot, BddDistLat.dual_map, ofDual_ratCast, Set.uIcc_toDual, StrictMono.dual_left, WithTop.ofDual_apply_coe, MulChar.mem_subgroupOrderIsoSubgroupMulChar_symm_iff, Set.Ioc_toDual, WithTop.toDual_apply_top, OrderDual.instContinuousVAdd_left, Iic_orderDual_def, SupHom.symm_dual_id, nnnorm_toDual, Valuation.ofAddValuation_toAddValuation, FinPartOrd.dual_map, CompleteLat.dual_map, InfTopHom.dual_comp, SemilatticeSup.dual_dual, maximal_toDual, OrderDual.instContinuousVAdd_right, BoundedLatticeHom.symm_dual_id, List.sortedLE_map_toDual, OrderDual.topologicalLattice, OrderDual.instContinuousInv, Order.IsPredLimit.dual, SupBotHom.dual_id, gc_Ici_sInf, IsMin.ofDual, LinearMap.polar_gc, LE.le.dual, BoundedOrderHom.dual_comp, List.SortedGT.map_toDual, WithBot.toDual_le_iff, OrderDual.instIsCancelAdd, WithBot.ofDual_lt_iff, ArchimedeanClass.FiniteResidueField.mk_eq_mk, Interval.dual_pure, Finset.Ico_ofDual, WithBot.toDual_apply_coe, Finset.toDual_inf, AddValuation.ofValuation_toValuation, instWellFoundedGTOrderDualOfWellFoundedLT, Finset.Ioc_orderDual_def, Finset.toDual_max', Order.PFilter.sInf_gc, MulChar.mem_subgroupOrderIsoSubgroupMulChar_iff, List.SortedLE.map_ofDual, WithBot.toDual_lt_toDual_iff, List.sortedLT_map_ofDual, OrderIso.dualAntisymmetrization_apply, OrderDual.instIsTopologicalAddGroup, antitoneOn_comp_ofDual_iff, OrderDual.toDual_le, OrderDual.mulLeftMono, instWellFoundedLTOrderDualOfWellFoundedGT, WCovBy.ofDual, codisjoint_toDual_iff, WithBot.ofDual_lt_ofDual_iff, WithTop.ofDual_le_ofDual_iff, antitone_dual_iff, AntitoneOn.dual_left, ofDual_one, Finset.Ioc_toDual, Set.Iic_toDual, WithTop.toDual_lt_toDual_iff, ofDual_iSup, Set.dual_ordSeparatingSet, ConvexOn.dual, OrderHom.dual_comp, WithBot.ofDual_symm_apply, Monotone.dual_right, Finset.Icc_toDual, BoolAlg.dual_map, Valuation.toAddValuation_symm_eq, OrderDual.instPosSMulStrictMono, sSupHom.dual_comp, List.SortedGT.map_ofDual, Monovary.dual_right, ArchimedeanClass.FiniteElement.val_zero, InfPrime.ofDual, OrderDual.instVAddCommClass_2, isAddRightRegular_toDual, OrderDual.mulRightStrictMono, WithBot.toDualTopEquiv_symm_bot, OrderDual.instLeftDistribClass, LatticeHom.symm_dual_comp, gc_upperClosure_coe, ArchimedeanClass.FiniteElement.isUnit_iff_mk_eq_zero, WithTop.toDual_symm_apply, WithTop.ofDual_map, sInfHom.dual_comp, WithTop.map_toDual, isLeftRegular_ofDual, List.SortedLE.of_map_ofDual, List.SortedGT.of_map_toDual, instContinuousConstVAddOrderDual, List.SortedLT.of_map_toDual, Matrix.BlockTriangular.transpose, OrderDual.instNontrivial, IsGalois.intermediateFieldEquivSubgroup_symm_apply, Finset.Ioi_ofDual, OrderDual.instSMulPosMono, ArchimedeanClass.FiniteResidueField.mk_ne_zero, denselyOrdered_orderDual, NonemptyFinLinOrd.dual_map, Submodule.dualAnnihilator_gc, Order.isPredLimit_toDual_iff, bddBelow_preimage_ofDual, BddBelow.dual, OrderIso.neg_symm_apply, MonotoneOn.dual, toDual_sub, infClosed_preimage_ofDual, continuous_toDual, OrderDual.noMinOrder, WithBot.lt_toDual_iff, Monotone.dual, BoundedLatticeHom.dual_apply_toFun, Antitone.dual_left, OrderDual.continuousConstVAdd', sInfHom.dual_symm_apply_toFun, WithBot.toDualTopEquiv_symm_coe, OrderDual.instSMulPosReflectLT, LE.le.ofDual, OrderIso.sumDualDistrib_inl, Matrix.blockTriangular_transpose_iff, Finset.Ici_toDual, WithTop.toDual_symm, OrderDual.toDual_top, WithBot.ofDual_bot, OrderIso.invENNReal_apply, isBot_toDual_iff, Order.PFilter.mem_mk, wellFoundedGT_dual_iff, SupPrime.dual, ProjectiveSpectrum.gc_ideal, Set.Iic_ofDual, nhds_ofDual, Order.IsPredPrelimit.dual, WithTop.toDual_le_toDual_iff, OrderDual.addRightReflectLT, Order.isSuccLimit_toDual_iff, QuasiconvexOn.dual, Set.Ioo_toDual, ofDual_natCast, ArchimedeanClass.FiniteElement.val_one, IsAtom.dual, ofDual_intCast, OrderDual.exists, isAddLeftRegular_toDual, Preord.dual_map, strictAnti_dual_iff, Set.Iio_ofDual, CategoryTheory.orderDualEquivalence_counitIso, OrderIso.sumDualDistrib_symm_inr, PrimeSpectrum.gc_set, OrderDual.isOrderedAddCancelMonoid, Finset.Icc_ofDual, Set.ordConnected_dual, infPrime_toDual, BotHom.dual_symm_apply_apply, OrderDual.instSMulCommClass_1, isCoatomistic_dual_iff_isAtomistic, CategoryTheory.orderDualEquivalence_functor_obj, Fin.revOrderIso_symm_apply, WithTop.le_ofDual_iff, OrderDual.addRightStrictMono, Finset.Iio_toDual, isUpperSet_preimage_ofDual_iff, toDual_neg, monotoneOn_toDual_comp_iff, WithBot.le_ofDual_iff, SupBotHom.symm_dual_id, Finset.ofDual_min', IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply, OrderDual.forall, StrictAnti.dual, IsLUB.dual, Finset.Iic_ofDual, OrderDual.instSMulCommClass, OrderDual.instVAddAssocClass, Finset.toDual_sup, BddAbove.dual, List.SortedGE.of_map_ofDual, OrderDual.noBotOrder, OrderDual.instLinearOrder.dual_dual, OrderDual.instIsOrderedModule, Submodule.torsion_gc, Order.krullDim_orderDual, IsCompl.ofDual, CategoryTheory.isArtinianObject_iff_antitone_chain_condition, TopHom.symm_dual_comp, fixingSubmonoid_fixedPoints_gc, WithTop.toDualBotEquiv_symm_coe, OrderDual.lt_toDual, BoundedOrderHom.dual_symm_apply_toOrderHom, isAddRegular_ofDual, ofDual_wcovBy_ofDual_iff, ofDual_toAdd_eq_top_iff, StrictAnti.dual_right, infIrred_toDual, Set.Ioi_toDual, isOpenMap_ofDual, OrderDual.instVAddCommClass, List.sortedGT_map_toDual, StrictMono.dual, OrderDual.noMaxOrder, eVariationOn.comp_ofDual, CategoryTheory.orderDualEquivalence_functor_map, LatticeHom.dual_comp, antitoneOn_dual_iff, OrderDual.opensMeasurableSpace, OrderDual.instIsCoatomic, OrderDual.instIsScalarTower, OrderIso.sumLexDualAntidistrib_symm_inl, infIrred_ofDual, isAtomic_dual_iff_isCoatomic, OrderDual.infConvergenceClass, WithBot.ofDual_symm, isRightRegular_ofDual, WithTop.ofDual_le_iff, OrderDual.toDual_trans_ofDual, SemilatInfCat.dual_map, AddValuation.toValuation_apply, Set.OrdConnected.dual, OrderDual.instNeBotNhdsWithinIoi, List.sortedLT_map_toDual, instIsLowerModularLatticeOrderDual, OrderDual.instIsUpperSet, OrderDual.instTrichotomousLt, WithBot.toDualTopEquiv_bot, OrderDual.finite, supClosed_preimage_toDual, MvPolynomial.zeroLocus_vanishingIdeal_galoisConnection, OrderDual.toDual_eq_top, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe', nucleusIsoSublocale.eq_toSublocale, nnnorm_ofDual, TopologicalSpace.gc_generateFrom, TopHom.dual_apply_apply, OrderDual.le_toDual, OrderDual.instDiscreteTopology, WithBot.toDual_lt_iff, OrderDual.toDual_lt, OrderHom.symm_dual_comp, IsExtrFilter.dual, OrderDual.instIsCancelMulZero, SetRel.gc_leftDual_rightDual, List.SortedLE.of_map_toDual, instIsStronglyAtomicOrderDualOfIsStronglyCoatomic, OrderDual.toDual_comp_ofDual, BotHom.symm_dual_id, ofDual_sup, instOrderClosedTopologyOrderDual, AntivaryOn.dual_left, OrderIso.inv_apply, instSeparatelyContinuousAddOrderDual, sInfHom.symm_dual_comp, WithBot.toDual_le_toDual_iff, CategoryTheory.ComposableArrows.opEquivalence_inverse_map, LinearMap.iterateRange_coe, IsGaloisGroup.intermediateFieldEquivSubgroup_apply, ofDual_sub, IsAntichain.to_dual, OrderDual.ofDual_symm_eq, fixingAddSubgroup_fixedPoints_gc, Finset.Ico_orderDual_def, monovary_toDual_left, sSupHom.symm_dual_comp, OrderIso.compl_apply, WithTop.ofDual_lt_iff, instOrderTopologyOrderDual, Set.uIoo_ofDual, toDual_bihimp, List.sortedGE_map_toDual, OrderIso.subLeft_symm_apply, bddAbove_preimage_ofDual, OrderDual.instIsLeftCancelMul, norm_toDual, nucleusIsoSublocale.symm_eq_toNucleus, ofDual_symmDiff, ofDual_inv, isMaxFilter_dual_iff, isLeftRegular_toDual, fixingSubgroup_fixedPoints_gc, BoundedLatticeHom.dual_comp, antivaryOn_toDual_right, OrderDual.instNoZeroDivisors, MonotoneOn.dual_right, OrderDual.toDual_bot, isRegular_toDual, LT.lt.dual, OrderDual.addRightReflectLE, Finset.ofDual_inf', Topology.isLowerSet_orderDual, monotone_stabilizes_iff_artinian, OrderDual.mulRightMono, IsLowerSet.toDual, Fintype.card_orderDual, List.sortedLE_map_ofDual, OrderHom.dual_apply_coe, OrderDual.continuousInf, InfHom.symm_dual_id, StrictConvexOn.dual, instContinuousMulOrderDual, OrderIso.sumDualDistrib_inr, grade_ofDual, CompleteLatticeHom.dual_apply_toFun, IsExtrOn.dual, OrderDual.total_ge, IsUpperSet.toDual, antivary_toDual_left, OrderDual.toDual_eq_bot, WithTop.ofDual_symm_apply, OrderDual.addLeftReflectLT, Order.isSuccPrelimit_toDual_iff, Set.dual_ordConnected_iff, OrderDual.instSubsingleton, Antivary.dual_right, OrderDual.ofDual_toDual, OrderHom.dual_symm_apply_coe, OrderDual.instIsTransLe, WithBot.toDual_symm_apply, instBoundedSpaceOrderDual, Finset.Iic_toDual, CompleteLatticeHom.dual_comp, Ordnode.dual_insert, BotHom.symm_dual_comp, ComplementedLattice.instOrderDual, Monovary.dual, List.SortedLT.map_ofDual, OrderIso.smulRightDual_symm_apply, BotHom.dual_comp, OrderDual.noTopOrder, antitone_comp_ofDual_iff, Ici_orderDual_def, QuasiconcaveOn.dual, WithTop.toDual_map, isMaxOn_dual_iff, BotHom.dual_id, instIsSuccArchimedeanOrderDualOfIsPredArchimedean, AddValuation.toValuation_symm_eq, InfClosed.dual, isTop_ofDual_iff, isMin_ofDual_iff, IsSublattice.dual, TopHom.dual_comp, IsCoatom.dual, ValuationSubring.coe_primeSpectrumOrderEquiv_symm_apply_asIdeal, IsCompl.dual, OrderDual.addLeftReflectLE, ofDual_bihimp, OrderDual.Ord.dual_dual, Finset.map_ofDual_min, OrderIso.divLeft_symm_apply, Valuation.toValuation_ofValuation, isMinFilter_dual_iff, isSublattice_preimage_toDual, OrderDual.isCobounded_preimage_ofDual, SupIrred.dual, toDual_eq_one, Interval.dual_map, ofDual_add, Ordnode.Valid'.dual, SimpleGraph.hasseDualIso_symm_apply, supPrime_ofDual, toDual_symmDiff, Topology.isLower_orderDual, StrictConcaveOn.dual, toDual_smul, AddValuation.ofValuation_symm_eq, monotone_comp_ofDual_iff, ofDual_sSup, instLipschitzMulOrderDual, WithBot.toDual_symm, isAddRegular_toDual, OrderDual.instContinuousSMul_right, IsMin.toDual, OrderDual.ofDual_trans_toDual, ofDual_vadd', CategoryTheory.ObjectProperty.galoisConnection_isLocal, isRegular_ofDual, CategoryTheory.orderDualEquivalence_inverse_obj, edist_toDual, IncidenceAlgebra.eulerChar_orderDual, toDual_iInf, instHasUpperLowerClosureOrderDual, SupHom.dual_symm_apply_toFun, WithTop.toDual_le_iff, OrderDual.ofDual_lt_ofDual, OrderDual.ofDual_comp_toDual, Ordnode.Bounded.dual_iff, monotoneOn_dual_iff, FinBddDistLat.dual_map, toDual_sup, WithTop.ofDual_top, toDual_iSup, WithTop.lt_ofDual_iff, IsTop.toDual, toDual_ofNat, OrderDual.isOrderedCancelMonoid, toDual_div, NonemptyInterval.snd_dual, Concept.swapEquiv_symm_apply, CategoryTheory.ComposableArrows.opEquivalence_counitIso_hom_app_app, ofDual_mul, Set.Ici_toDual, Set.Icc_toDual, sSupHom.dual_id, OrderDual.isCobounded_preimage_toDual, OrderIso.sumLexDualAntidistrib_symm_inr, IncidenceAlgebra.mu_toDual, nhds_toDual, StrictMonoOn.dual_right, OrderIso.sumLexDualAntidistrib_inr, OrderDual.instContinuousSMul_left, CompleteLatticeHom.symm_dual_comp, instProperSpaceOrderDual, NonemptyInterval.toDualProd_apply, OrderDual.isOrderedAddMonoid, toDual_ratCast, OrderDual.instVAddAssocClass_2, Dense.orderDual, OrderDual.ofDual_inj, OrderDual.isDirected_ge, FinBoolAlg.dual_map, NonemptyInterval.toDualProd_injective, OrderDual.continuousSup, grade_toDual, strictMonoOn_comp_ofDual_iff, Ordnode.Valid'.dual_iff, StrictMonoOn.dual, CategoryTheory.Abelian.subobjectIsoSubobjectOp_symm_apply, ofAdd_toDual_eq_zero_iff, OrderDual.ofDual_eq_top, isCoatom_dual_iff_isAtom, toDual_natCast, strictMono_toDual_comp_iff, CovBy.ofDual, ofDual_vadd, toDual_add, LT.lt.ofDual, Finset.ofDual_max', CategoryTheory.Limits.cokernelOrderHom_coe, OrderIso.dual_symm_apply, AddValuation.supp_quot_supp, AddValuation.ofValuation_apply, ofDual_covBy_ofDual_iff, instContinuousConstSMulOrderDual, bddAbove_preimage_toDual, ofDual_div, Matrix.blockTriangular_single', BddLat.dual_map, OrderIso.sumLexDualAntidistrib_inl, MonovaryOn.dual, Order.coheight_ofDual, OrderDual.instRightDistribClass, IsMinOn.dual, OrderDual.mulRightReflectLE, Finset.ofDual_sup, cmpLE_toDual, PrimitiveSpectrum.gc, toDual_covBy_toDual_iff, IsMax.ofDual, ofDual_zero, SupPrime.ofDual, List.SortedGE.of_map_toDual, Valuation.ofAddValuation_symm_eq, toDual_inf, ofDual_eq_zero, strictAntiOn_dual_iff, monovaryOn_toDual_left, CategoryTheory.orderDualEquivalence_inverse_map, cmp_ofDual, WithBot.ofDual_le_ofDual_iff, OrderDual.instIsStronglyCoatomic, Order.height_toDual, WithTop.toDual_apply_coe, Finset.Ico_toDual, Antivary.dual, ConcaveOn.dual, strictAnti_comp_ofDual_iff, OrderDual.mulRightReflectLT, WithTop.coe_toDualBotEquiv, gc_lowerPolar_upperPolar, WithBot.map_toDual, Minimal.dual, StrictAntiOn.dual_right, isOpenMap_toDual, OrderDual.instIsLeftCancelMulZero, ArchimedeanClass.FiniteElement.ext_iff, IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply_toDual, OrderDual.addLeftStrictMono, OrderDual.toDual_ofDual, instSecondCountableTopologyOrderDual, WithTop.toDualBotEquiv_top, OrderDual.isOrderedMonoid, toDual_one, Finset.Iio_ofDual, Order.coheight_toDual, Finset.Ici_ofDual, TopHom.dual_id, IsMaxFilter.dual, OrderDual.instIsSimpleOrder, InfIrred.ofDual, ofDual_smul', Set.Ico_ofDual, nndist_ofDual, Finset.toDual_sup', OrderDual.ofDual_top, IsGalois.ofDual_intermediateFieldEquivSubgroup_apply, OrderIso.dualDual_symm_apply, instClosedIicTopologyOrderDual, AntitoneOn.dual, OrderIso.symm_dual, sInfHom.symm_dual_id, WithBot.ofDual_apply_bot, SupHom.dual_apply_toFun, OrderDual.ofDual_eq_bot
|