| Metric | Count |
|---|
DefinitionssetSubtypeComm, some, decidableCompl, decidableEmptyset, decidableInsert, decidableInter, decidableSdiff, decidableSetOf, decidableUnion, decidableUniv, instBoundedOrder, instDistribLattice, instHasSSubset, instInhabited, instTransSSubset, instTransSSubsetSubset, instTransSubset, instTransSubsetSSubset, uniqueEmpty, instCoeTCElem | 20 |
TheoremssetSubtypeComm_apply, setSubtypeComm_symm_apply, nonempty_apply_iff, lt, le, subset, ssubset, elim, coe_sort, empty_ssubset, eq_univ, inl, inr, left, mono, ne_empty, not_subset_empty, of_diff, of_subtype, right, some_mem, to_subtype, to_type, canLift, canLift', antisymm, antisymm_iff, refl, rfl, trans, bot_eq_empty, coe_eq_subtype, coe_setOf, empty_def, empty_inter, empty_ne_univ, empty_ssubset, empty_subset, empty_union, eq_empty_iff_forall_notMem, eq_empty_of_forall_notMem, eq_empty_of_isEmpty, eq_empty_of_subset_empty, eq_empty_or_nonempty, eq_of_forall_subset_iff, eq_of_subset_of_subset, eq_or_ssubset_of_subset, eq_univ_iff_forall, eq_univ_of_forall, eq_univ_of_subset, eq_univ_of_univ_subset, exists_mem_of_nonempty, exists_of_ssubset, forall_mem_empty, inf_eq_inter, instAntisymmSubset, instAsymmSSubset, instIrreflSSubset, instIsEmptyElemEmptyCollection, instIsNonstrictStrictOrderSubsetSSubset, instIsTransSSubset, instIsTransSubset, instNonemptyTop, instReflSubset, inter_assoc, inter_comm, inter_congr_left, inter_congr_right, inter_def, inter_empty, inter_eq_inter_iff_left, inter_eq_inter_iff_right, inter_eq_left, inter_eq_right, inter_eq_self_of_subset_left, inter_eq_self_of_subset_right, inter_inter_distrib_left, inter_inter_distrib_right, inter_inter_inter_comm, inter_isAssoc, inter_isComm, inter_left_comm, inter_nonempty, inter_nonempty_iff_exists_left, inter_nonempty_iff_exists_right, inter_right_comm, inter_self, inter_setOf_eq_sep, inter_ssubset_left_iff, inter_ssubset_right_iff, inter_subset_inter, inter_subset_inter_left, inter_subset_inter_right, inter_subset_left, inter_subset_right, inter_union_distrib_left, inter_union_distrib_right, inter_univ, isEmpty_coe_sort, le_eq_subset, le_iff_subset, left_eq_inter, lt_eq_ssubset, lt_iff_ssubset, mem_dite_empty_left, mem_dite_empty_right, mem_dite_univ_left, mem_dite_univ_right, mem_empty_iff_false, mem_inter, mem_inter_iff, mem_ite_empty_left, mem_ite_empty_right, mem_ite_univ_left, mem_ite_univ_right, mem_of_eq_of_mem, mem_of_mem_inter_left, mem_of_mem_inter_right, mem_of_mem_of_subset, mem_of_subset_of_mem, mem_or_mem_of_mem_union, mem_powerset, mem_powerset_iff, mem_sep, mem_sep_iff, mem_union, mem_union_left, mem_union_right, monotone_powerset, ne_univ_iff_exists_notMem, nonempty_coe_sort, nonempty_def, nonempty_iff_empty_ne, nonempty_iff_ne_empty, nonempty_iff_ne_empty', nonempty_iff_univ_nonempty, nonempty_of_mem, nonempty_of_not_subset, nonempty_of_ssubset, nonempty_of_ssubset', nontrivial_of_nonempty, notMem_empty, notMem_subset, not_nonempty_empty, not_nonempty_iff_eq_empty, not_nonempty_iff_eq_empty', not_notMem, not_subset, not_subset_iff_exists_mem_notMem, not_top_subset, powerset_empty, powerset_inter, powerset_mono, powerset_nonempty, powerset_univ, right_eq_inter, sep_and, sep_empty, sep_eq_empty_iff_mem_false, sep_eq_inter_sep, sep_eq_of_subset, sep_eq_self_iff_mem_true, sep_ext_iff, sep_false, sep_inter, sep_mem_eq, sep_of_subset, sep_or, sep_setOf, sep_subset, sep_subset_setOf, sep_true, sep_union, sep_univ, setOf_and, setOf_bijective, setOf_bot, setOf_false, setOf_inj, setOf_injective, setOf_inter_eq_sep, setOf_or, setOf_subset, setOf_subset_setOf, setOf_subset_setOf_of_imp, setOf_top, setOf_true, ssubset_def, ssubset_iff_exists, ssubset_iff_of_subset, ssubset_iff_subset_ne, ssubset_of_ssubset_of_subset, ssubset_of_subset_of_ssubset, ssubset_union_left_iff, ssubset_union_right_iff, ssubset_univ_iff, subset_def, subset_empty_iff, subset_eq_empty, subset_inter, subset_inter_iff, subset_of_mem_powerset, subset_setOf, subset_union_left, subset_union_of_subset_left, subset_union_of_subset_right, subset_union_right, subset_univ, sup_eq_union, top_eq_univ, union_assoc, union_comm, union_congr_left, union_congr_right, union_def, union_empty, union_empty_iff, union_eq_left, union_eq_right, union_eq_self_of_subset_left, union_eq_self_of_subset_right, union_eq_union_iff_left, union_eq_union_iff_right, union_inter_cancel_left, union_inter_cancel_right, union_inter_distrib_left, union_inter_distrib_right, union_isAssoc, union_isComm, union_left_comm, union_nonempty, union_right_comm, union_self, union_subset, union_subset_iff, union_subset_union, union_subset_union_left, union_subset_union_right, union_union_distrib_left, union_union_distrib_right, union_union_union_comm, union_univ, nonempty, univ_eq_empty_iff, univ_inter, univ_nonempty, univ_subset_iff, univ_union, univ_unique, exists, exists', ext, ext_iff, forall, forall', eq_univ_of_nonempty, mem_iff_nonempty, set_cases, mem, set_coe_cast | 260 |
| Total | 280 |
| Name | Category | Theorems |
|---|
decidableCompl 📖 | CompOp | 7 mathmath: SimpleGraph.edgeFinset_top, SimpleGraph.neighborFinset_subset_between_union, SimpleGraph.neighborFinset_subset_between_union_compl, SimpleGraph.degree_le_between_add, Sym2.card_diagSet_compl, SimpleGraph.degree_le_between_add_compl, SimpleGraph.card_edgeFinset_induce_compl_singleton
|
decidableEmptyset 📖 | CompOp | 1 mathmath: schnirelmannDensity_empty
|
decidableInsert 📖 | CompOp | — |
decidableInter 📖 | CompOp | — |
decidableSdiff 📖 | CompOp | — |
decidableSetOf 📖 | CompOp | 16 mathmath: FormalMultilinearSeries.comp_rightInv_aux1, quadraticChar_card_sqrts, schnirelmannDensity_setOf_prime, schnirelmannDensity_setOf_even, PEquiv.symm_trans_self, Finset.sum_toFinset_eq_subtype, FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1, legendreSym.card_sqrts, schnirelmannDensity_setOf_modeq_one, schnirelmannDensity_setOf_Odd, PEquiv.self_trans_symm, FormalMultilinearSeries.rightInv_coeff, Finset.prod_toFinset_eq_subtype, FormalMultilinearSeries.comp_rightInv_aux2, schnirelmannDensity_setOf_mod_eq_one, SimpleGraph.Walk.IsEulerian.card_odd_degree
|
decidableUnion 📖 | CompOp | — |
decidableUniv 📖 | CompOp | 2 mathmath: schnirelmannDensity_univ, PEquiv.ofSet_univ
|
instBoundedOrder 📖 | CompOp | 38 mathmath: TopCat.binaryCofan_isColimit_iff, CategoryTheory.Limits.Types.binaryCofan_isColimit_iff, disjoint_or_nonempty_inter, disjoint_union_right, isCompl_range_some_none, disjoint_singleton_right, disjoint_left, MeasureTheory.SignedMeasure.exists_isCompl_positive_negative, disjoint_singleton_left, disjoint_right, Concept.isCompl_extent_intent, disjoint_singleton, instNonemptyTop, Order.Ideal.PrimePair.isCompl_I_F, not_disjoint_iff_nonempty_inter, Int.isCompl_even_odd, AlgebraicGeometry.isCompl_range_inl_inr, disjoint_insert_left, addCentralizer_empty, bot_eq_empty, top_eq_univ, not_disjoint_iff, disjoint_iff_inter_eq_empty, disjoint_insert_right, disjoint_univ, isCompl_range_inl_range_inr, disjoint_iff_forall_ne, univ_disjoint, disjoint_empty, centralizer_empty, Nat.isCompl_even_odd, not_top_subset, disjoint_range_iff, empty_disjoint, disjoint_union_left, OnePoint.isCompl_range_coe_infty, disjoint_iff, Nonempty.not_disjoint
|
instDistribLattice 📖 | CompOp | 32 mathmath: disjoint_or_nonempty_inter, disjoint_union_right, disjoint_singleton_right, disjoint_left, disjoint_singleton_left, disjoint_right, antitone_setOf, disjoint_singleton, HasSSubset.SSubset.lt, sup_eq_union, not_disjoint_iff_nonempty_inter, disjoint_insert_left, lt_eq_ssubset, not_disjoint_iff, disjoint_iff_inter_eq_empty, antitone_bforall, disjoint_insert_right, disjoint_univ, SetLike.coe_strictMono, monotone_setOf, disjoint_iff_forall_ne, univ_disjoint, disjoint_empty, inf_eq_inter, lt_iff_ssubset, disjoint_range_iff, empty_disjoint, disjoint_union_left, monotone_powerset, SetLike.coe_mono, disjoint_iff, Nonempty.not_disjoint
|
instHasSSubset 📖 | CompOp | 86 mathmath: not_maximal_subset_iff, Submodule.iUnion_ssubset_of_forall_ne_top_of_card_lt, ssubset_iff_sdiff_singleton, ssubset_iff_subset_ne, Matroid.IsStrictMinor.ssubset, Ioi_ssubset_Ioi, PrimeSpectrum.vanishingIdeal_strict_anti_mono_iff, empty_ssubset_singleton, Finite.ssubset_toFinset, toFinset_ssubset_toFinset, inter_ssubset_left_iff, ssubset_def, SetSemiring.up_lt_up, UpperSet.coe_ssubset_coe, ssubset_insert, Matroid.not_spanning_iff_closure_ssubset, Ici_ssubset_Ici, singleton_ssubset_univ, Sublattice.mk_lt_mk, Iio_ssubset_Iic_self, SimpleGraph.edgeSet_ssubset_edgeSet, range_inter_ssubset_iff_preimage_ssubset, diff_ssubset_left_iff, AffineSubspace.lt_def, Minimal.not_ssubset, Filter.sets_ssubset_sets, LowerSet.coe_ssubset_coe, ssubset_iff_exists, Matroid.IsStrictRestriction.ssubset, NonemptyInterval.coe_ssubset_coe, diff_singleton_ssubset, instIsNonstrictStrictOrderSubsetSSubset, not_minimal_subset_iff, lt_eq_ssubset, Finite.toFinset_ssubset_toFinset, Matroid.Indep.closure_diff_singleton_ssubset, Matroid.indep_iff_forall_closure_ssubset_of_ssubset, Finset.coe_ssubset, AddAction.IsBlock.not_vadd_set_ssubset_vadd_set, Matroid.Indep.closure_diff_ssubset, Finite.toFinset_ssubset, Concept.intent_ssubset_intent_iff, Iic_ssubset_Iic, SetLike.coe_ssubset_coe, LT.lt.ssubset, Affine.Simplex.interior_ssubset_closedInterior, SimpleGraph.edgeSet_strict_mono, instAsymmSSubset, toFinset_ssubset, Iio_ssubset_Iio_iff, HasSubset.Subset.diff_ssubset_of_nonempty, Matroid.IsCircuit.not_ssubset, ssubset_toFinset, Icc_ssubset_Icc_left, instIrreflSSubset, SetSemiring.down_ssubset_down, Interval.coe_sSubset_coe, HasSubset.Subset.ssubset_of_mem_notMem, Maximal.not_ssuperset, ssubset_union_right_iff, prod_self_ssubset_prod_self, MulAction.IsBlock.not_smul_set_ssubset_smul_set, Icc_ssubset_Icc_right, TwoSidedIdeal.lt_iff, toFinset_ssubset_univ, ssubset_univ_iff, empty_ssubset, lt_iff_ssubset, InjOn.image_ssubset_image_iff, Iio_ssubset_Iio, ssubset_union_left_iff, ssubset_iff_of_subset, inter_ssubset_right_iff, ssubset_singleton_iff, Concept.extent_ssubset_extent_iff, instIsTransSSubset, Matroid.IsBase.ssubset_ground, Order.Ideal.coe_ssubset_coe, Matroid.isStrictMinor_iff_isMinor_ssubset, eq_or_ssubset_of_subset, Ioi_ssubset_Ici_self, Nonempty.empty_ssubset, Matroid.IsStrictRestriction.exists_eq_restrict, ssubset_iff_insert, Ioi_ssubset_Ioi_iff, Matroid.Indep.ssubset_ground
|
instInhabited 📖 | CompOp | — |
instTransSSubset 📖 | CompOp | — |
instTransSSubsetSubset 📖 | CompOp | — |
instTransSubset 📖 | CompOp | — |
instTransSubsetSSubset 📖 | CompOp | — |
uniqueEmpty 📖 | CompOp | — |