| Name | Category | Theorems |
|---|
IsStrongLimit 📖 | CompData | 8 mathmath: isStrongLimit_preBeth, isStrongLimit_aleph0, IsStrongLimit.univ, isInaccessible_def, isStrongLimit_beth, not_isStrongLimit_zero, IsInaccessible.isStrongLimit, isInaccesible_def
|
commSemiring 📖 | CompOp | 124 mathmath: toNat_ofENat, natCast_lt_toENat_iff, toNat_surjective, toNat_ofNat, Set.toENat_cardinalMk_subtype, toENat_eq_natCast_iff, Ideal.rank_prime_pow_ramificationIdx, toNat_eq_iff, toNat_congr, toENat_ofENat, Subfield.relrank_dvd_of_le_left, Module.length_of_free, sum_zero_pow, sum_pow_le_max_aleph0, mk_vector, toNat_mul, mk_list_eq_sum_pow, Submodule.spanRank_toENat_eq_iInf_encard, toENat_eq_zero, toENat_eq_ofNat, AddMonoidAlgebra.cardinalMk_lift_of_fintype, toNat_apply_of_aleph0_le, nsmul_lt_aleph0_iff_of_ne_zero, power_nat_le, Matrix.cRank_toNat_eq_rank, toENat_lt_natCast_iff, cast_toNat_eq_iff_lt_aleph0, toENat_lift, Matrix.cRank_toNat_eq_finrank, toNat_monotoneOn, toENat_le_ofNat, mk_toNat_eq_card, mk_univ_quaternionAlgebra, TensorAlgebra.rank_eq, nat_coe_dvd_iff, Ideal.height_le_spanRank_toENat_of_mem_minimal_primes, AddMonoidAlgebra.cardinalMk_of_fintype, IntermediateField.relrank_dvd_of_le_left, power_nat_eq, toNat_rightInverse, toNat_strictMonoOn, toNat_le_toNat, instCharZero, toNat_lt_iff_lt_of_lt_aleph0, toNat_lift, isUnit_iff, toNat_eq_one, toNat_toENat, IntermediateField.relfinrank_eq_toNat_relrank, Subfield.relfinrank_eq_toNat_relrank, toENat_rank_span_set, mk_finsupp_of_fintype, mk_toNat_of_infinite, IntermediateField.relrank_dvd_rank_top_of_le, toENat_strictMonoOn, IntermediateField.relrank_dvd_rank_bot, cast_toNat_of_aleph0_le, Submodule.spanRank_toENat_eq_iInf_finset_card, Subfield.relrank_dvd_rank_top_of_le, continuum_toENat, toNat_inj_of_lt_aleph0, mk_finset_of_fintype, not_irreducible_of_aleph0_le, toNat_injOn, MonoidAlgebra.cardinalMk_lift_of_fintype, mk_finsupp_lift_of_fintype, toNat_le_iff_le_of_lt_aleph0, toENat_le_iff_of_le_aleph0, isOrderedRing, toENat_eq_top, toNat_eq_one_iff_unique, Ideal.rank_pow_quot, toNat_lt_toNat, toENat_le_natCast_iff, Set.toENat_cardinalMk, nsmul_lt_aleph0_iff, enat_gc, dvd_of_le_of_aleph0_le, toENat_le_nat, cast_toNat_of_lt_aleph0, toNat_eq_zero, Field.finSepDegree_eq, toENat_comp_ofENat, Field.finInsepDegree_def', toENat_le_iff_of_lt_aleph0, ofENat_toENat_le, toENat_le_one, toENat_injOn, LinearIndepOn.encard_le_toENat_rank, toENat_eq_nat, aleph0_toNat, mk_quaternion, ofENat_toENat_eq_self, toNat_natCast, MonoidAlgebra.cardinalMk_of_fintype, ofENat_toENat, aleph_toENat, sum_pow_eq_max_aleph0, toENat_eq_iff_of_le_aleph0, toNat_apply_of_lt_aleph0, toNat_lift_add_lift, Ideal.height_le_spanRank_toENat, toNat_pos, natCast_eq_toENat_iff, toNat_add, toENat_nat, mk_univ_quaternion, Matroid.toENat_cRank_eq, zero_toNat, LinearMap.rank_finset_sum_le, natCast_le_toENat_iff, aleph_toNat, natCast_toNat_le, Module.length_eq_rank, toENat_lt_top, toENat_congr, toNat_eq_ofNat, one_toNat, continuum_toNat, power_natCast, Matroid.toENat_cRk_eq, HahnSeries.cardSupp_pow_le, toENat_eq_one, mk_quaternionAlgebra
|
instCommMonoid 📖 | CompOp | 1 mathmath: prod_eq_of_fintype
|
instCommMonoidWithZero 📖 | CompOp | 5 mathmath: isPrimePow_iff, Field.nonempty_iff, is_prime_iff, nat_is_prime_iff, prime_of_aleph0_le
|
instConditionallyCompleteLinearOrderBot 📖 | CompOp | 151 mathmath: mk_sUnion_le, Module.rank_def, Algebra.lift_cardinalMk_adjoin_le, SymmetricAlgebra.rank_eq, powerlt_max, lift_iSup_le_lift_iSup, mk_list_eq_max_mk_aleph0, mk_list_le_max, mk_multiset_of_nonempty, iSup_of_empty, iSup_lt_of_isRegular, mul_le_max_of_aleph0_le_right, Filter.cardinalInterFilter_sup, sum_pow_le_max_aleph0, MonoidAlgebra.cardinalMk_of_infinite, mul_eq_max_of_aleph0_le_right, sum_le_mk_mul_iSup, mk_finsupp_lift_of_infinite, Subfield.cardinalMk_closure_le_max, mul_eq_left_iff, lift_iInf, Algebraic.cardinalMk_le_max, Matroid.cRank_eq_iSup_cardinalMk_indep, Algebra.IsAlgebraic.cardinalMk_le_max, Ordinal.card_omega0_opow, lift_iSup, lift_sSup, FreeAlgebra.cardinalMk_le_max, mk_biUnion_le_lift, MonoidAlgebra.cardinalMk_lift_of_infinite, lift_iSup_le, WType.cardinalMk_le_max_aleph0_of_finite', FirstOrder.Language.card_functions_sum_skolem₁_le, Ordinal.sSup_ord, AddMonoidAlgebra.cardinalMk_of_infinite', mul_eq_max, mk_freeMonoid, mk_bounded_set_le, MeasurableSpace.cardinal_generateMeasurableRec_le, WType.cardinalMk_le_max_aleph0_of_finite, mk_list_eq_max, mk_freeAddGroup, Ordinal.card_iSup_Iio_le_card_mul_iSup, mk_finsupp_nat, AddMonoidAlgebra.cardinalMk_lift_of_infinite, mul_ciSup, ciSup_mul, IntermediateField.cardinalMk_adjoin_le, mk_freeAddMonoid, mul_le_max_of_aleph0_le_left, powerlt_min, power_nat_le_max, Algebra.IsAlgebraic.lift_cardinalMk_le_max, preAleph_limit, MonoidAlgebra.cardinalMk_of_infinite', lift_iSup_le_sum, HahnSeries.cardSupp_div_le, sum_le_lift_mk_mul_iSup, mk_freeRing, add_eq_max', Ordinal.card_opow_le_of_omega0_le_right, trdeg_eq_iSup_cardinalMk_isTranscendenceBasis, mul_mk_eq_max, sInf_eq_zero_iff, aleph_max, OreLocalization.cardinalMk_le_max, Ordinal.card_opow_omega0, Ordinal.cof_eq_sInf_lsub, add_eq_max, preAleph_max, iSup_lt_lift_of_isRegular, Polynomial.cardinalMk_eq_max, IsAlgClosed.cardinal_le_max_transcendence_basis', beth_limit, mk_biUnion_le, FirstOrder.Language.Term.card_sigma, mk_bounded_subset_le, sum_le_iSup_lift, Ordinal.iSup_lt_lift, mk_iUnion_le_lift, add_mk_eq_max, AddMonoidAlgebra.cardinalMk_lift_of_infinite', succ_def, Ordinal.iSup_ord, sInf_empty, mk_freeGroup, Ordinal.card_opow_eq_of_omega0_le_right, MeasurableSpace.cardinal_measurableSet_le, MeasurableSpace.cardinal_generateMeasurable_le, sum_le_lift_mk_mul_iSup_lift, IsAlgClosed.cardinal_le_max_transcendence_basis, preBeth_limit, Ordinal.card_opow_le_of_omega0_le_left, FirstOrder.Language.Term.card_le, Ordinal.card_opow_eq_of_omega0_le_left, add_mk_eq_max', ciSup_mul_ciSup, lift_sInf, MvPolynomial.cardinalMk_le_max_lift, max_aleph0_card_le_rank_fun_nat, FreeAlgebra.cardinalMk_le_max_lift, IntermediateField.lift_cardinalMk_adjoin_le, add_ciSup, powerlt_aleph0_le, MonoidAlgebra.cardinalMk_lift_of_infinite', add_eq_left_iff, LinearMap.rank_comp_le, mk_finsupp_of_infinite, mul_eq_max_of_aleph0_le_left, lift_iSup_le_lift_iSup', Polynomial.cardinalMk_le_max, Algebra.cardinalMk_adjoin_le, sum_le_iSup, iInf_eq_zero_iff, lift_iSup_le_iff, sum_pow_eq_max_aleph0, Filter.cardinalInterFilter_inf, aleph_limit, mul_eq_max', IsTranscendenceBasis.lift_cardinalMk_eq_max_lift, IsTranscendenceBasis.lift_rank_eq_max_lift, MvRatFunc.rank_eq_max_lift, MvPolynomial.cardinalMk_le_max, ciSup_add_ciSup, mk_freeCommRing, mk_freeAbelianGroup, HahnSeries.cardSupp_hsum_powers_le, add_le_max, Ordinal.card_opow_le, mk_finsupp_lift_of_infinite', mul_le_max, AddOreLocalization.cardinalMk_le_max, HahnSeries.cardSupp_inv_le, AddMonoidAlgebra.cardinalMk_of_infinite, FreeAlgebra.cardinalMk_eq_max, mk_iUnion_le, iSup_le_sum, add_eq_right_iff, iSup_mk_le_mk_iUnion, ZFSet.iSup_card_le_card_iUnion, mk_finsupp_of_infinite', MvPolynomial.cardinalMk_eq_max_lift, ciSup_add, Ordinal.iSup_lt, FirstOrder.Language.Substructure.lift_card_closure_le, FreeAlgebra.cardinalMk_eq_max_lift, LinearMap.lift_rank_comp_le, MvPolynomial.cardinalMk_eq_max, Algebraic.cardinalMk_lift_le_max, FirstOrder.Language.BoundedFormula.card_le, Algebra.rank_adjoin_le
|
instDistribLattice 📖 | CompOp | 1 mathmath: power_le_max_power_one
|
instLE 📖 | CompOp | 517 mathmath: mk_le_of_module, aleph_le_beth, Ordinal.lift_card_iSup_le_sum_card, mk_le_of_surjective, mk_sUnion_le, ofENat_le_lift, add_le_aleph0, Algebra.lift_cardinalMk_adjoin_le, lift_le_ofENat, natCast_le_rank_iff_finset, Ordinal.cof_iSup_le_lift, Subalgebra.adjoin_rank_le, Ideal.height_le_spanRank, mk_insert_le, le_mk_iff_exists_subset, le_beth_ord, Ordinal.cof_blsub_le, linearIndependent_le_span, rank_le_card_isVisible, lift_mk_le, Algebraic.cardinalMk_lift_le_mul, Ordinal.card_le_ofNat, Ideal.height_le_iff_exists_minimalPrimes, mk_list_le_max, LinearIndependent.cardinal_lift_le_rank, Matrix.lift_cRank_submatrix_le, lift_rank_map_le, aleph_succ, linearIndependent_le_span_finset, Matroid.Indep.cardinalMk_le_cRk_of_subset, LinearMap.rank_le_domain, Ordinal.isInitialIso_apply, mk_preimage_of_subset_range_lift, two_le_iff_one_lt, aleph_pos, mk_embedding_le_arrow, aleph0_le_continuum, le_sum, rank_le_one, ofENat_le_ofNat, Algebra.IsAlgebraic.trdeg_le_cardinalMk, mk_subtype_le_of_subset, Computability.Encoding.card_le_aleph0, HahnSeries.cardSupp_smul_le, Submodule.spanRank_map_le, mk_subtype_mono, ord.orderEmbedding_coe, ofNat_le_lift_iff, linearIndependent_le_span', lift_le_aleph0, Field.insepDegree_le_rank, mk_equiv_le_embedding, AddOreLocalization.cardinalMk_le, isPrimePow_iff, LinearMap.lift_rank_le_of_surjective, lift_eq_aleph_one, aleph0_le_rank_of_isEmpty_oreSet, Ordinal.card_le_aleph, sum_pow_le_max_aleph0, exists_spanRank_le_and_le_height_of_le_height, HahnSeries.cardSupp_single_le, Ordinal.card_iSup_Iio_le_sum_card, ofENat_le_aleph0, le_aleph0_iff_set_countable, card_le_of_finset, LinearMap.le_rank_iff_exists_linearIndependent, sum_le_mk_mul_iSup, rank_map_le, LinearMap.lift_rank_comp_le_right, Module.le_rank_iff_exists_linearMap, Ordinal.isInitialIso_symm_apply_coe, IsStrongLimit.aleph0_le, Order.le_cof, mk_le_one_iff_set_subsingleton, mk_le_aleph0_iff, isNormal_preAleph, bddAbove_ord_image_iff, Subfield.cardinalMk_closure_le_max, mul_eq_left_iff, mul_natCast_le_mul_natCast, FixedPoints.rank_le_card, algebraicIndependent_bounded_of_finset_algebraicIndependent_bounded, Matroid.IsBase.cardinalMk_le_cRank, le_mk_iff_exists_set, preAleph_nat, aleph0_le_beth, Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat, le_range_of_union_finset_eq_top, Ordinal.card_le_card, Algebraic.cardinalMk_le_max, ofENat_le_ofENat_of_le, mk_le_aleph0, mk_subset_ge_of_subset_image_lift, Computability.Encoding.card_le_card_list, zero_le, rank_le_of_injective_injective, Ordinal.card_sInf_range_compl_le_lift, Nat.count_le_cardinal, AddLocalization.cardinalMk_le, Algebra.IsAlgebraic.cardinalMk_le_max, mk_div_le, Ordinal.cof_lsub_le_lift, preAleph_le_aleph, Field.Emb.Cardinal.two_le_deg, Module.Basis.le_span, Submodule.rank_le_spanRank, FirstOrder.Language.Sentence.realize_cardGe, mk_iUnion_le_sum_mk_lift, rank_submodule_le_one_iff, Ordinal.cof_blsub_le_lift, aleph_one_le_continuum, Module.one_le_rank_iff, HahnSeries.cardSupp_truncLT_le, Matrix.cRank_le_card_height, Module.rank_bot_le_rank_of_isScalarTower, Ordinal.card_le_preAleph, aleph_mul_aleph0, le_one_iff_subsingleton, zero_power_le, HahnSeries.cardSupp_one_le, mk_le_iff_forall_finset_subset_card_le, Submodule.spanRank_range_le, lift_trdeg_le_of_injective, rank_range_le, Submodule.rank_le, Ordinal.card_sInf_range_compl_le, mk_union_le_aleph0, HahnSeries.cardSupp_map_le, Submodule.spanRank_span_le_card, card_le_iff, natCast_le_rank_iff, natCast_add_one_le_iff, LinearIndependent.cardinal_le_rank, Matroid.cRk_le_cardinalMk, Ordinal.IsNormal.cof_le, lift_rank_le_of_surjective_injective, FreeAlgebra.cardinalMk_le_max, aleph_add_aleph, Submodule.LinearDisjoint.rank_inf_le_one_of_flat, LinearEquiv.mem_dilatransvections_iff_rank, mk_biUnion_le_lift, Module.rank_top_le_rank_of_isScalarTower, preAleph_omega0, rank_le_of_surjective_injective, Ordinal.nat_le_card, Submodule.le_spanRank_restrictScalars, WType.cardinalMk_le_max_aleph0_of_finite', lift_le_nat_iff, toENat_le_ofNat, lt_omega_iff_card_lt, instCanLiftENatOfENatLeAleph0, le_preAleph_ord, aleph1_le_lift, Module.le_rank_iff, FirstOrder.Language.card_functions_sum_skolem₁_le, Ordinal.card_le_one, Module.lift_rank_bot_le_lift_rank_of_isScalarTower, aleph0_le, infinite_iff, mk_iUnion_le_sum_mk, FirstOrder.Language.Substructure.lift_card_closure_le_card_term, IsRegular.aleph0_le, le_aleph_ord, RCLike.rank_le_two, mk_bounded_set_le, cardinalInterFilter_aleph_one_iff, univLE_iff_cardinal_le, LinearMap.rank_comp_le_left, aleph0_le_mk_iff, Module.le_rank_iff_exists_finset, Matrix.cRank_le_card_width, MeasurableSpace.cardinal_generateMeasurableRec_le, one_le_ofENat, mk_image_le, HahnSeries.cardSupp_neg_le, aleph_le_aleph, WType.cardinalMk_le_max_aleph0_of_finite, Ordinal.cof_le_card, ofNat_le_aleph0, one_le_iff_ne_zero, Algebra.rank_le_of_surjective_injective, lift_rank_add_lift_rank_le_rank_prod, Matroid.IsBasis.cardinalMk_le_cRk, Ordinal.le_cof_iff_blsub, Ordinal.card_le_preBeth, Filter.frequently_cocardinal, beth_le_beth, LinearMap.lift_rank_le_of_injective, Ordinal.card_iSup_Iio_le_card_mul_iSup, rank_submodule_le_one_iff', Algebra.rank_le_of_injective_injective, ord_aleph, LinearMap.rank_le_of_injective, IsClosed.two_pow_mk_le_two_pow_mk_dense, Submodule.rank_mono, mk_image2_le, aleph0_le_of_isSuccLimit, bddAbove_range, lift_le_ofNat_iff, ord_le, lift_trdeg_le_of_surjective, mk_preimage_of_subset_range, Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_right, Set.Subsingleton.cardinalMk_le_one, IntermediateField.cardinalMk_adjoin_le, Matroid.cRank_le_iff, isRegular_aleph_succ, ord_le_ord, rank_le_of_injective_injectiveₛ, Matroid.Indep.cardinalMk_le_isBasis, preBeth_le_beth, le_mk_diff_add_mk, power_nat_le_max, aleph1_lt_lift, AddOreLocalization.cardinalMk_le_lift_cardinalMk_of_addCommute, Algebra.IsAlgebraic.lift_cardinalMk_le_max, preAleph_limit, LinearIndependent.cardinal_le_rank', iSupIndep.subtype_ne_bot_le_rank, isNormal_aleph, Computability.FinEncoding.card_le_aleph0, omega0_le_ord, Ideal.spanRank_map_le, trdeg_add_le, linearIndependent_bounded_of_finset_linearIndependent_bounded, linearIndependent_le_basis, lift_iSup_le_sum, mk_subtype_le, ZFSet.lift_card_iUnion_le_sum_card, ofENat_le_ofENat, rank_le_card, add_one_le_succ, is_prime_iff, le_powerlt, lift_eq_aleph1, rank_span_finset_le, le_rank_iff_exists_linearIndependent, HahnSeries.cardSupp_div_le, sum_le_lift_mk_mul_iSup, HahnSeries.cardSupp_mul_single_le, Ordinal.cof_le_of_isNormal, canonicallyOrderedAdd, ZFSet.lift_card_range_le, mk_range_le, Ordinal.card_opow_le_of_omega0_le_right, add_nat_le_add_nat_iff, Algebra.IsAlgebraic.lift_cardinalMk_le_sigma_polynomial, HahnSeries.cardSupp_single_mul_le, aleph0_le_lift, aleph_max, le_lift_iff, ord_preAleph, OreLocalization.cardinalMk_le_max, OreLocalization.cardinalMk_le_lift_cardinalMk_of_commute, powerlt_le, Ordinal.aleph0_le_card, mk_quot_le, addRightMono, le_mul_left, preAleph_max, preBeth_le_preBeth, mk_abelianization_le, Matroid.cRk_le_iff, Matroid.Indep.cardinalMk_le_cRank, Set.Countable.le_aleph0, MeasurableSpace.cardinal_measurableSet_le_continuum, IsClosed.two_pow_mk_lt_continuum, Algebra.lift_rank_le_of_injective_injective, Algebra.IsAlgebraic.cardinalMk_le_sigma_polynomial, Ordinal.card_le_nat, AlgebraicIndependent.cardinalMk_le_trdeg, rank_span_le, Matroid.Indep.cardinalMk_le_isBasis', preAleph_le_of_isSuccPrelimit, range_aleph, IsAlgClosed.cardinal_le_max_transcendence_basis', Matroid.rankInfinite_iff_aleph0_le_cRank, aleph0_le_preAleph, LinearMap.rank_le_range, preAleph_succ, ofNat_le_ofENat, mk_biUnion_le, aleph0_le_add_iff, aleph_one_le_lift, le_preBeth_ord, mk_bounded_subset_le, collinear_iff_rank_le_one, sum_le_iSup_lift, Ordinal.cof_type_le, mk_le_mk_of_subset, mk_iUnion_le_lift, MeasurableSpace.cardinal_generateMeasurable_le_continuum, lift_le_one_iff, continuum_le_cardinal_of_nontriviallyNormedField, lift_le_aleph1, le_mul_right, mk_set_le, Ordinal.card_le_beth, ZFSet.card_union_le, FirstOrder.Language.Theory.exists_large_model_of_infinite_model, IntermediateField.rank_sup_le_of_isAlgebraic, preAleph_zero, Ordinal.aleph0_le_cof, Ordinal.card_omega, Submodule.rank_add_le_rank_add_rank, toNat_le_iff_le_of_lt_aleph0, Submodule.spanRank_sup_le_sum_spanRank, lift_aleph, rank_quotient_add_rank_le, Ordinal.ofNat_le_card, continuum_le_lift, IntermediateField.adjoin_rank_le_of_isAlgebraic_right, MeasurableSpace.cardinal_measurableSet_le, two_le_iff, MeasurableSpace.cardinal_generateMeasurable_le, Submodule.LinearDisjoint.rank_le_one_of_flat_of_self, aleph0_le_aleph, Ordinal.IsInitial.card_le_card, preAleph_le_preAleph, addLeftMono, ZFSet.card_insert_le, sum_le_lift_mk_mul_iSup_lift, IsAlgClosed.cardinal_le_max_transcendence_basis, Matroid.cRk_inter_add_cRk_union_le, toENat_eq_top, IsLocalization.lift_cardinalMk_le, mk_mul_le, Ordinal.lift_card_sInf_compl_le, bddAbove_iff_small, two_le_iff', aleph0_lt_aleph_one, Subalgebra.rank_sup_le_of_free, rank_quotient_le, Submodule.LinearDisjoint.rank_le_one_of_commute_of_flat_of_self, preAleph_lt_preAleph, Module.rank_le_one_iff_top_isPrincipal, aleph_mul_aleph, IntermediateField.adjoin_rank_le_of_isAlgebraic, Ordinal.card_opow_le_of_omega0_le_left, le_of_dvd, isRegular_aleph_one, ofENat_le_one, LinearIndependent.aleph0_le_rank, Matroid.Spanning.cRank_le_cardinalMk, Algebraic.aleph0_le_cardinalMk_of_charZero, lift_mk_le_lift_mk_of_injective, FirstOrder.Language.Term.card_le, lift_le_sum, lift_le_aleph_one, toENat_le_natCast_iff, cardinalMk_algHom_le_rank, Filter.cocardinal_inf_principal_neBot_iff, Algebraic.cardinalMk_le_mul, HahnSeries.cardSupp_mono, le_aleph0_iff_subtype_countable, aleph0_le_mul_iff', toENatAux_le_nat, toENat_le_nat, LinearMap.rank_le_of_surjective, Ordinal.card_preOmega, lift_mk_le', Order.cof_le, MvPolynomial.cardinalMk_le_max_lift, toNat_eq_zero, HahnSeries.cardSupp_add_le, max_aleph0_card_le_rank_fun_nat, FreeAlgebra.cardinalMk_le_max_lift, Filter.frequently_cocardinal_mem, aleph1_eq_lift, IntermediateField.lift_cardinalMk_adjoin_le, mk_add_le, natCast_mul_le_natCast_mul, preAleph_le_of_strictMono, powerlt_aleph0_le, mk_quotient_le, Submodule.rank_le_one_iff_isPrincipal, preAleph_le_preBeth, mk_bounded_set_le_of_infinite, IntermediateField.rank_sup_le, toENat_le_iff_of_lt_aleph0, preAleph_pos, add_eq_left_iff, LinearMap.rank_comp_le, Matrix.cRank_submatrix_le, ZFSet.card_mono, ofENat_toENat_le, rank_add_rank_le_rank_prod, Ordinal.card_le_card_vonNeumann, bddAbove_of_small, Ordinal.cof_ord_le, toENat_le_one, mk_le_of_injective, Function.Embedding.cardinal_le, Polynomial.cardinalMk_le_max, basis_le_span', aleph_eq_preAleph, nat_le_ofENat, trdeg_le_of_surjective, infinite_basis_le_maximal_linearIndependent', ofENat_toENat_eq_self, Algebra.cardinalMk_adjoin_le, sum_le_iSup, AlgebraicIndependent.lift_cardinalMk_le_trdeg, lift_mk_le_lift_mk_of_surjective, CountableInterFilter.toCardinalInterFilter, Localization.cardinalMk_le, aleph_one_eq_lift, Field.insepDegree_top_le_insepDegree_of_isScalarTower, one_le_lift_iff, aleph_toENat, LinearMap.rank_add_le, countable_iff_lt_aleph_one, IntermediateField.adjoin_rank_le_of_isAlgebraic_left, card_le_of_le_ord, lift_rank_range_le, lift_trdeg_add_le, linearIndependent_le_span'', cardinalMk_algHom, lift_le_continuum, mk_image_le_lift, aleph_limit, lift_rank_le_of_injective_injective, Ordinal.cof_lsub_le, Ordinal.cof_bsup_le_lift, nat_le_lift_iff, continuum_le_cardinal_of_module, le_rank_iff_exists_linearIndependent_finset, aleph0_mul_aleph, mk_union_le, lift_lt_aleph1, lift_rank_le_of_injective_injectiveₛ, rank_le_of_isSMulRegular, ofENat_le_nat, MvPolynomial.cardinalMk_le_max, rank_le_one_iff, one_le_iff_pos, Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_left, HahnSeries.cardSupp_sub_le, infinite_basis_le_maximal_linearIndependent, ord_le_omega0, aleph_one_lt_lift, Ordinal.le_cof_iff_lsub, HahnSeries.cardSupp_hsum_powers_le, add_le_max, mk_preimage_of_injective_lift, linearIndependent_le_infinite_basis, Matroid.Indep.cardinalMk_le_isBase, Matroid.cRk_le_of_subset, Field.sepDegree_le_rank, Ordinal.card_opow_le, OreLocalization.cardinalMk_le, IsLocalization.cardinalMk_le, mk_preimage_of_injective, Ordinal.cof_bsup_le, mem_range_aleph_iff, ZFSet.card_image_le, aleph_lt_aleph, Algebra.lift_rank_le_of_surjective_injective, rank_le, mul_le_max, Matroid.IsBasis'.cardinalMk_le_cRk, AddOreLocalization.cardinalMk_le_max, HahnSeries.cardSupp_inv_le, Submodule.FG.spanRank_le_iff_exists_span_set_card_le, card_le_of_injective'', Field.insepDegree_le_of_left_le, aleph0_le_mul_iff, LinearMap.le_rank_iff_exists_linearIndependent_finset, card_le_of, LinearMap.rank_finset_sum_le, add_one_le_add_one_iff, natCast_le_toENat_iff, out_embedding, Submodule.LinearDisjoint.rank_inf_le_one_of_flat_right, mk_subset_ge_of_subset_image, continuum_le_cardinal_of_isOpen, Ordinal.cof_iSup_le, aleph_toNat, natCast_toNat_le, HahnSeries.cardSupp_hsum_le, add_le_add_iff_of_lt_aleph0, mk_iUnion_le, Submodule.LinearDisjoint.rank_inf_le_one_of_flat_left, Ordinal.one_le_card, iSup_le_sum, add_eq_right_iff, Matrix.rank_vecMulVec, iSup_mk_le_mk_iUnion, Ordinal.le_cof_type, succ_aleph0, le_def, ZFSet.iSup_card_le_card_iUnion, Ordinal.card_iSup_le_sum_card, isOpen_setOf_nat_le_rank, aleph0_le_mk, mk_range_le_lift, one_le_aleph0, FirstOrder.Language.Substructure.lift_card_closure_le, LinearMap.rank_comp_le_right, FirstOrder.Language.card_le_of_model_distinctConstantsTheory, aleph_zero, mk_sub_le, HahnSeries.cardSupp_pow_le, lift_preAleph, lift_lt_aleph_one, LinearMap.lift_rank_comp_le, natCast_le_aleph0, HahnSeries.cardSupp_mul_le, iSupIndep.subtype_ne_bot_le_finrank_aux, LinearIndependent.cardinalMk_le_finrank, lift_le, Algebraic.cardinalMk_lift_le_max, FirstOrder.Language.BoundedFormula.card_le, Algebra.rank_adjoin_le, trdeg_le_of_injective, isRegular_preAleph_succ, FirstOrder.Language.empty.nonempty_embedding_iff
|
instSuccOrder 📖 | CompOp | 24 mathmath: lt_ord_succ_card, Ordinal.sInf_compl_lt_lift_ord_succ, aleph_succ, OrdinalApprox.gfpApprox_ord_mem_fixedPoint, succ_eq_of_lt_aleph0, succ_natCast, lift_succ, card_le_iff, OrdinalApprox.lfpApprox_ord_eq_lfp, OrdinalApprox.lfpApprox_ord_mem_fixedPoint, isRegular_succ, add_one_le_succ, OrdinalApprox.gfpApprox_ord_eq_gfp, preAleph_succ, OrdinalApprox.exists_gfpApprox_eq_gfpApprox, nat_succ, not_injective_limitation_set, succ_def, OrdinalApprox.exists_lfpApprox_eq_lfpApprox, powerlt_succ, Ordinal.sInf_compl_lt_ord_succ, succ_zero, succ_pos, succ_aleph0
|
instWellFoundedRelation 📖 | CompOp | — |
liftInitialSeg 📖 | CompOp | 1 mathmath: liftInitialSeg_toFun
|
linearOrder 📖 | CompOp | 8 mathmath: isNormal_preAleph, isNormal_aleph, type_cardinal, isNormal_beth, isNormal_preBeth, isNormal_ord, lift_min, lift_max
|
orderBot 📖 | CompOp | — |
partialOrder 📖 | CompOp | 264 mathmath: lt_ord_succ_card, natCast_lt_toENat_iff, Module.rank_lt_aleph0_iff, HahnSeries.mem_cardSuppLTSubfield, Ordinal.sInf_compl_lt_lift_ord_succ, Set.toENat_cardinalMk_subtype, toENat_eq_natCast_iff, ofENat_lt_lift, ofENat_lt_ofNat, IsNoetherian.iff_rank_lt_aleph0, aleph_succ, two_le_iff_one_lt, aleph_pos, HahnSeries.coe_cardSuppLTAddSubmonoid, toENat_ofENat, Module.length_of_free, range_ofENat, OrdinalApprox.gfpApprox_ord_mem_fixedPoint, one_lt_aleph0, Matroid.isRkFinite_iff_cRk_lt_aleph0, mk_monotone, succ_natCast, Submodule.spanRank_toENat_eq_iInf_encard, ofNat_lt_lift_iff, toENat_eq_zero, toENat_eq_ofNat, lift_lt_ofNat_iff, lift_succ, ofENat_mono, trdeg_lt_aleph0, Module.one_lt_rank_of_one_lt_finrank, Module.rank_pos_iff_of_free, nsmul_lt_aleph0_iff_of_ne_zero, lt_power_cof, liftInitialSeg_toFun, Filter.mem_cardinaleGenerate_iff, lift_monotone, ofENat_lt_aleph0, isInaccessible_def, rank_lt_rank_dual', toENat_lt_natCast_iff, card_le_iff, small_Iio, nat_lt_aleph0, natCast_add_one_le_iff, mk_strictMonoOn, Filter.mem_cocardinal, mul_natCast_strictMono, cast_toNat_eq_iff_lt_aleph0, nat_lt_continuum, HahnSeries.mem_cardSuppLTSubring, toENat_lift, continuum_lt_lift, toNat_monotoneOn, Matroid.cRk_mono, instNoMaxOrder, toENat_le_ofNat, lt_omega_iff_card_lt, strongRankCondition_iff_forall_rank_lt_aleph0, lift_lt_ofENat, lt_univ, add_lt_aleph0_iff, mk_embedding_eq_zero_iff_lift_lt, Ordinal.IsInitial.card_lt_card, lt_one_iff_zero, IsInaccessible.nat_lt, Ordinal.nat_lt_card, Submodule.spanRank_finite_iff_fg, lift_rank_lt_rank_dual', Ideal.height_le_spanRank_toENat_of_mem_minimal_primes, small_Icc, IsStrongLimit.isSuccLimit, HahnSeries.mem_cardSuppLTAddSubgroup, rank_pos_iff_nontrivial, lift_lt_univ', univ_pos, IsInaccessible.aleph0_lt, Module.rank_pos_of_free, OrdinalApprox.lfpApprox_ord_eq_lfp, Ordinal.card_lt_nat, Module.lt_rank_of_lt_finrank, HahnSeries.coe_cardSuppLTAddSubgroup, Ordinal.one_lt_card, ofENat_lt_ofENat_of_lt, OrdinalApprox.lfpApprox_ord_mem_fixedPoint, continuum_pos, beth_mono, ofNat_lt_aleph0, powerlt_mono_left, aleph0_lt_mk_iff, aleph1_lt_lift, toNat_strictMonoOn, isRegular_succ, card_lt_card_of_left_finite, card_typein_lt, add_one_le_succ, ofNat_lt_ofENat, card_typein_toType_lt, small_Ioo, natCast_lt_aleph0, IsInaccessible.pos, OrdinalApprox.gfpApprox_ord_eq_gfp, lift_lt, lt_wf, aleph0_lt_mk, preBeth_lt_preBeth, instWellFoundedLT, ord_lt_omega0, lift_rank_lt_rank_dual, toENatAux_gc, toNat_toENat, IsStrongLimit.isSuccPrelimit, isSuccLimit_aleph0, mk_strictMono, small_Ioc, beth_pos, type_cardinal, toENat_rank_span_set, nat_lt_lift_iff, toENat_strictMonoOn, not_isSuccLimit_natCast, range_aleph, cantor, lift_lt_univ, preAleph_succ, lt_aleph0_iff_subtype_finite, lt_lift_iff, Submodule.spanRank_toENat_eq_iInf_finset_card, trdeg_pos, Filter.hasBasis_cocardinal, OrdinalApprox.exists_gfpApprox_eq_gfpApprox, aleph0_lt_univ, nat_succ, not_injective_limitation_set, continuum_toENat, Field.Emb.Cardinal.deg_lt_aleph0, natCast_mul_strictMono, Ordinal.ofNat_lt_card, gc_ord_card, toNat_injOn, succ_def, mul_lt_aleph0_iff, lt_aleph0_iff_finite, Filter.eventually_cocardinal, ofENat_lt_ofENat, isSuccLimit_iff, Matroid.rankFinite_iff_cRank_lt_aleph0, cardinal_lt_aleph0_of_finiteDimensional, small_iff_lift_mk_lt_univ, ofENat_strictMono, HahnSeries.mem_cardSuppLTAddSubmonoid, toENat_le_iff_of_le_aleph0, Ordinal.zero_lt_card, isOrderedRing, one_lt_two, toENat_eq_top, small_Iic, mk_surjective_eq_zero_iff, one_lt_iff_nontrivial, aleph0_lt_aleph_one, one_lt_ofENat, LinearIndependent.lt_aleph0_of_finiteDimensional, preAleph_lt_preAleph, rank_span_of_finset, ofENat_lt_nat, beth_strictMono, one_lt_lift_iff, ofENat_pos, toENat_le_natCast_iff, Set.toENat_cardinalMk, nsmul_lt_aleph0_iff, enat_gc, LinearIndependent.lt_aleph0_of_finite, toENat_le_nat, OrdinalApprox.exists_lfpApprox_eq_lfpApprox, powerlt_succ, rank_pos_iff_exists_ne_zero, isSuccPrelimit_aleph0, canLiftCardinalNat, aleph0_lt_lift, lift_lt_aleph0, lt_aleph0_of_finite, Ordinal.sInf_compl_lt_ord_succ, ord_strictMono, toENat_comp_ofENat, ord_lt_ord, preAleph_pos, beth_lt_beth, Set.Finite.lt_aleph0, small_Ico, aleph0_pos, isSuccPrelimit_zero, ofENat_toENat_le, omega0_lt_ord, IsClosed.mk_lt_continuum, succ_zero, toENat_le_one, lt_aleph0, range_natCast, toENat_injOn, LinearIndepOn.encard_le_toENat_rank, toENat_eq_nat, rank_pos, mul_natCast_lt_mul_natCast, ofENat_toENat_eq_self, preBeth_strictMono, ofENat_toENat, mk_surjective_eq_zero_iff_lift, aleph_toENat, preBeth_mono, lift_lt_continuum, countable_iff_lt_aleph_one, hasCardinalLT_iff_cardinal_mk_lt, Ordinal.card_lt_aleph0, IsRegular.nat_lt, toENat_eq_iff_of_le_aleph0, mk_lt_aleph0, mk_lt_aleph0_iff, Ordinal.card_lt_ofNat, IsClosed.mk_lt_two_pow_mk_dense, lift_lt_aleph1, Ideal.height_le_spanRank_toENat, toNat_pos, rank_lt_rank_dual, lift_strictMono, natCast_eq_toENat_iff, one_le_iff_pos, aleph_one_lt_lift, toENat_nat, IsRegular.pos, isInaccesible_def, toNat_ne_zero, Matroid.toENat_cRank_eq, preBeth_pos, lt_univ', mul_lt_aleph0_iff_of_ne_zero, Module.rank_lt_aleph0, mk_embedding_eq_zero_iff_lt, ord_mono, aleph_lt_aleph, zero_lt_lift_iff, nat_lt_univ, toENat_ne_top, aleph0_lt_continuum, succ_pos, card_lt_card_of_right_finite, natCast_le_toENat_iff, lt_ord, lt_aleph0_iff_set_finite, finset_card_lt_aleph0, Module.length_eq_rank, toENat_lt_top, succ_aleph0, lt_aleph0_iff_fintype, lift_lt_nat_iff, toENat_congr, Matroid.toENat_cRk_eq, lift_lt_aleph_one, toENat_eq_one, mk_Iio_ord_toType, Filter.mem_cardinalGenerate_iff, not_isSuccLimit_zero, natCast_mul_lt_natCast_mul, nat_lt_ofENat
|