OrderEmbedding ๐ | CompOp | 398 mathmath: Cardinal.aleph_le_beth, Set.IsPWO.exists_monotone_subseq, Ordinal.principal_add_omega, Field.Emb.Cardinal.equivLim_coherence, OrderEmbedding.supIrredLowerSet_apply, OrderEmbedding.sorted_ge_listMap, RightOrdContinuous.coe_toOrderEmbedding, integralClosure_le_span_dualBasis, OrderEmbedding.birkhoffFinset_inf, Subalgebra.toSubmodule_injective, BoxIntegral.TaggedPrepartition.tag_mem_Icc, Cardinal.aleph_succ, Finset.image_orderEmbOfFin_univ, OrderEmbedding.sorted_lt_listMap, finSumEquivOfFinset_inr, Finset.add_sum_eq_sum_insertNone, OrderEmbedding.monotone, Cardinal.aleph_pos, OrderEmbedding.le_map_sup, OrderEmbedding.image_Ioc, Ordinal.omega_lt_omega, Ordinal.omega0_lt_omega_one, Submodule.mulMap_one_right_eq, Finset.orderEmbOfFin_unique, Field.Emb.Cardinal.directed_filtration, BoxIntegral.Box.upper_mem_Icc, BoxIntegral.Box.measurableSet_Icc, OrderEmbedding.infIrredUpperSet_surjective, Cardinal.ord.orderEmbedding_coe, Ordinal.omega0_lt_preOmega_iff, Field.Emb.Cardinal.instInverseSystemWithTopToTypeOrdRankAlgHomSubtypeMemIntermediateFieldCoeOrderEmbeddingFiltrationAlgebraicClosureEmbFunctor, Cardinal.lift_eq_aleph_one, Ordinal.card_le_aleph, Composition.embedding_comp_inv, Ordinal.omega_zero, Nat.orderEmbeddingOfSet_apply, InitialSeg.toOrderEmbedding_apply, OrderEmbedding.maximal_mem_image, Nat.coe_orderEmbeddingOfSet, IsChain.preimage_embedding, UnitAddTorus.mFourierSubalgebra_coe, Ordinal.toGame_lt_iff, IsChain.image_embedding_iff, Composition.blocksFun_sigmaCompositionAux, Ordinal.omega_le_omega, Finset.card_insertNone, OrderEmbedding.preimage_uIoc, Ordinal.isInitial_preOmega, OrderEmbedding.preimage_Ici, OrderEmbedding.preimage_Icc, Subalgebra.mulMap_toLinearMap, BoxIntegral.Box.le_iff_Icc, Submonoid.adjoin_eq_span_of_eq_span, Ordinal.toGame_one, OrderEmbedding.preimage_Iic, Ordinal.range_omega, BoxIntegral.Prepartition.card_filter_mem_Icc_le, Ordinal.cof_preOmega, OrderEmbedding.preimage_Ioc, Algebra.span_le_adjoin, Finset.orderEmbOfFin_eq_orderEmbOfFin_iff, Cardinal.preAleph_le_aleph, OrderEmbedding.coe_ofStrictMono, Set.PartiallyWellOrderedOn.exists_monotone_subseq, Finset.insertNone_eraseNone, OrderEmbedding.toOrderHom_coe, BoxIntegral.Box.isCompact_Icc, Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective, Subalgebra.mem_toSubmodule, Subalgebra.range_isScalarTower_toAlgHom, GradeMinOrder.exists_nat_orderEmbedding_of_forall_covby_finite, Cardinal.aleph_one_le_continuum, Algebra.toSubmodule_bot, Cardinal.aleph_mul_aleph0, CovBy.image, OrderEmbedding.coe_birkhoffFinset, PartOrdEmb.comp_apply, Algebra.sInf_toSubmodule, exists_increasing_or_nonincreasing_subseq, PartOrdEmb.hom_inv_apply, instFullFunctor, Cardinal.aleph_add_aleph, WithBot.Ico_bot_coe, Subalgebra.finrank_toSubmodule, BoxIntegral.Box.measure_Icc_lt_top, Ordinal.mem_range_omega_iff, Subalgebra.isIdempotentElem_toSubmodule, nonempty_orderEmbedding_of_finite_infinite, Cardinal.lt_omega_iff_card_lt, StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, span_coeff_minpolyDiv, Cardinal.aleph1_le_lift, OrderEmbedding.image_Ioo, OrderEmbedding.minimal_mem_image, PartOrdEmb.Limits.CoconePt.fac_apply, Algebra.top_toSubmodule, Finset.coe_orderIsoOfFin_apply, Cardinal.le_aleph_ord, OrderEmbedding.sortedLT_listMap, OrderEmbedding.birkhoffSet_inf, exists_increasing_or_nonincreasing_subseq', cardinalInterFilter_aleph_one_iff, BoxIntegral.Box.coe_ae_eq_Icc, OrderEmbedding.strictMono, OrderEmbedding.infIrredUpperSet_apply, FirstOrder.Language.LHom.coe_substructureReduct, CompositionAsSet.blocks_partial_sum, BoxIntegral.Box.Ioo_ae_eq_Icc, OrderIso.coe_toOrderEmbedding, Submodule.toSubalgebra_toSubmodule, Composition.index_embedding, Cardinal.aleph_le_aleph, traceForm_dualSubmodule_adjoin, FractionalIdeal.adjoinIntegral_coe, Subalgebra.mul_toSubmodule, Algebra.adjoin_nonUnitalSubalgebra_eq_span, SetTheory.Game.birthday_ordinalToGame, PartOrdEmb.ofHom_apply, HahnSeries.embDomain_single, SetTheory.Game.le_birthday, Finset.orderEmbOfFin_zero, SSet.stdSimplex.nonDegenerateEquiv_apply_apply, Finset.none_mem_insertNone, Finset.mul_prod_eq_prod_insertNone, Order.exists_orderEmbedding_insert, PartOrdEmb.Limits.cocone_ฮน_app, HahnSeries.embDomain_coeff, FractionalIdeal.isFractional_adjoin_integral, Cardinal.ord_aleph, Composition.boundary_zero, mem_integralClosure_iff_mem_fg, exists_orderEmbedding_covby_of_forall_covby_finite, Finset.orderEmbOfFin_last, FirstOrder.Language.Substructure.skolemโ_reduct_isElementary, Affine.Simplex.face_points, Finset.range_orderEmbOfFin, Subalgebra.adjoin_eq_span_basis, Ordinal.isNormal_preOmega, Field.Emb.Cardinal.equivSucc_coherence, Ordinal.preOmega_ofNat, BoxIntegral.Box.lower_mem_Icc, Finset.orderEmbOfFin_singleton, Ordinal.preOmega_le_omega, Cardinal.isRegular_aleph_succ, Finset.coe_coeEmb, Set.powersetCard.ofFinEmbEquiv_symm_apply, Ordinal.principal_mul_omega, Cardinal.aleph1_lt_lift, Submodule.map_subtype_embedding_eq, DFinsupp.coe_orderEmbeddingToFun, Subalgebra.mul_toSubmodule_le, FiniteArchimedeanClass.subsemigroup_eq_addSubgroup, Module.Flat.instSubalgebraToSubmodule, OrderEmbedding.maximal_mem_image_iff, partOrdEmb_dual_comp_forget_to_pardOrd, Cardinal.isNormal_aleph, Algebra.adjoin_toSubmodule_le, Set.isPWO_iff_exists_monotone_subseq, exteriorPower.ฮนMultiDual_apply_ฮนMulti, Subalgebra.LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent, OrderEmbedding.withTopMap_apply, Cardinal.lift_eq_aleph1, PartOrdEmb.coe_comp, BoxIntegral.Box.Icc_def, OrderEmbedding.preimage_uIcc, FirstOrder.Language.Substructure.reduct_withConstants, Algebra.inf_toSubmodule, BoxIntegral.Box.isBounded_Icc, Algebra.adjoin_eq_span_of_subset, Finset.sum_insertNone, Cardinal.aleph_max, Cardinal.ord_preAleph, Field.Emb.Cardinal.eq_bot_of_not_nonempty, Subalgebra.linearDisjoint_iff, Ordinal.omega0_lt_omega1, OrderEmbedding.supIrredLowerSet_surjective, PartOrdEmb.inv_hom_apply, Ordinal.mk_toPGame, Submodule.comapMkQOrderEmbedding_eq, Ordinal.preOmega_zero, Finset.orderEmbOfCardLe_mem, exteriorPower.pairingDual_apply_apply_eq_one, Ordinal.coe_preOmega, Fin.OrderEmbedding.default_def, Subalgebra.map_toSubmodule, Ordinal.omega0_le_omega, FirstOrder.Language.order.instStrongHomClassOrderEmbedding, PartOrdEmb.id_apply, BoxIntegral.Box.mapsTo_insertNth_face_Icc, Ordinal.toGame_zero, IsAntichain.preimage_embedding, WellQuasiOrdered.exists_monotone_subseq, Submodule.span_range_natDegree_eq_adjoin, Cardinal.range_aleph, Finset.some_mem_insertNone, Algebra.iInf_toSubmodule, fourierSubalgebra_coe, OrderEmbedding.sortedGE_listMap, OrderEmbedding.preimage_Iio, BoxIntegral.Box.Ioo_subset_Icc, OrderEmbedding.image_setOf_maximal, Cardinal.aleph_one_le_lift, BoxIntegral.Box.exists_seq_mono_tendsto, Subalgebra.finiteDimensional_toSubmodule, Ordinal.isInitial_omega, PartOrdEmb.forget_map, LeftOrdContinuous.coe_toOrderEmbedding, Subalgebra.toSubmodule_toSubalgebra, Algebra.adjoin_union_coe_submodule, Submodule.mulMap_one_left_eq, OrderEmbedding.maximal_apply_mem_inter_range_iff, Cardinal.lift_le_aleph1, BoxIntegral.Box.diam_Icc_le_of_distortion_le, OrderEmbedding.birkhoffSet_sup, Composition.mem_range_embedding, Ordinal.toGame_nmul, fg_adjoin_of_finite, OrderEmbedding.image_setOf_minimal, Ordinal.le_preOmega_self, Ordinal.toGame_lf_iff, Composition.invEmbedding_comp, PartOrdEmb.Limits.instPreservesColimitsOfShapeForgetOrderEmbeddingCarrier, Algebra.adjoin_eq_span, CliffordAlgebra.even_toSubmodule, Algebra.toSubmodule_eq_top, Composition.mem_range_embedding_iff', Ordinal.card_omega, Cardinal.lift_aleph, Finset.orderEmbOfFin_apply, Ordinal.omega0_le_preOmega_iff, OrderType.type_le_type_iff, Subalgebra.pi_toSubsemiring, BoxIntegral.Prepartition.injOn_setOf_mem_Icc_setOf_lower_eq, Ordinal.lift_preOmega, Cardinal.aleph0_le_aleph, Finset.intervalGapsWithin_snd_of_lt, NonemptyInterval.coe_coeHom, Set.powersetCard.mem_ofFinEmbEquiv_iff_mem_range, Ordinal.omega_strictMono, Finset.intervalGapsWithin_succ_fst_of_lt, BoxIntegral.TaggedPrepartition.IsSubordinate.diam_le, OrderEmbedding.minimal_mem_image_iff, OrderEmbedding.gtEmbedding_apply, List.sublist_iff_exists_fin_orderEmbedding_get_eq, OrderEmbedding.preimage_Ico, Cardinal.aleph0_lt_aleph_one, Composition.ones_embedding, IsAntichain.image_embedding_iff, Order.embedding_from_countable_to_dense, OrderEmbedding.orderIso_apply, PartOrdEmb.Hom.injective, Ordinal.toGame_inj, Subalgebra.coe_pi, OrderEmbedding.image_Icc, Cardinal.aleph_mul_aleph, IsAntichain.image_embedding, OrderEmbedding.minimal_apply_mem_inter_range_iff, SetTheory.Game.neg_birthday_le, Cardinal.isRegular_aleph_one, PartOrdEmb.Hom.le_iff_le, BoxIntegral.Box.Icc_eq_pi, Cardinal.lift_le_aleph_one, Finset.intervalGapsWithin_fst_of_lt_lt, Finset.prod_insertNone, Ordinal.preOmega_strictMono, Ordinal.principal_opow_omega, Ordinal.card_preOmega, OrderEmbedding.subtype_apply, WithTop.top_mem_insertTop, OrderEmbedding.coe_ofIsEmpty, Finset.insertNone_nonempty, Nat.nth_eq_orderEmbOfFin, BoxIntegral.Box.coe_subset_Icc, Cardinal.aleph1_eq_lift, Composition.disjoint_range, OrderEmbedding.sortedLE_listMap, RelEmbedding.orderEmbeddingOfLTEmbedding_apply, univ_option, exteriorPower.pairingDual_apply_apply_eq_one_zero, Subalgebra.coe_toSubmodule, MeasurableSpace.generateMeasurableRec_omega_one, OrderEmbedding.birkhoffSet_apply, Finset.mapEmbedding_apply, PartOrdEmb.Limits.instPreservesFilteredColimitsOfSizeForgetOrderEmbeddingCarrier, PartOrdEmb.ext_iff, Nat.exists_subseq_of_forall_mem_union, Subalgebra.restrictScalars_toSubmodule, FiniteMulArchimedeanClass.subsemigroup_eq_subgroup, StarAlgebra.adjoin_eq_span, wellQuasiOrdered_iff_exists_monotone_subseq, Set.OrdConnected.apply_covBy_apply_iff, Ordinal.mem_range_preOmega_iff, Submodule.iSup_eq_toSubmodule_range, Ordinal.omega_max, Nat.orderEmbeddingOfSet_range, Set.OrdConnected.apply_wcovBy_apply_iff, OrderEmbedding.sorted_le_listMap, Cardinal.aleph_eq_preAleph, Ordinal.omega_pos, OrderEmbedding.lt_iff_lt, IsIntegral.fg_adjoin_singleton, OrderEmbedding.preimage_Ioi, Composition.boundary_last, WithTop.Ioc_coe_top, Ordinal.toGame_injective, CountableInterFilter.toCardinalInterFilter, Cardinal.aleph_one_eq_lift, OrderEmbedding.isEmbedding_of_ordConnected, Cardinal.aleph_toENat, Cardinal.countable_iff_lt_aleph_one, MvPolynomial.range_mapAlgHom, FormalMultilinearSeries.applyComposition_update, OrderEmbedding.range_inj, IsChain.image_embedding, OrderEmbedding.sortedGT_listMap, OrderEmbedding.coe_subtype, OrderEmbedding.ltEmbedding_apply, MeasurableSpace.generateMeasurableRec_omega1, FiniteDimensional.subalgebra_toSubmodule, Field.Emb.Cardinal.iSup_filtration, Cardinal.aleph_limit, Set.partiallyWellOrderedOn_iff_exists_monotone_subseq, OrderEmbedding.map_inf_le, Ordinal.preOmega_le_preOmega, FirstOrder.Language.LHom.mem_substructureReduct, Ordinal.lift_omega, Ordinal.preOmega_omega0, OrderEmbedding.preimage_Ioo, OrderEmbedding.coe_ofMapLEIff, Cardinal.aleph0_mul_aleph, Ordinal.preOmega_lt_preOmega, Cardinal.lift_lt_aleph1, HahnSeries.support_embDomain_subset, OrderEmbedding.le_iff_le, CompositionAsSet.boundary_length, WithTop.some_mem_insertTop, Subalgebra.pointwise_smul_toSubmodule, Set.powersetCard.mem_range_ofFinEmbEquiv_symm_iff_mem, Cardinal.isSuccLimit_omega, Ordinal.cof_omega, Cardinal.aleph_one_lt_lift, Affine.Simplex.face_points', WithTop.Icc_coe_top, Subalgebra.prod_toSubmodule, BoxIntegral.unitPartition.diam_boxIcc, Finset.orderEmbOfFin_mem, Ordinal.preOmega_natCast, PartOrdEmb.Limits.instPreservesColimitForgetOrderEmbeddingCarrier, Composition.coe_embedding, Finset.listMap_orderEmbOfFin_finRange, Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, PartOrdEmb.coe_id, Cardinal.mem_range_aleph_iff, Cardinal.aleph_lt_aleph, SSet.stdSimplex.nonDegenerateEquiv_symm_apply_coe, AlgHom.equalizer_toSubmodule, HahnSeries.orderTop_embDomain, OrderEmbedding.withBotMap_apply, Subalgebra.pi_toSubmodule, WCovBy.image, OrderEmbedding.subtype_injective, OrderEmbedding.sorted_gt_listMap, Composition.mem_range_embedding_iff, finSumEquivOfFinset_inl, OrderEmbedding.image_Ico, Ordinal.IsInitial.mem_range_preOmega, Finset.eraseNone_insertNone, List.sublist_iff_exists_orderEmbedding_getElem?_eq, InitialSeg.coe_toOrderEmbedding, Cardinal.aleph_toNat, Ordinal.range_preOmega, Finset.orderEmbOfFin_compl_singleton_apply, Ordinal.preOmega_max, Ordinal.toGame_nadd, CompositionAsSet.boundary_zero, WithBot.some_mem_insertBot, Subalgebra.rank_toSubmodule, Cardinal.succ_aleph0, Subalgebra.fg_bot_toSubmodule, WithBot.bot_mem_insertBot, WithBot.Icc_bot_coe, Ordinal.toGame_natCast, Fin.coe_succOrderEmb, exists_orderEmbedding_covby_of_forall_covby_finite_of_bot, Ordinal.le_omega_self, Cardinal.aleph_zero, OrderEmbedding.birkhoffFinset_sup, Ordinal.toGame_le_iff, Ordinal.omega_eq_preOmega, Cardinal.lift_lt_aleph_one, Composition.single_embedding, OrderEmbedding.eq_iff_eq, DFinsupp.orderEmbeddingToFun_apply, Finset.mem_insertNone, Set.powersetCard.ofFinEmbEquiv_apply, Ordinal.isNormal_omega, MeasurableSpace.generateMeasurable_eq_rec, Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective
|