| Metric | Count |
|---|
DefinitionscompleteLattice, infSet, instCompleteLattice, supSet, infSet, instCompleteLattice, supSet, instCompleteLattice, instCompleteLinearOrder | 9 |
TheoremsiInf, iSup, le_map_iInf, le_map_iInfβ, le_map_sInf, map_iSup_le, map_iSupβ_le, map_sSup_le, sInf, sSup, biInf_comp, biSup_comp, iInf_comp, iInf_congr, iSup_comp, iSup_congr, iInf_comp, iInf_congr, iSup_comp, iSup_congr, iInf_eq, iSup_eq, iInf, iInf_comp_eq, iSup, iSup_comp_eq, le_map_iSup, le_map_iSupβ, le_map_sSup, map_iInf_le, map_iInfβ_le, map_sInf_le, sInf, sSup, map_iInf, map_iInfβ, map_iSup, map_iSupβ, map_sInf, map_sInf_eq_sInf_symm_preimage, map_sSup, map_sSup_eq_sSup_symm_preimage, fst_iInf, fst_iSup, fst_sInf, fst_sSup, iInf_mk, iSup_mk, snd_iInf, snd_iSup, snd_sInf, snd_sSup, swap_iInf, swap_iSup, swap_sInf, swap_sSup, iInf_comp, iInf_congr, iSup_comp, iSup_congr, biInf_congr, biInf_congr', biInf_const, biInf_ge_eq_iInf, biInf_ge_eq_inf, biInf_ge_eq_of_monotone, biInf_gt_eq_iInf, biInf_inf, biInf_le, biInf_le_biSup, biInf_le_eq_iInf, biInf_le_eq_inf, biInf_le_eq_of_antitone, biInf_lt_eq_iInf, biInf_mono, biInf_prod, biInf_prod', biSup_congr, biSup_congr', biSup_const, biSup_ge_eq_iSup, biSup_ge_eq_of_antitone, biSup_ge_eq_sup, biSup_gt_eq_iSup, biSup_le_eq_iSup, biSup_le_eq_of_monotone, biSup_le_eq_sup, biSup_lt_eq_iSup, biSup_mono, biSup_prod, biSup_prod', biSup_sup, binary_relation_sInf_iff, binary_relation_sSup_iff, bot_lt_iSup, eq_singleton_bot_of_sSup_eq_bot_of_nonempty, eq_singleton_top_of_sInf_eq_top_of_nonempty, iInf_Prop_eq, iInf_and, iInf_and', iInf_apply, iInf_comm, iInf_congr, iInf_congr_Prop, iInf_const, iInf_const_mono, iInf_dite, iInf_emptyset, iInf_eq_bot, iInf_eq_dif, iInf_eq_if, iInf_eq_of_forall_ge_of_forall_gt_exists_lt, iInf_eq_top, iInf_exists, iInf_extend_top, iInf_false, iInf_iInf_eq_left, iInf_iInf_eq_right, iInf_image, iInf_image2, iInf_inf, iInf_inf_eq, iInf_insert, iInf_ite, iInf_le, iInf_le_iInf_of_subset, iInf_le_iInfβ, iInf_le_iSup, iInf_le_of_le, iInf_lt_top, iInf_mono, iInf_mono', iInf_ne_top_subtype, iInf_neg, iInf_of_empty, iInf_of_isEmpty, iInf_option, iInf_option_elim, iInf_or, iInf_pair, iInf_plift_down, iInf_plift_up, iInf_pos, iInf_prod, iInf_prod', iInf_psigma, iInf_psigma', iInf_range, iInf_range', iInf_sigma, iInf_sigma', iInf_singleton, iInf_split, iInf_split_single, iInf_subtype, iInf_subtype', iInf_subtype'', iInf_sum, iInf_top, iInf_true, iInf_ulift, iInf_union, iInf_unique, iInf_univ, iInfβ_comm, iInfβ_eq_bot, iInfβ_eq_top, iInfβ_le, iInfβ_le_of_le, iInfβ_mono, iInfβ_mono', iSup_Prop_eq, iSup_and, iSup_and', iSup_apply, iSup_bot, iSup_comm, iSup_comp_le, iSup_congr, iSup_congr_Prop, iSup_const, iSup_const_le, iSup_const_mono, iSup_dite, iSup_emptyset, iSup_eq_bot, iSup_eq_dif, iSup_eq_if, iSup_eq_of_forall_le_of_forall_lt_exists_gt, iSup_eq_top, iSup_exists, iSup_extend_bot, iSup_false, iSup_iInf_le_iInf_iSup, iSup_iSup_eq_left, iSup_iSup_eq_right, iSup_image, iSup_image2, iSup_insert, iSup_ite, iSup_le, iSup_le_iSup_of_subset, iSup_le_iff, iSup_lt_iff, iSup_mono, iSup_mono', iSup_ne_bot_subtype, iSup_neg, iSup_of_empty, iSup_of_empty', iSup_option, iSup_option_elim, iSup_or, iSup_pair, iSup_plift_down, iSup_plift_up, iSup_pos, iSup_prod, iSup_prod', iSup_psigma, iSup_psigma', iSup_range, iSup_range', iSup_sigma, iSup_sigma', iSup_singleton, iSup_split, iSup_split_single, iSup_subtype, iSup_subtype', iSup_subtype'', iSup_sum, iSup_sup, iSup_sup_eq, iSup_true, iSup_ulift, iSup_union, iSup_unique, iSup_univ, iSupβ_comm, iSupβ_eq_bot, iSupβ_eq_top, iSupβ_le, iSupβ_le_iSup, iSupβ_le_iff, iSupβ_mono, iSupβ_mono', inf_biInf, inf_iInf, isGLB_biInf, isGLB_iInf, isLUB_biSup, isLUB_iSup, le_biSup, le_iInf, le_iInf_comp, le_iInf_const, le_iInf_iff, le_iInfβ, le_iInfβ_iff, le_iSup, le_iSup_of_le, le_iSupβ, le_iSupβ_of_le, le_sInf_inter, lt_iInf_iff, sInf_Prop_eq, sInf_apply, sInf_diff_singleton_top, sInf_empty, sInf_eq_iInf, sInf_eq_iInf', sInf_eq_of_forall_ge_of_forall_gt_exists_lt, sInf_eq_top, sInf_image, sInf_image', sInf_image2, sInf_insert, sInf_le_sInf_of_isCoinitialFor, sInf_le_sInf_of_subset_insert_top, sInf_le_sSup, sInf_pair, sInf_prod, sInf_range, sInf_singleton, sInf_union, sInf_univ, sInf_upperBounds_eq_csSup, sInf_upperBounds_eq_sSup, sSup_Prop_eq, sSup_apply, sSup_diff_singleton_bot, sSup_empty, sSup_eq_bot, sSup_eq_bot', sSup_eq_iSup, sSup_eq_iSup', sSup_eq_of_forall_le_of_forall_lt_exists_gt, sSup_image, sSup_image', sSup_image2, sSup_insert, sSup_inter_le, sSup_le_sSup_of_isCofinalFor, sSup_le_sSup_of_subset_insert_bot, sSup_lowerBounds_eq_sInf, sSup_pair, sSup_prod, sSup_range, sSup_singleton, sSup_union, sSup_univ, sup_biSup, sup_iSup, unary_relation_sInf_iff, unary_relation_sSup_iff | 316 |
| Total | 325 |