| Metric | Count |
|---|
DefinitionsGenerateSets, generate, giGenerate, inhabitedMem, instCoframe, instCompleteLatticeFilter, instDistribLattice, instInhabited, instTransForallEventuallyEq, instTransForallEventuallyEqEventuallyLE, instTransForallEventuallyLE, instTransForallEventuallyLEEventuallyEq, instTransSetMemSubset, instTransSetSupersetMem, mkOfClosure, unique | 16 |
TheoremseventuallyEq, and, and_frequently, choice, exists, exists_mem, filter_mono, forall_mem, frequently, lt_top_iff_ne_top, lt_top_of_ne, mono, mp, ne_of_lt, ne_top_of_lt, of_forall, set_eq, add, add_left, add_right, compl, comp₂, congr_left, congr_right, const_smul, const_vadd, diff, div, eventually, exists_mem, filter_mono, fun_add, fun_comp, fun_const_smul, fun_const_vadd, fun_div, fun_inv, fun_mul, fun_neg, fun_pow_const, fun_star, fun_sub, inf, inter, inv, le, mem_iff, mul, mul_left, mul_right, neg, of_eq, pow_const, preimage, prodMk, refl, rfl, rw, smul, sub, sub_eq, sup, symmDiff, trans, trans_le, union, vadd, antisymm, compl, diff, ge_iff_eq', inter, le_sup_of_le_left, le_sup_of_le_right, refl, rfl, sup, sup_le, trans, trans_eq, union, and_eventually, exists, filter_mono, inf_principal, mono, mp, of_forall, of_inf_principal, Iic_principal, mono, ne, nonempty, nonempty_of_mem, not_disjoint, biInf_sets_eq, biInter_mem', bot_sets_eq, coext, compl_mem_comk, compl_notMem, congr_sets, copy_eq, diff_mem, diff_mem_inf_principal_compl, disjoint_iff, disjoint_of_disjoint_of_mem, empty_mem_iff_bot, empty_notMem, eq_biInf_of_mem_iff_exists_mem, eq_iInf_of_mem_iff_exists_mem, eq_or_neBot, eq_sInf_of_mem_iff_exists_mem, eq_top_of_neBot, eventuallyEq_comm, eventuallyEq_empty, eventuallyEq_iff_all_subsets, eventuallyEq_iff_exists_mem, eventuallyEq_iff_sub, eventuallyEq_inf_principal_iff, eventuallyEq_of_mem, eventuallyEq_principal, eventuallyEq_set, eventuallyEq_top, eventuallyEq_univ, eventuallyLE_antisymm_iff, eventuallyLE_congr, eventuallyLE_iff_all_subsets, eventually_and, eventually_bot, eventually_congr, eventually_const, eventually_false_iff_eq_bot, eventually_iSup, eventually_iff, eventually_iff_all_subsets, eventually_iff_exists_mem, eventually_imp_distrib_left, eventually_imp_distrib_right, eventually_inf, eventually_inf_principal, eventually_mem_principal, eventually_mem_set, eventually_of_mem, eventually_or_distrib_left, eventually_or_distrib_right, eventually_principal, eventually_sSup, eventually_sup, eventually_top, eventually_true, exists_mem_and_iff, exists_mem_subset_iff, ext', filter_eq_bot_of_isEmpty, filter_eq_iff, forall_eventually_of_eventually_forall, forall_mem_nonempty_iff_neBot, frequently_and_distrib_left, frequently_and_distrib_right, frequently_bot, frequently_congr, frequently_const, frequently_false, frequently_iSup, frequently_iff, frequently_iff_forall_eventually_exists_and, frequently_iff_neBot, frequently_imp_distrib, frequently_imp_distrib_left, frequently_imp_distrib_right, frequently_inf_principal, frequently_mem_iff_neBot, frequently_or_distrib, frequently_or_distrib_left, frequently_or_distrib_right, frequently_principal, frequently_sSup, frequently_sup, frequently_top, frequently_true_iff_neBot, generate_empty, generate_eq_biInf, generate_iUnion, generate_singleton, generate_union, generate_univ, iInf_eq_generate, iInf_neBot_iff_of_directed, iInf_neBot_iff_of_directed', iInf_neBot_of_directed, iInf_neBot_of_directed', iInf_sets_eq, iInf_sets_induct, iInter_mem', iSup_inf_principal, iSup_join, iSup_neBot, iSup_principal, iSup_sets_eq, inf_eq_bot_iff, inf_principal, inf_principal_eq_bot, instNeBotTop, instNontrivialFilter, inter_eventuallyEq_left, inter_eventuallyEq_right, inter_mem_iff, inter_mem_inf, isCompl_principal, join_le, join_mono, join_principal_eq_sSup, le_generate_iff, le_principal_iff, mem_biInf_of_directed, mem_generate_of_mem, mem_iInf_of_directed, mem_iInf_of_mem, mem_iSup, mem_inf_iff, mem_inf_iff_superset, mem_inf_of_inter, mem_inf_of_left, mem_inf_of_right, mem_inf_principal, mem_inf_principal', mem_of_eq_bot, mem_principal_self, mem_sdiff_iff_union, mem_sup, mkOfClosure_sets, monotone_mem, monotone_principal, neBot_of_le, nonempty_of_mem, nonempty_of_neBot, nontrivial_iff_nonempty, not_disjoint_self_iff, not_eventually, not_frequently, not_le, not_neBot, principal_empty, principal_eq_bot_iff, principal_eq_iff_eq, principal_le_iff, principal_mono, principal_neBot_iff, principal_univ, sInf_neBot_of_directed, sInf_neBot_of_directed', sSup_sets_eq, set_eventuallyEq_iff_inf_principal, set_eventuallyLE_iff_inf_principal_le, set_eventuallyLE_iff_mem_inf_principal, sets_ssubset_sets, sets_subset_sets, skolem, sup_join, sup_neBot, sup_principal, sup_sets_eq, union_mem_sup, eventuallyLE, eventuallyEq, eventuallyEq_of_mem, principal_neBot | 268 |
| Total | 284 |