| Metric | Count |
|---|
DefinitionsinstAlternative, kernMap, monad, Map, Map | 5 |
Theoremscomap, comap_of_image_mem, comap_of_range_mem, comap_of_surj, map, of_map, biSup_pure_eq_principal, bind_def, bind_inf_principal, bind_le, bind_map, bind_mono, canLift, comap_bot, comap_coe_neBot_of_le_principal, comap_comap, comap_comm, comap_const_of_mem, comap_const_of_notMem, comap_eq_bot_iff_compl_range, comap_equiv_symm, comap_eval_neBot, comap_eval_neBot_iff, comap_eval_neBot_iff', comap_fst_neBot, comap_fst_neBot_iff, comap_iInf, comap_iSup, comap_id, comap_id', comap_inf, comap_inf_principal_neBot_of_image_mem, comap_inf_principal_range, comap_injective, comap_inl_map_inr, comap_inr_map_inl, comap_le_comap_iff, comap_le_iff_le_kernMap, comap_map, comap_mono, comap_neBot, comap_neBot_iff, comap_neBot_iff_compl_range, comap_neBot_iff_frequently, comap_principal, comap_pure, comap_sSup, comap_snd_neBot, comap_snd_neBot_iff, comap_sumElim_eq, comap_sup, comap_surjective_eq_bot, comap_top, compl_mem_comap, compl_mem_kernMap, disjoint_comap, disjoint_comap_iff, disjoint_comap_iff_map, disjoint_comap_iff_map', disjoint_map, disjoint_of_map, eventuallyEq_bind, eventuallyEq_map, eventuallyLE_bind, eventuallyLE_map, eventually_bind, eventually_comap, eventually_map, eventually_pure, filter_injOn_Iic_iff_injOn, frequently_bind, frequently_comap, frequently_map, gc_comap_kernMap, gc_map_comap, generate_image_preimage_le_comap, iSup_pure_eq_top, image_coe_mem_of_mem_comap, image_mem_map, image_mem_map_iff, image_mem_of_mem_comap, inf_principal_eq_bot_iff_comap, instCommApplicative, instLawfulApplicative, instLawfulFunctor, join_pure, kernMap_principal, lawfulMonad, le_comap_map, le_comap_top, le_map, le_map_iff, le_pure_iff, le_seq, map_biInf_eq, map_bind, map_bot, map_comap, map_comap_inl_sup_map_comap_inr, map_comap_le, map_comap_of_mem, map_comap_of_surjective, map_comap_setCoe_val, map_comm, map_compose, map_congr, map_const, map_def, map_eq_bot_iff, map_eq_comap_of_inverse, map_eq_map_iff_of_injOn, map_equiv_symm, map_generate_le_generate_preimage_preimage, map_iInf_eq, map_iInf_le, map_iSup, map_id, map_id', map_inf, map_inf', map_inf_le, map_inj, map_injective, map_inl_inf_map_inr, map_inr_inf_map_inl, map_le_iff_le_comap, map_le_map_iff, map_le_map_iff_of_injOn, map_map, map_mono, map_neBot, map_neBot_iff, map_principal, map_pure, map_sumElim_eq, map_sup, map_surjOn_Iic_iff_le_map, map_surjOn_Iic_iff_surjOn, map_swap4_eq_comap, map_swap_eq_comap_swap, map_top, mem_bind, mem_bind', mem_comap, mem_comap', mem_comap'', mem_comap_iff, mem_comap_iff_compl, mem_comap_prodMk, mem_kernMap, mem_kernMap_iff_compl, mem_map, mem_map', mem_map_iff_exists_image, mem_map_seq_iff, mem_seq_def, mem_seq_iff, neBot_inf_comap_iff_map, neBot_inf_comap_iff_map', neBot_of_comap, preimage_mem_comap, principal_bind, principal_eq_map_coe_top, principal_singleton, principal_subtype, prod_map_seq_comm, pure_bind, pure_injective, pure_le_principal, pure_neBot, pure_seq_eq_map, pure_sets, push_pull, push_pull', range_mem_map, sInter_comap_sets, seq_assoc, seq_eq_filter_seq, seq_mem_seq, seq_mono, seq_pure, singleton_mem_pure, subtype_coe_map_comap, sup_bind, filter_comap, filter_map, filter_comap, filter_map, filter_comap, filter_map, filter_comap, filter_map, filter_map_top, filter_map_Iic, filter_map_Iic, filter_map_Iic, filter_map_Iic | 197 |
| Total | 202 |