| Metric | Count |
|---|
Definitionspowerlt, «term_^<_» | 2 |
Theoremsaleph0_le, add_le_aleph0, add_lt_aleph0, add_lt_aleph0_iff, aleph0_add_aleph0, aleph0_add_nat, aleph0_add_ofNat, aleph0_le, aleph0_le_add_iff, aleph0_le_mk, aleph0_le_mk_iff, aleph0_le_mul_iff, aleph0_le_mul_iff', aleph0_le_of_isSuccLimit, aleph0_lt_mk, aleph0_lt_mk_iff, aleph0_mul_aleph0, aleph0_mul_nat, aleph0_mul_ofNat, bddAbove_iff_small, bddAbove_image, bddAbove_of_small, bddAbove_range, bddAbove_range_comp, canLiftCardinalNat, cantor', card_le_of, card_lt_card_of_left_finite, card_lt_card_of_right_finite, compl_nonempty_of_mk_lt_mk, denumerable_iff, diff_nonempty_of_mk_lt_mk, eq_one_iff_unique, exists_eq_natCast_of_iSup_eq, exists_finset_eq_card, exists_finset_le_card, exists_nat_eq_of_le_nat, exists_notMem_of_length_lt, finset_card_lt_aleph0, iInf_eq_zero_iff, iSup_mk_le_mk_iUnion, iSup_of_empty, infinite_iff, isStrongLimit_aleph0, isSuccLimit_aleph0, isSuccPrelimit_aleph0, le_aleph0_iff_set_countable, le_aleph0_iff_subtype_countable, le_mk_diff_add_mk, le_mk_iff_exists_subset, le_one_iff_subsingleton, le_powerlt, lift_iInf, lift_iSup, lift_iSup_le, lift_iSup_le_iff, lift_iSup_le_lift_iSup, lift_iSup_le_lift_iSup', lift_iSup_le_sum, lift_mk_le_lift_mk_of_injective, lift_mk_le_lift_mk_of_surjective, lift_mk_shrink, lift_mk_shrink', lift_mk_shrink'', lift_sInf, lift_sSup, lt_aleph0, lt_aleph0_iff_finite, lt_aleph0_iff_fintype, lt_aleph0_iff_set_finite, lt_aleph0_iff_subtype_finite, lt_aleph0_of_finite, lt_one_iff_zero, mk_addOpposite, mk_additive, mk_biUnion_le, mk_biUnion_le_lift, mk_denumerable, mk_diff_add_mk, mk_emptyCollection, mk_emptyCollection_iff, mk_eq_aleph0, mk_eq_nat_iff, mk_eq_nat_iff_finset, mk_eq_nat_iff_fintype, mk_eq_two_iff, mk_eq_two_iff', mk_finset_of_fintype, mk_iUnion_eq_sum_mk, mk_iUnion_eq_sum_mk_lift, mk_iUnion_le, mk_iUnion_le_lift, mk_iUnion_le_sum_mk, mk_iUnion_le_sum_mk_lift, mk_image2_le, mk_image_embedding, mk_image_embedding_lift, mk_image_eq, mk_image_eq_lift, mk_image_eq_of_injOn, mk_image_eq_of_injOn_lift, mk_image_le, mk_image_le_lift, mk_insert, mk_insert_le, mk_int, mk_le_aleph0, mk_le_aleph0_iff, mk_le_iff_forall_finset_subset_card_le, mk_le_mk_of_subset, mk_le_one_iff_set_subsingleton, mk_list_eq_sum_pow, mk_lt_aleph0, mk_lt_aleph0_iff, mk_monotone, mk_mulOpposite, mk_multiplicative, mk_pnat, mk_preimage_down, mk_preimage_equiv, mk_preimage_equiv_lift, mk_preimage_of_injective, mk_preimage_of_injective_lift, mk_preimage_of_injective_of_subset_range, mk_preimage_of_injective_of_subset_range_lift, mk_preimage_of_subset_range, mk_preimage_of_subset_range_lift, mk_quot_le, mk_quotient_le, mk_range_eq, mk_range_eq_lift, mk_range_eq_of_injective, mk_range_inl, mk_range_inr, mk_range_le, mk_range_le_lift, mk_sUnion_le, mk_sep, mk_setProd, mk_set_eq_nat_iff_finset, mk_set_eq_one_iff, mk_set_eq_zero_iff, mk_set_ne_zero_iff, mk_singleton, mk_strictMono, mk_strictMonoOn, mk_subset_ge_of_subset_image, mk_subset_ge_of_subset_image_lift, mk_subtype_le_of_subset, mk_subtype_mono, mk_sum_compl, mk_union_add_mk_inter, mk_union_le, mk_union_le_aleph0, mk_union_of_disjoint, mk_univ, mk_vector, mul_lt_aleph0, mul_lt_aleph0_iff, mul_lt_aleph0_iff_of_ne_zero, natCast_add_one_le_iff, natCast_le_aleph0, natCast_lt_aleph0, nat_add_aleph0, nat_lt_aleph0, nat_mul_aleph0, nat_succ, not_isSuccLimit_natCast, not_isSuccLimit_of_lt_aleph0, nsmul_lt_aleph0_iff, nsmul_lt_aleph0_iff_of_ne_zero, ofNat_add_aleph0, ofNat_le_aleph0, ofNat_lt_aleph0, ofNat_mul_aleph0, one_le_aleph0, one_le_iff_ne_zero, one_le_iff_pos, one_lt_aleph0, one_lt_iff_nontrivial, one_lt_two, power_lt_aleph0, powerlt_le, powerlt_le_powerlt_left, powerlt_max, powerlt_min, powerlt_mono_left, powerlt_succ, powerlt_zero, prod_eq_of_fintype, range_natCast, sInf_eq_zero_iff, small_Icc, small_Ico, small_Iic, small_Iio, small_Ioc, small_Ioo, succ_eq_of_lt_aleph0, succ_natCast, succ_zero, sum_le_iSup, sum_le_iSup_lift, sum_le_lift_mk_mul_iSup, sum_le_lift_mk_mul_iSup_lift, sum_le_mk_mul_iSup, sum_zero_pow, three_le, two_le_iff, two_le_iff', two_le_iff_one_lt, uncountable, zero_powerlt, le_aleph0, lt_aleph0, cardinalMk_le_one, countable_infinite_iff_nonempty_denumerable, not_small_cardinal | 218 |
| Total | 220 |