| Name | Category | Theorems |
|---|
toBot 📖 | CompOp | 109 mathmath: SimpleGraph.locallyLinear_bot, SimpleGraph.cliqueSet_bot, BooleanSubalgebra.val_bot, SimpleGraph.killCopies_bot, Equiv.Perm.support_prod_of_pairwise_disjoint, SimpleGraph.cliqueFree_two, SimpleGraph.eccent_bot, SimpleGraph.copyCount_bot, CategoryTheory.isCoseparating_empty_of_thin, SimpleGraph.bot_not_connected, CategoryTheory.isCodetecting_empty_of_groupoid, Polynomial.roots_eq_zero_iff_isRoot_eq_bot, SimpleGraph.bot_not_preconnected, BooleanSubalgebra.coe_bot, SimpleGraph.UnitDistEmbedding.bot_p, CategoryTheory.ObjectProperty.isCodetecting_bot_of_isGroupoid, SimpleGraph.cycleGraph_one_eq_bot, SimpleGraph.edgeDisjointTriangles_bot, SimpleGraph.emptyGraph_eq_bot, SimpleGraph.singletonSubgraph_adj, SimpleGraph.center_bot, SimpleGraph.deleteEdges_univ, ofBoolAlg_bot, SimpleGraph.girth_bot, CategoryTheory.ObjectProperty.isDetecting_bot_of_isGroupoid, BooleanSubalgebra.bot_mem', SimpleGraph.free_bot, toBoolAlg_zero, SSet.nonDegenerate_eq_bot_of_hasDimensionLT, Digraph.default_def, Digraph.bot_adj, SimpleGraph.edgeSet_bot, SimpleGraph.edge_self_eq_bot, SimpleGraph.cliqueFree_bot, SimpleGraph.Subgraph.spanningCoe_bot, MeasurableSet.coe_bot, Irreducible.isRoot_eq_bot_of_natDegree_ne_one, Sym2.fromRel_bot_iff, SimpleGraph.preconnected_bot, inf_compl_le_bot, SimpleGraph.egirth_bot, SimpleGraph.support_eq_bot_iff, CategoryTheory.Subfunctor.Subpresheaf.bot_obj, SimpleGraph.isVertexCover_bot, CategoryTheory.isSeparating_empty_of_thin, SimpleGraph.maxDegree_bot_eq_zero, SimpleGraph.vertexCoverNum_eq_zero, ofBoolRing_zero, SimpleGraph.not_connected_bot, SimpleGraph.default_def, Digraph.toSimpleGraphInclusive_bot, Coheyting.boundary_eq_bot, SimpleGraph.IsContained.bot, SimpleGraph.edist_bot, SimpleGraph.bot_isContained_iff_card_le, SimpleGraph.dist_bot, inf_compl_eq_bot', SimpleGraph.diam_bot, Set.pairwise_bot_iff, CategoryTheory.Subfunctor.bot_obj, SimpleGraph.support_bot, SimpleGraph.fromEdgeSet_empty, SimpleGraph.connected_bot_iff, Sym2.fromRel_bot, SimpleGraph.lineGraph_bot, SimpleGraph.reachable_bot, CategoryTheory.ObjectProperty.isSeparating_bot_of_isThin, Equiv.Perm.support_prod_le, SimpleGraph.bot_preconnected_iff_subsingleton, SimpleGraph.bot_adj, SimpleGraph.isClique_bot_iff, SimpleGraph.eq_bot_iff_forall_not_adj, SimpleGraph.edgeFinset_bot, SimpleGraph.completeEquipartiteGraph_eq_bot_iff, SimpleGraph.not_isHamiltonian_bot_of_card_ne_one, compl_eq_bot, SimpleGraph.edgeFinset_eq_empty, MvPolynomial.zeroLocus_top, SimpleGraph.bot_degree, SimpleGraph.bot_isCompleteMultipartite, Polynomial.roots_eq_zero_iff_eq_zero_or_isRoot_eq_bot, Digraph.toSimpleGraphStrict_bot, BooleanSubalgebra.bot_mem, SimpleGraph.minDegree_bot_eq_zero, SimpleGraph.preconnected_bot_iff_subsingleton, SimpleGraph.radius_bot, compl_eq_top, CategoryTheory.isDetecting_empty_of_groupoid, SimpleGraph.edgeSet_eq_empty, SimpleGraph.not_preconnected_bot, bot_le, Digraph.emptyDigraph_eq_bot, SimpleGraph.killCopies_def, CategoryTheory.ObjectProperty.isCoseparating_bot_of_isThin, SimpleGraph.isAcyclic_bot, SimpleGraph.isNClique_bot_iff, SimpleGraph.bot_preconnected, SimpleGraph.ediam_bot, SimpleGraph.cycleGraph_zero_eq_bot, SimpleGraph.chromaticNumber_eq_one_iff, toBoolRing_bot, BooleanSubalgebra.mk_bot, SimpleGraph.bot_strongly_regular, SimpleGraph.isVertexCover_empty, BooleanSubalgebra.mem_bot, bihimp_eq_bot, SimpleGraph.edist_bot_of_ne, SimpleGraph.chromaticNumber_bot, SimpleGraph.Subgraph.coe_bot
|
toBoundedOrder 📖 | CompOp | 64 mathmath: BoolAlg.coe_id, BoolRing.hasForgetToBoolAlg_forget₂_obj_coe, BooleanSubalgebra.map_map, BoolAlg.hasForgetToBoolRing_forget₂_obj_carrier, BoolAlg.ext_iff, BoolAlg.hasForgetToBoolRing_forget₂_map, BooleanSubalgebra.subtype_comp_inclusion, boolRingCatEquivBoolAlg_functor, BoolAlg.ofHom_comp, BooleanSubalgebra.mem_comap, BooleanSubalgebra.coe_map, BoolAlg.hom_id, BoolAlg.hasForgetToHeytAlg_forget₂_map, FinBoolAlg.forgetToFinPartOrdFaithful, BooleanSubalgebra.subtype_injective, BooleanSubalgebra.apply_coe_mem_map, BooleanSubalgebra.coe_inclusion, BooleanSubalgebra.comap_id, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_carrier, RingHom.asBoolAlg_id, BoolAlg.hom_comp, BooleanSubalgebra.mem_map_of_mem, eq_compl_iff_isCompl, RingHom.asBoolAlg_comp, BooleanSubalgebra.subtype_apply, BooleanSubalgebra.inclusion_injective, BoolAlg.ofHom_id, BoolAlg.dual_map, boolRingCatEquivBoolAlg_inverse, BoolAlg.coe_comp, BoundedLatticeHom.asBoolRing_apply, BoolRing.hasForgetToBoolAlg_forget₂_map, BoolAlg.hom_inv_apply, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_isFintype, BooleanSubalgebra.mem_map, BoolAlg.comp_apply, toComplementedLattice, BoundedLatticeHom.asBoolRing_id, finBoolAlg_dual_comp_forget_to_finBddDistLat, BoundedLatticeHom.asBoolRing_comp, BoolAlg.hasForgetToHeytAlg_forget₂_obj_coe, BooleanSubalgebra.coe_subtype, BooleanSubalgebra.inclusion_rfl, compl_eq_iff_isCompl, symmDiff_eq_top, isCompl_compl, BooleanSubalgebra.coe_comap, Finset.compl_truncatedInf, BoolAlg.inv_hom_apply, boolAlg_dual_comp_forget_to_bddDistLat, FinBoolAlg.hasForgetToFinPartOrd_forget₂_map, FinBoolAlg.forgetToBoolAlg_full, BooleanSubalgebra.inclusion_apply, BooleanSubalgebra.map_id, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_str, FinBoolAlg.dual_map, BoolAlg.id_apply, FinBoolAlg.forgetToBoolAlgFaithful, Finset.compl_truncatedSup, bihimp_eq_bot, BooleanSubalgebra.comap_comap, BoolAlg.ofHom_apply, BoolAlg.forget_map, RingHom.asBoolAlg_toFun
|
toCompl 📖 | CompOp | 217 mathmath: Finset.insert_compl_self, codisjoint_iff_compl_le_right, compl_symmDiff_self, Finset.compl_ssubset_compl, MeasureTheory.GridLines.T_lmarginal_antitone, SSet.horn₃₁.desc.multicofork_π_two, Finset.Ioi_disjUnion_Iio, Finset.compl_inter, SSet.horn.faceSingletonComplIso_inv_ι_assoc, symmDiff_eq', IsAntichain.image_compl, sup_inf_inf_compl, Set.compl_compl_image, Finset.compl_eq_univ_sdiff, Finset.card_compl_add_card, Fin.image_succ_univ, compl_inf, Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub, symmDiff_compl_self, compl_sInf, Set.toFinset_compl, Finset.insert_compl_insert, Finset.compl_inf, compl_sdiff, Order.Ideal.IsProper.notMem_or_compl_notMem, symmDiff_top, SSet.horn₃₂.desc.multicofork_π_one, compl_compl, Order.Ideal.IsPrime.compl_mem_of_notMem, Finset.union_compl, Matrix.adjp_apply, Bool.compl_eq_bnot, sdiff_eq, Finset.card_add_card_compl, map_compl', Finset.compl_erase, Finset.compl_sup, Finset.inclusion_exclusion_card_inf_compl, Filter.limsup_compl, disjoint_compl_right_iff, codisjoint_iff_compl_le_left, IsAntichain.preimage_compl, Finset.compl_union, top_symmDiff, Finset.card_compl, isCoatom_compl, himp_eq, Finset.compl_singleton, compl_sSup', Finset.compl_mem_compls, SimpleGraph.neighborFinset_completeEquipartiteGraph, compl_symmDiff, Affine.Simplex.inner_mongePoint_vsub_face_centroid_vsub, SSet.horn₃₁.desc.multicofork_pt, SimpleGraph.neighborFinset_compl, SSet.horn.faceSingletonComplIso_inv_ι, compl_lt_self, Finset.inter_compl, compl_sSup, compl_bijective, SSet.stdSimplex.range_δ, Language.IsRegular_compl, NumberField.InfinitePlace.card_eq_card_isUnramifiedIn, Fintype.prod_add, compl_sdiff_compl, Finset.subset_compl_singleton, Finset.piecewise_compl, Finset.inclusion_exclusion_sum_inf_compl, compl_image_latticeClosure, SSet.horn₃₁.desc.multicofork_π_two_assoc, Affine.Simplex.mongePlane_def, SSet.horn₃₁.desc.multicofork_π_zero_assoc, BooleanSubalgebra.compl_mem_iff, Finset.prod_mul_prod_compl, Affine.Simplex.ExcenterExists.excenterWeights_eq_excenterWeights_iff, Fintype.prod_eq_prod_compl_mul, Finset.isCoatom_compl_singleton, inf_compl_le_bot, sdiff_eq, compl_lt_compl_iff_lt, exists_sum_eq_one_iff_pairwise_coprime', Order.Ideal.isPrime_iff_mem_or_compl_mem, GaloisConnection.compl, Finset.compl_insert, BooleanSubalgebra.compl_mem', Fintype.prod_eq_mul_prod_compl, symmDiff_eq, OrderIso.compl_symm_apply, hnot_eq_compl, compl_injective, Finset.sum_compl_add_sum, Finset.preimage_compl, Affine.Simplex.exsphere_compl, Finset.compl_filter, SSet.stdSimplex.faceSingletonComplIso_hom_ι, bihimp_eq, NumberField.InfinitePlace.card_isUnramified_compl, Finset.mem_compl, Set.Intersecting.disjoint_map_compl, Finset.coe_compl, compl_iSup, Affine.Simplex.exradius_compl, compl_iInf, Finset.compl_univ, Equiv.Perm.card_compl_support_modEq, Heyting.isRegular_of_boolean, top_sdiff, BooleanSubalgebra.val_compl, Filter.liminf_compl, compl_le_self, Finset.compl_empty, eq_compl_iff_isCompl, Finset.prod_prod_Ioi_mul_eq_prod_prod_off_diag, BooleanSubalgebra.compl_mk, SSet.face_le_horn, inf_compl_eq_bot', Finset.orderEmbOfFin_compl_singleton_eq_succAboveOrderEmb, compl_surjective, DFA.accepts_compl, Set.powersetCard.coe_compl, disjoint_compl_left_iff, SSet.horn.faceι_ι, Finset.forall_mem_compls, compl_comp_compl, compl_himp, compl_symmDiff_compl, Fin.image_castSucc, SSet.horn_eq_iSup, sup_compl_eq_top, Set.mem_compl_image, compl_involutive, SimpleGraph.sdiff_compl_neighborFinset_inter_eq, SSet.horn₃₂.desc.multicofork_π_zero_assoc, Finset.sum_sum_Ioi_add_eq_sum_sum_off_diag, Finset.compl_eq_univ_iff, Fintype.sum_eq_sum_compl_add, SSet.horn.faceι_ι_assoc, compl_antitone, himp_eq, compl_strictAnti, sdiff_compl, Language.IsRegular.compl, SSet.horn.multicoequalizerDiagram, compl_himp_compl, DFA.acceptsFrom_compl, SSet.horn₃₁.desc.multicofork_π_three_assoc, Finset.subset_compl_comm, Finset.card_compl_lt_iff_nonempty, disjointed_eq_inf_compl, SSet.horn₃₁.desc.multicofork_π_zero, Language.compl_compl, SSet.stdSimplex.ofSimplex_yonedaEquiv_δ, symmDiff_symmDiff_right', Finset.mem_compls, SSet.horn₃₂.desc.multicofork_π_three, Affine.Simplex.mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter, Set.Intersecting.compl_notMem, compl_le_compl_iff_le, Finset.exists_compls_iff, IsCompl.compl_eq_iff, OrderIso.compl_apply, compl_eq_bot, top_le_sup_compl, Finset.coe_compls, SSet.stdSimplex.faceSingletonComplIso_hom_ι_assoc, Set.preimage_compl_eq_image_compl, compl_eq_iff_isCompl, IsAtom.compl, SSet.boundary_eq_iSup, isCompl_compl, Set.powersetCard.coe_mulActionHom_compl, Finset.isCoatom_iff, SSet.horn₃₂.desc.multicofork_pt, Finset.compl_truncatedInf, Affine.Simplex.excenterExists_compl, SimpleGraph.compl_neighborFinset_sdiff_inter_eq, compl_le_iff_compl_le, compl_eq_top, compl_bihimp_compl, BooleanSubalgebra.compl_mem, compl_sInf', compl_inj_iff, bihimp_eq', Fintype.sum_eq_add_sum_compl, Fin.image_succAbove_univ, Finset.prod_compl_mul_prod, Finset.subset_compl_iff_disjoint_left, Affine.Simplex.excenterWeightsUnnorm_compl, compl_eq_comm, compl_bihimp, SSet.horn₃₂.desc.multicofork_π_zero, SSet.horn₃₂.desc.multicofork_π_three_assoc, SSet.horn₃₂.desc.multicofork_π_one_assoc, compl_sup_eq_top, Fintype.not_linearIndependent_iffₒₛ, Affine.Simplex.excenter_compl, Finset.sum_add_sum_compl, Finset.image_compl, SSet.horn₃₁.desc.multicofork_π_three, Affine.Simplex.ExcenterExists.excenter_eq_excenter_iff, Finset.compl_subset_compl, Finset.sdiff_eq_inter_compl, Affine.Simplex.faceOppositeCentroid_eq_affineCombination, IsCoatom.compl, Affine.Simplex.excenterWeights_compl, ofBoolAlg_compl, isAtom_compl, Finset.compls_singleton, SSet.stdSimplex.face_singleton_compl, Finset.compl_eq_empty_iff, Finset.compl_truncatedSup, eq_compl_comm, Finset.subset_compl_iff_disjoint_right, Order.Ideal.IsPrime.mem_or_compl_mem, Finset.notMem_compl, Finset.insert_inj_on', Set.Finite.toFinset_compl
|
toDistribLattice 📖 | CompOp | 13 mathmath: sdiff_eq, himp_eq, inf_compl_le_bot, sdiff_eq, inf_compl_eq_bot', sup_compl_eq_top, toComplementedLattice, himp_eq, top_le_sup_compl, isCompl_compl, le_top, bot_le, compl_sup_eq_top
|
toHImp 📖 | CompOp | 63 mathmath: bihimp_left_involutive, bihimp_bihimp_cancel_right, bihimp_eq_left, codisjoint_bihimp_sup, inf_himp_bihimp, IsClopen.himp, compl_sdiff, Codisjoint.bihimp_right, bihimp_right_surjective, bihimp_himp_left, himp_eq, bihimp_eq_right, compl_symmDiff, himp_bihimp_left, bihimp_left_comm, Finset.inf_himp_right, bihimp_left_surjective, bihimp_le_iff_left, bihimp_le_iff_right, Topology.IsConstructible.himp, bihimp_bihimp_self, himp_le, MeasurableSet.bihimp, himp_le_left, bihimp_eq, bihimp_right_inj, bihimp_right_comm, himp_eq_left, MeasurableSet.himp, bihimp_iff_iff, Set.Definable.himp, MeasurableSet.coe_himp, Codisjoint.bihimp_left, compl_himp, Codisjoint.bihimp_inf_bihimp_le_right, himp_bihimp_right, bihimp_right_involutive, bihimp_eq_inf, himp_eq, TopologicalSpace.Clopens.coe_himp, compl_himp_compl, bihimp_left_inj, bihimp_left_injective, bihimp_bihimp_cancel_left, Codisjoint.bihimp_inf_bihimp_le_left, BooleanSubalgebra.mk_himp_mk, Finset.sup_himp_right, bihimp_bihimp_bihimp_comm, FirstOrder.Language.DefinableSet.coe_himp, codisjoint_himp_self_left, BooleanSubalgebra.val_himp, BooleanSubalgebra.himp_mem, compl_bihimp_compl, bihimp_eq', bihimp_isAssociative, compl_bihimp, codisjoint_himp_self_right, Finset.sup_himp_left, bihimp_himp_right, bihimp_assoc, TopologicalSpace.CompactOpens.coe_himp, bihimp_eq_bot, bihimp_right_injective
|
toSDiff 📖 | CompOp | 46 mathmath: map_symmDiff', BooleanSubalgebra.mk_sdiff_mk, compl_symmDiff_self, Filter.sdiff_limsup, ofBoolRing_sub, symmDiff_eq', symmDiff_compl_self, compl_sdiff, symmDiff_top, sdiff_eq, Disjoint.le_symmDiff_sup_symmDiff_right, top_symmDiff, biSup_symmDiff_biSup_le, compl_symmDiff, ofBoolRing_add, Heyting.Regular.coe_sdiff, compl_sdiff_compl, toBoolAlg_add, Filter.limsup_sdiff, sdiff_eq, symmDiff_eq, BooleanSubalgebra.sdiff_mem, Finset.inf_sdiff_right, ofBoolAlg_symmDiff, top_sdiff, BooleanSubalgebra.mem_closure_iff_sup_sdiff, Disjoint.le_symmDiff_sup_symmDiff_left, Filter.liminf_sdiff, ofBoolAlg_sdiff, compl_himp, compl_symmDiff_compl, sdiff_compl, Finset.sup_sdiff_left, symmDiff_eq_Xor', BooleanSubalgebra.val_sdiff, symmDiff_symmDiff_right', Bool.symmDiff_eq_xor, symmDiff_eq_top, MeasureTheory.ae_eq_set_symmDiff, Filter.sdiff_liminf, map_sdiff', Finset.inf_sdiff_left, MeasureTheory.ae_eq_set_diff, iSup_symmDiff_iSup_le, compl_bihimp, toBoolRing_symmDiff
|
toTop 📖 | CompOp | 262 mathmath: ofBoolRing_one, compl_symmDiff_self, SimplexCategoryGenRel.multiplicativeClosure_isGenerator_eq_top, CategoryTheory.MorphismProperty.comp_eq_top_iff, SimpleGraph.TopEdgeLabeling.labelGraph_adj, SSet.degenerate_eq_top_of_hasDimensionLT, bihimp_eq_left, CategoryTheory.MorphismProperty.DescendsAlong.top, CategoryTheory.MorphismProperty.Over.hasPullbacks, SimpleGraph.turanGraph_eq_top, CategoryTheory.MorphismProperty.Over.instHasTerminalTopOfContainsIdentities, SimpleGraph.isExtremal_top_free_iff_isTuranMaximal, symmDiff_compl_self, SimpleGraph.toTopEdgeLabeling_labelGraph_compl, CategoryTheory.ObjectProperty.topEquivalence_counitIso, SimpleGraph.edgeFinset_top, SimpleGraph.isClique_iff_induce_eq, CategoryTheory.MorphismProperty.Over.map_obj_left, CategoryTheory.MorphismProperty.Over.pullbackComp_hom_app_left, AlgebraicGeometry.Scheme.locallyCoverDense_of_le, BooleanSubalgebra.top_mem, CategoryTheory.MorphismProperty.Under.mk_hom, symmDiff_top, AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitMapWalkingSpanOverTopMorphismPropertySpan, SimpleGraph.Copy.topEmbedding_apply, BooleanSubalgebra.coe_bot, CategoryTheory.MorphismProperty.Over.mapCongr_inv_app_left, CategoryTheory.MorphismProperty.IsMultiplicative.instTop, CategoryTheory.MorphismProperty.Over.pullbackMapHomPullback_app, CategoryTheory.MorphismProperty.Over.mk_hom, CategoryTheory.MorphismProperty.Over.pullback_obj_left, CategoryTheory.MorphismProperty.Over.map_map_left, top_symmDiff, SSet.Subcomplex.degenerate_eq_top_iff, SSet.Truncated.HomotopyCategory.multiplicativeClosure_morphismPropertyHomMk, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap, SimpleGraph.chromaticNumber_top, CategoryTheory.Localization.Construction.morphismProperty_eq_top', bihimp_eq_right, CategoryTheory.MorphismProperty.Over.Hom.ext_iff, SimpleGraph.edgeSet_top, SimpleGraph.completeMultipartiteGraph.topEmbedding_apply_fst, Sym2.fromRel_top, CategoryTheory.Functor.isLeftAdjoint_iff_rightAdjointObjIsDefined_eq_top, SimpleGraph.support_top_of_nontrivial, SimpleGraph.neighborFinset_completeEquipartiteGraph, CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst, SimpleGraph.toTopEdgeLabeling_get, CategoryTheory.MorphismProperty.Over.mapPullbackAdj_counit_app, SimpleGraph.cycleGraph_two_eq_top, SimpleGraph.preconnected_iff_reachable_eq_top, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_f, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_pt, CategoryTheory.MorphismProperty.instRespectsIsoTop, CategoryTheory.MorphismProperty.instFaithfulOverTopOverForget, CategoryTheory.MorphismProperty.IsLocalAtSource.top, compl_lt_self, SimpleGraph.IsSRGWith.top, SimpleGraph.degree_completeEquipartiteGraph, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_id, CategoryTheory.MorphismProperty.Over.map_comp, CategoryTheory.MorphismProperty.Comma.instFullTopCommaForget, CategoryTheory.ObjectProperty.topEquivalence_unitIso, CategoryTheory.MorphismProperty.Over.instPreservesFiniteLimitsTopPullback, SimpleGraph.edist_top, SimpleGraph.cycleGraph_three_eq_top, CategoryTheory.Cat.FreeRefl.multiplicativeClosure_morphismPropertyHomMk, CategoryTheory.MorphismProperty.Over.mapPullbackAdj_unit_app, Digraph.toSimpleGraphStrict_top, Sylow.orbit_eq_top, CategoryTheory.MorphismProperty.Over.mapId_inv_app_left, Setoid.top_def, SSet.Truncated.liftOfStrictSegal.naturalityProperty_eq_top, SSet.hasDimensionLT_iff, SimpleGraph.preconnected_top, AlgebraicGeometry.instHasOfPostcompPropertySchemeQuasiSeparatedTopMorphismProperty, Matrix.toBlock_mul_eq_mul, CategoryTheory.MorphismProperty.Over.mapCongr_hom_app_left, CategoryTheory.MorphismProperty.IsLocalAtTarget.top, SimpleGraph.fromEdgeSet_not_isDiag, SSet.skeleton_obj_eq_top, SimpleGraph.ConnectedComponent.top_supp_eq_univ, Setoid.mk_eq_top, CategoryTheory.ObjectProperty.instIsSerreClassTop, SimpleGraph.chromaticNumber_eq_card_iff, SSet.stdSimplex.face_obj, CategoryTheory.ObjectProperty.instIsClosedUnderExtensionsTop, CategoryTheory.MorphismProperty.instIsStableUnderCobaseChangeTop, CategoryTheory.MorphismProperty.Over.forget_comp_forget_map, CategoryTheory.MorphismProperty.Over.pullbackComp_inv_app_left, SimpleGraph.extremalNumber_top, SimpleGraph.dist_top_of_ne, CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong, SimpleGraph.top_adj, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_ι_app, SimplexCategory.Truncated.morphismProperty_eq_top, SimpleGraph.card_edgeFinset_top_eq_card_choose_two, SimpleGraph.fromEdgeSet_univ, SimpleGraph.isExtremal_top_free_turanGraph, SimpleGraph.ediam_top, CategoryTheory.MorphismProperty.instHasOfPrecompPropertyTop, himp_le_left, Subgroup.closure_mul_image_mul_eq_top, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_X, CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.essentiallyLarge_top, SimpleGraph.top_isIndContained_iff_top_isContained, himp_eq_left, CategoryTheory.ObjectProperty.instContainsZeroTopOfHasZeroObject, SimpleGraph.ediam_eq_one, SimpleGraph.diam_eq_one, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_f, MvPolynomial.zeroLocus_bot, SimpleGraph.toTopEdgeLabeling_labelGraph, ContinuousMap.sublattice_closure_eq_top, top_sdiff, AlgebraicGeometry.Scheme.smallGrothendieckTopologyOfLE_eq_toGrothendieck_smallPretopology, CategoryTheory.MorphismProperty.instFullUnderTopUnderForget, CategoryTheory.Paths.morphismProperty_eq_top', Digraph.top_adj, CategoryTheory.Localization.Construction.morphismProperty_is_top', CategoryTheory.MorphismProperty.instIsLeftAdjointOverTopMapOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong, compl_le_self, CategoryTheory.MorphismProperty.Over.mapComp_hom_app_left, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap_assoc, CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop, CategoryTheory.MorphismProperty.Over.w_assoc, CategoryTheory.Localization.Construction.morphismProperty_eq_top, CategoryTheory.MorphismProperty.instHasOfPostcompPropertyTop, Quot.subsingleton_iff, CategoryTheory.Subfunctor.Subpresheaf.top_obj, CategoryTheory.exists_equivalence_iff_of_locallySmall, SimpleGraph.nonempty_dart_top, CategoryTheory.ObjectProperty.instEssentiallySmallTopOfEssentiallySmall, SimpleGraph.turanGraph_zero, CategoryTheory.MorphismProperty.instFaithfulCostructuredArrowTopOverToOver, CategoryTheory.MorphismProperty.CostructuredArrow.toOver_map, AlgebraicGeometry.instHasCoproductsOfShapeOverSchemeTopMorphismPropertyOfSmall, locallyFinsuppWithin.logCounting_divisor, CategoryTheory.MorphismProperty.CostructuredArrow.toOver_obj, CategoryTheory.MorphismProperty.Under.w, SimpleGraph.induce_singleton_eq_top, SimpleGraph.pathGraph_two_eq_top, sup_compl_eq_top, Set.eq_top_of_card_le_of_finite, CategoryTheory.MorphismProperty.Over.mk_left, SimpleGraph.cycleGraph_one_eq_top, CategoryTheory.MorphismProperty.CostructuredArrow.mk_left, Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const, CategoryTheory.ObjectProperty.ι_map_top, CategoryTheory.MorphismProperty.Under.Hom.ext_iff, SimpleGraph.isNClique_map_copy_top, CategoryTheory.ObjectProperty.IsLocal.top, CategoryTheory.MorphismProperty.Under.mk_left, BooleanSubalgebra.mk_top, CategoryTheory.ObjectProperty.instIsClosedUnderQuotientsTop, SSet.horn_obj_zero, SimpleGraph.diam_top, CategoryTheory.MorphismProperty.Over.instPreservesFiniteLimitsTopOverForget, ofBoolAlg_top, SimpleGraph.isClique_range_copy_top, CategoryTheory.MorphismProperty.Under.forget_comp_forget_map, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_X, CategoryTheory.MorphismProperty.instFullOverTopOverForget, SSet.skeletonOfMono_obj_eq_top, CategoryTheory.MorphismProperty.Comma.hasColimitsOfShape_of_closedUnderColimitsOfShape, SimpleGraph.eq_top_iff_forall_eccent_eq_one, CategoryTheory.MorphismProperty.Over.w, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans_app_left, Digraph.completeDigraph_eq_top, AlgebraicGeometry.Scheme.instLocallyCoverDenseOverTopMorphismPropertyOverForgetOverGrothendieckTopology, CategoryTheory.MorphismProperty.CodescendsAlong.top, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_comp, SimpleGraph.TopEdgeLabeling.labelGraph_toTopEdgeLabeling, CategoryTheory.Cat.FreeRefl.morphismProperty_eq_top, CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsTop, CategoryTheory.Paths.morphismProperty_eq_top_of_isMultiplicative, SimpleGraph.completeGraph_eq_top, SSet.HasDimensionLT.degenerate_eq_top, SimpleGraph.center_top, MeasurableSet.coe_top, AlgebraicGeometry.instHasOfPostcompPropertySchemeIsSeparatedTopMorphismProperty, CategoryTheory.MorphismProperty.Comma.hasColimit_of_closedUnderColimitsOfShape, CategoryTheory.IsCardinalFilteredGenerator.of_isDense, CategoryTheory.MorphismProperty.CostructuredArrow.Hom.ext_iff, AlgebraicGeometry.IsImmersion.instHasOfPostcompPropertySchemeTopMorphismProperty, SimpleGraph.completeMultipartiteGraph.topEmbedding_apply_snd, AlgebraicGeometry.Scheme.smallGrothendieckTopology_eq_toGrothendieck_smallPretopology, CategoryTheory.MorphismProperty.Over.pullback_map_left, SimpleGraph.chromaticNumber_top_eq_top_of_infinite, compl_eq_bot, top_le_sup_compl, BooleanSubalgebra.val_top, SimpleGraph.top_preconnected, CategoryTheory.Functor.isRightAdjoint_iff_leftAdjointObjIsDefined_eq_top, SimpleGraph.card_commonNeighbors_top, AlgebraicGeometry.instIsLocallyDirectedCompSchemeOverOverTopMorphismPropertyForgetForgetForget, symmDiff_eq_top, SimpleGraph.eq_top_iff_forall_ne_adj, CategoryTheory.MorphismProperty.Over.pullback_obj_hom, Digraph.toSimpleGraphInclusive_top, CategoryTheory.Subfunctor.top_obj, CategoryTheory.FreeGroupoid.instIsLocalizationOfTopMorphismProperty, CategoryTheory.MorphismProperty.instHasTwoOutOfThreePropertyTop, CategoryTheory.MorphismProperty.Over.mapComp_inv_app_left, CategoryTheory.Localization.morphismProperty_eq_top, SimpleGraph.radius_top, CategoryTheory.MorphismProperty.Under.w_assoc, CategoryTheory.MorphismProperty.instFullCostructuredArrowTopOverToOver, AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology, CategoryTheory.MorphismProperty.map_top_eq_top_of_essSurj_of_full, SimpleGraph.commonNeighbors_top_eq, CategoryTheory.MorphismProperty.instHasPullbackSndHomDiscretePUnitOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong, le_top, SimpleGraph.card_edgeFinset_completeEquipartiteGraph, compl_eq_top, RingCon.coe_top, SimpleGraph.eq_top_of_chromaticNumber_eq_card, essentiallySmall_of_le, PresheafOfModules.pullbackObjIsDefined_eq_top, AlgebraicGeometry.instMonoObjWalkingSpanCompOverSchemeTopMorphismPropertySpanOverForgetForgetForgetNoneWalkingPairSomeMapInitOfIsOpenImmersionLeftDiscretePUnit, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_map, CategoryTheory.ObjectProperty.instIsClosedUnderSubobjectsTop, Set.pairwise_top, CategoryTheory.ObjectProperty.topEquivalence_inverse, SimpleGraph.IsRegularOfDegree.top, CompactSpace.elim_nhds_subcover, CategoryTheory.ObjectProperty.topEquivalence_functor, SimpleGraph.Hom.injective_of_top_hom, toBoolRing_top, SimpleGraph.card_edgeFinset_eq_extremalNumber_top_iff_nonempty_iso_turanGraph, toBoolAlg_one, SimpleGraph.edist_top_of_ne, compl_sup_eq_top, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_obj, PMF.support_uniformOfFintype, AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology, CategoryTheory.MorphismProperty.Over.mapId_hom_app_left, CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fst, SimpleGraph.cliqueFree_iff_top_free, CategoryTheory.MorphismProperty.Comma.hasLimitsOfShape_of_closedUnderLimitsOfShape, Sym2.fromRel_top_iff, CategoryTheory.isGroupoid_iff_isomorphisms_eq_top, CategoryTheory.Localization.instIsGroupoidLocalizationTopMorphismProperty, irreducibleSpace_def, Submodule.IsPrimary.mem_or_mem, CategoryTheory.MorphismProperty.top_apply, AlgebraicGeometry.instHasFiniteCoproductsOverSchemeTopMorphismProperty, CategoryTheory.Localization.Construction.morphismProperty_is_top, SimpleGraph.card_topEdgeLabeling, SimpleGraph.cycleGraph_zero_eq_top, SSet.Truncated.HomotopyCategory.morphismProperty_eq_top, CategoryTheory.MorphismProperty.top_eq, CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst_assoc, BooleanSubalgebra.mem_bot, CategoryTheory.MorphismProperty.CostructuredArrow.mk_hom, CategoryTheory.Paths.morphismProperty_eq_top, SimpleGraph.dist_top, SimpleGraph.eccent_top, CategoryTheory.MorphismProperty.Comma.hasLimit_of_closedUnderLimitsOfShape, CategoryTheory.MorphismProperty.Over.map_obj_hom, CategoryTheory.MorphismProperty.instFaithfulUnderTopUnderForget, SimplexCategory.morphismProperty_eq_top
|