| Metric | Count |
|---|
DefinitionsofLeftInverse, subsemigroupCongr, subsemigroupMap, codRestrict, restrict, srange, srangeRestrict, subsemigroupComap, subsemigroupMap, comap, equivMapOfInjective, gciMapComap, giMapComap, inclusion, map, prod, prodEquiv, toSubsemigroup, toSubsemigroup', topEquiv, ofLeftInverse, subsemigroupCongr, subsemigroupMap, codRestrict, restrict, srange, srangeRestrict, subsemigroupComap, subsemigroupMap, comap, equivMapOfInjective, gciMapComap, giMapComap, inclusion, map, prod, prodEquiv, toAddSubsemigroup, toAddSubsemigroup', topEquiv | 40 |
TheoremsofLeftInverse_apply, ofLeftInverse_symm_apply, subsemigroupMap_apply_coe, subsemigroupMap_symm_apply_coe, codRestrict_apply_coe, coe_srange, coe_srangeRestrict, map_mclosure, map_srange, mclosure_preimage_le, mem_srange, prod_map_comap_prod', restrict_apply, srangeRestrict_surjective, srange_eq_map, srange_eq_top_iff_surjective, srange_eq_top_of_surjective, srange_mk, subsemigroupComap_apply_coe, subsemigroupMap_apply_coe, subsemigroupMap_surjective, apply_coe_mem_map, bot_prod_bot, closure_closure_coe_preimage, coe_comap, coe_equivMapOfInjective_apply, coe_map, coe_prod, coe_toSubsemigroup_apply, coe_toSubsemigroup_symm_apply, comap_comap, comap_equiv_eq_map_symm, comap_iInf, comap_iInf_map_of_injective, comap_iSup_map_of_injective, comap_id, comap_inf, comap_inf_map_of_injective, comap_injective_of_surjective, comap_le_comap_iff_of_surjective, comap_map_comap, comap_map_eq_of_injective, comap_strictMono_of_surjective, comap_sup_map_of_injective, comap_surjective_of_injective, comap_top, eq_top_iff', gc_map_comap, le_comap_map, le_comap_of_map_le, le_prod_iff, map_bot, map_comap_eq, map_comap_eq_of_surjective, map_comap_eq_self, map_comap_le, map_comap_map, map_equiv_eq_comap_symm, map_equiv_top, map_iInf, map_iInf_comap_of_surjective, map_iSup, map_iSup_comap_of_surjective, map_id, map_inf, map_inf_comap_of_surjective, map_injective_of_injective, map_le_iff_le_comap, map_le_map_iff_of_injective, map_le_of_le_comap, map_map, map_strictMono_of_injective, map_sup, map_sup_comap_of_surjective, map_surjective_of_surjective, mem_comap, mem_map, mem_map_equiv, mem_map_iff_mem, mem_map_of_mem, mem_prod, monotone_comap, monotone_map, prod_eq_top_iff, prod_mono, prod_top, range_subtype, srange_fst, srange_snd, toSubsemigroup'_closure, toSubsemigroup_closure, topEquiv_apply, topEquiv_symm_apply_coe, topEquiv_toAddHom, top_prod, top_prod_top, ofLeftInverse_apply, ofLeftInverse_symm_apply, subsemigroupMap_apply_coe, subsemigroupMap_symm_apply_coe, codRestrict_apply_coe, coe_srange, coe_srangeRestrict, map_mclosure, map_srange, mclosure_preimage_le, mem_srange, prod_map_comap_prod', restrict_apply, srangeRestrict_surjective, srange_eq_map, srange_eq_top_iff_surjective, srange_eq_top_of_surjective, srange_mk, subsemigroupComap_apply_coe, subsemigroupMap_apply_coe, subsemigroupMap_surjective, apply_coe_mem_map, bot_prod_bot, closure_closure_coe_preimage, coe_comap, coe_equivMapOfInjective_apply, coe_map, coe_prod, coe_toAddSubsemigroup_apply, coe_toAddSubsemigroup_symm_apply, comap_comap, comap_equiv_eq_map_symm, comap_iInf, comap_iInf_map_of_injective, comap_iSup_map_of_injective, comap_id, comap_inf, comap_inf_map_of_injective, comap_injective_of_surjective, comap_le_comap_iff_of_surjective, comap_map_comap, comap_map_eq_of_injective, comap_strictMono_of_surjective, comap_sup_map_of_injective, comap_surjective_of_injective, comap_top, eq_top_iff', gc_map_comap, le_comap_map, le_comap_of_map_le, le_prod_iff, map_bot, map_comap_eq, map_comap_eq_of_surjective, map_comap_eq_self, map_comap_le, map_comap_map, map_equiv_eq_comap_symm, map_equiv_top, map_iInf, map_iInf_comap_of_surjective, map_iSup, map_iSup_comap_of_surjective, map_id, map_inf, map_inf_comap_of_surjective, map_injective_of_injective, map_le_iff_le_comap, map_le_map_iff_of_injective, map_le_of_le_comap, map_map, map_strictMono_of_injective, map_sup, map_sup_comap_of_surjective, map_surjective_of_surjective, mem_comap, mem_map, mem_map_equiv, mem_map_iff_mem, mem_map_of_mem, mem_prod, monotone_comap, monotone_map, prod_eq_top_iff, prod_mono, prod_top, range_subtype, srange_fst, srange_snd, toAddSubsemigroup'_closure, toAddSubsemigroup_closure, topEquiv_apply, topEquiv_symm_apply_coe, topEquiv_toMulHom, top_prod, top_prod_top | 192 |
| Total | 232 |