| Metric | Count |
|---|
DefinitionsbfamilyOfFamily, bfamilyOfFamily', blsub, brange, bsup, familyOfBFamily, familyOfBFamily', lsub | 8 |
Theoremsapply_of_isSuccLimit, apply_omega0, blsub_eq, bsup, bsup_eq, eq_iff_zero_and_succ, map_iSup, map_iSup_of_bddAbove, map_sSup, map_sSup_of_bddAbove, apply_omega0_of_isNormal, bddAbove_iff_small, bddAbove_image, bddAbove_of_small, bddAbove_range, bddAbove_range_comp, bfamilyOfFamily'_typein, bfamilyOfFamily_typein, blsub_comp, blsub_congr, blsub_const, blsub_eq_blsub, blsub_eq_lsub, blsub_eq_lsub', blsub_eq_of_brange_eq, blsub_eq_zero_iff, blsub_id, blsub_le, blsub_le_bsup_succ, blsub_le_iff, blsub_le_of_brange_subset, blsub_one, blsub_pos, blsub_succ_of_mono, blsub_type, blsub_zero, brange_bfamilyOfFamily, brange_bfamilyOfFamily', brange_const, bsup'_eq_iSup, bsup_comp, bsup_congr, bsup_const, bsup_eq_blsub, bsup_eq_blsub_iff_lt_bsup, bsup_eq_blsub_iff_succ, bsup_eq_blsub_of_lt_succ_limit, bsup_eq_blsub_or_succ_bsup_eq_blsub, bsup_eq_bsup, bsup_eq_iSup, bsup_eq_of_brange_eq, bsup_eq_sup, bsup_eq_sup', bsup_eq_zero_iff, bsup_id_limit, bsup_id_succ, bsup_le, bsup_le_blsub, bsup_le_iff, bsup_le_of_brange_subset, bsup_not_succ_of_ne_bsup, bsup_one, bsup_succ_eq_blsub, bsup_succ_le_blsub, bsup_succ_of_mono, bsup_zero, card_sInf_range_compl_le, card_sInf_range_compl_le_lift, comp_bfamilyOfFamily, comp_bfamilyOfFamily', comp_familyOfBFamily, comp_familyOfBFamily', familyOfBFamily'_enum, familyOfBFamily_enum, iSup'_eq_bsup, iSup_Iio_eq_bsup, iSup_add_nat, iSup_add_natCast, iSup_eq_bsup, iSup_eq_iSup, iSup_eq_lsub, iSup_eq_lsub_iff, iSup_eq_lsub_iff_lt_iSup, iSup_eq_lsub_or_succ_iSup_eq_lsub, iSup_eq_of_range_eq, iSup_eq_zero_iff, iSup_le, iSup_le_iff, iSup_le_lsub, iSup_mul_nat, iSup_mul_natCast, iSup_natCast, iSup_ord, iSup_succ, iSup_sum, iSup_typein_limit, iSup_typein_succ, isNormal_iff_lt_succ_and_blsub_eq, isNormal_iff_lt_succ_and_bsup_eq, le_bsup, le_iSup, lift_card_sInf_compl_le, lsub_const, lsub_empty, lsub_eq_blsub, lsub_eq_blsub', lsub_eq_lsub, lsub_eq_of_range_eq, lsub_eq_zero_iff, lsub_le, lsub_le_iff, lsub_le_of_range_subset, lsub_le_succ_iSup, lsub_le_sup_succ, lsub_notMem_range, lsub_pos, lsub_sum, lsub_typein, lsub_unique, lt_blsub, lt_blsub_iff, lt_bsup, lt_bsup_of_limit, lt_bsup_of_ne_bsup, lt_iSup_iff, lt_lsub, lt_lsub_iff, mem_brange, mem_brange_self, nonempty_compl_range, not_bddAbove_compl_of_small, range_familyOfBFamily, range_familyOfBFamily', sInf_compl_lt_lift_ord_succ, sInf_compl_lt_ord_succ, sSup_eq_bsup, sSup_ord, succ_iSup_eq_lsub_iff, succ_iSup_le_lsub_iff, succ_lt_iSup_of_ne_iSup, sup_eq_bsup, sup_eq_bsup', sup_eq_lsub, sup_eq_lsub_iff_lt_sup, sup_eq_lsub_iff_succ, sup_eq_lsub_or_sup_succ_eq_lsub, sup_eq_sup, sup_le_lsub, sup_succ_eq_lsub, sup_succ_le_lsub, sup_typein_limit, sup_typein_succ, unbounded_range_of_le_iSup, uncountable, not_injective_of_ordinal, not_injective_of_ordinal_of_small, not_small_ordinal, not_surjective_of_ordinal, not_surjective_of_ordinal_of_small | 159 |
| Total | 167 |
| Name | Category | Theorems |
|---|
bfamilyOfFamily 📖 | CompOp | 6 mathmath: comp_bfamilyOfFamily, bsup_eq_sup, bfamilyOfFamily_typein, brange_bfamilyOfFamily, bsup_eq_iSup, blsub_eq_lsub
|
bfamilyOfFamily' 📖 | CompOp | 8 mathmath: blsub_eq_blsub, comp_bfamilyOfFamily', brange_bfamilyOfFamily', bfamilyOfFamily'_typein, bsup'_eq_iSup, bsup_eq_sup', blsub_eq_lsub', bsup_eq_bsup
|
blsub 📖 | CompOp | 39 mathmath: cof_blsub_le, Cardinal.blsub_lt_ord_lift_of_isRegular, blsub_congr, blsub_le_iff, blsub_eq_blsub, IsFundamentalSequence.blsub_eq, blsub_id, cof_blsub_le_lift, blsub_eq_of_brange_eq, bsup_succ_eq_blsub, blsub_lt_ord_lift, lsub_eq_blsub', bsup_eq_blsub_iff_succ, blsub_le_of_brange_subset, lt_blsub_iff, bsup_eq_blsub_of_lt_succ_limit, blsub_lt_ord, blsub_type, lt_blsub, Cardinal.blsub_lt_ord_of_isRegular, isNormal_iff_lt_succ_and_blsub_eq, blsub_le, bsup_eq_blsub_or_succ_bsup_eq_blsub, blsub_pos, bsup_eq_blsub_iff_lt_bsup, bsup_succ_le_blsub, blsub_succ_of_mono, bsup_eq_blsub, blsub_const, blsub_one, bsup_le_blsub, blsub_eq_lsub, IsNormal.blsub_eq, blsub_eq_lsub', blsub_eq_zero_iff, blsub_zero, lsub_eq_blsub, exists_blsub_cof, blsub_le_bsup_succ
|
brange 📖 | CompOp | 8 mathmath: brange_bfamilyOfFamily', sSup_eq_bsup, brange_const, range_familyOfBFamily', range_familyOfBFamily, brange_bfamilyOfFamily, mem_brange, mem_brange_self
|
bsup 📖 | CompOp | 48 mathmath: iSup_eq_bsup, bsup_id_succ, bsup_const, Cardinal.bsup_lt_ord_of_isRegular, mem_closure_iff_bsup, isClosed_iff_bsup, sSup_eq_bsup, bsup_le, bsup_succ_eq_blsub, isNormal_iff_lt_succ_and_bsup_eq, bsup_eq_blsub_iff_succ, bsup_one, bsup_zero, mem_closed_iff_bsup, sup_eq_bsup, bsup_eq_blsub_of_lt_succ_limit, bsup_eq_of_brange_eq, bsup_eq_sup, lt_bsup_of_limit, bsup_le_of_brange_subset, bsup_lt_ord_lift, mem_closure_tfae, bsup_eq_blsub_or_succ_bsup_eq_blsub, iSup'_eq_bsup, Cardinal.bsup_lt_ord_lift_of_isRegular, IsNormal.bsup, bsup_id_limit, bsup_succ_of_mono, bsup_congr, bsup_eq_blsub_iff_lt_bsup, le_bsup, sup_eq_bsup', bsup_succ_le_blsub, lt_bsup_of_ne_bsup, bsup_le_iff, bsup'_eq_iSup, iSup_Iio_eq_bsup, bsup_eq_iSup, bsup_eq_blsub, bsup_lt_ord, bsup_eq_sup', bsup_comp, bsup_eq_zero_iff, bsup_le_blsub, IsNormal.bsup_eq, lt_bsup, bsup_eq_bsup, blsub_le_bsup_succ
|
familyOfBFamily 📖 | CompOp | 6 mathmath: iSup_eq_bsup, sup_eq_bsup, comp_familyOfBFamily, range_familyOfBFamily, lsub_eq_blsub, familyOfBFamily_enum
|
familyOfBFamily' 📖 | CompOp | 9 mathmath: iSup_eq_iSup, lsub_eq_blsub', comp_familyOfBFamily', lsub_eq_lsub, iSup'_eq_bsup, range_familyOfBFamily', sup_eq_sup, sup_eq_bsup', familyOfBFamily'_enum
|
lsub 📖 | CompOp | 46 mathmath: sup_eq_lsub_iff_lt_sup, lsub_pos, sup_eq_lsub_iff_succ, sup_succ_le_lsub, iSup_le_lsub, cof_lsub_le_lift, lsub_const, Cardinal.lsub_lt_ord_of_isRegular, iSup_eq_lsub_or_succ_iSup_eq_lsub, sup_succ_eq_lsub, Cardinal.lsub_lt_ord_lift_of_isRegular, lsub_eq_blsub', sup_le_lsub, lsub_lt_ord, blsub_type, cof_lsub_def_nonempty, lsub_eq_lsub, exists_lsub_cof, cof_eq_sInf_lsub, lsub_le_of_range_subset, lsub_eq_of_range_eq, SetTheory.PGame.birthday_def, lsub_le_iff, succ_iSup_eq_lsub_iff, sup_eq_lsub, iSup_eq_lsub_iff_lt_iSup, lsub_typein, lsub_le_succ_iSup, lt_lsub, lsub_notMem_range, blsub_eq_lsub, sup_eq_lsub_or_sup_succ_eq_lsub, blsub_eq_lsub', lsub_le, cof_lsub_le, iSup_eq_lsub, iSup_eq_lsub_iff, lsub_empty, lsub_eq_blsub, lsub_eq_zero_iff, lsub_unique, lsub_le_sup_succ, succ_iSup_le_lsub_iff, lsub_sum, lsub_lt_ord_lift, lt_lsub_iff
|