| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1184 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (23 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (224 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (34 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (405 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (33 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (56 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (96 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (299 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
Global Index
A
AC [definition, in Digraph.constructions.circulant]AC [section, in Digraph.constructions.circulant]
ACBase [section, in Digraph.applications.k5.acn_base]
ACBase.A [variable, in Digraph.applications.k5.acn_base]
ACBase.c1 [variable, in Digraph.applications.k5.acn_base]
ACBase.c2 [variable, in Digraph.applications.k5.acn_base]
ACBase.c3 [variable, in Digraph.applications.k5.acn_base]
ACBase.m' [variable, in Digraph.applications.k5.acn_base]
ACBase.N0 [variable, in Digraph.applications.k5.acn_base]
ACBase.qid [variable, in Digraph.applications.k5.acn_base]
ACBase.qidE [variable, in Digraph.applications.k5.acn_base]
ACBase.q0 [variable, in Digraph.applications.k5.acn_base]
ACBase.q0E [variable, in Digraph.applications.k5.acn_base]
ACBase.rid [variable, in Digraph.applications.k5.acn_base]
ACBase.r0 [variable, in Digraph.applications.k5.acn_base]
ACBase.shift [variable, in Digraph.applications.k5.acn_base]
ACBase.zeta [variable, in Digraph.applications.k5.acn_base]
ACBase.z0 [variable, in Digraph.applications.k5.acn_base]
ACdel [abbreviation, in Digraph.applications.k5.acn_base]
ACdel_pos [lemma, in Digraph.applications.k5.k5_lower]
ACdel_Ntransb [lemma, in Digraph.applications.k5.acn_base]
ACm [abbreviation, in Digraph.applications.k5.k5_lower]
ACm [abbreviation, in Digraph.applications.k5.k5_upper]
ACm [abbreviation, in Digraph.applications.k5.cells]
ACm [abbreviation, in Digraph.applications.k5.main]
ACm [abbreviation, in Digraph.applications.k5.acn_base]
ACm [abbreviation, in Digraph.applications.k4.k4_del]
ACm [abbreviation, in Digraph.applications.k4.k4_main]
ACm [abbreviation, in Digraph.applications.k4.k4_value]
ACm [abbreviation, in Digraph.applications.k5.obstructions]
ACm [abbreviation, in Digraph.applications.k4.k4_lower]
ACm [abbreviation, in Digraph.applications.k5.acn_arc_facts]
ACm_pos [lemma, in Digraph.applications.k5.k5_lower]
ACm_pos [lemma, in Digraph.applications.k4.k4_lower]
AcnBands [section, in Digraph.applications.acn_bands]
AcnBands.dbl_lt_addr [variable, in Digraph.applications.acn_bands]
AcnBands.lt_addl_pos [variable, in Digraph.applications.acn_bands]
AcnBands.m' [variable, in Digraph.applications.acn_bands]
acn_bands [library]
acn_arc_facts [library]
acn_base [library]
ACset [definition, in Digraph.constructions.circulant]
ACset_cond [lemma, in Digraph.constructions.circulant]
AC_kcritical3 [lemma, in Digraph.applications.k5.acn_base]
AC_del_uniform [lemma, in Digraph.invariants_advanced.transitive]
AC_mem_Lo_opp [lemma, in Digraph.applications.k5.acn_arc_facts]
AC_mem_Lo [lemma, in Digraph.applications.k5.acn_arc_facts]
AC_mem_Hi_opp [lemma, in Digraph.applications.k5.acn_arc_facts]
AC_mem_Hi [lemma, in Digraph.applications.k5.acn_arc_facts]
AC_band_arc [lemma, in Digraph.applications.k5.acn_arc_facts]
AC_arc_gt [lemma, in Digraph.applications.k5.acn_arc_facts]
AC_arc_lt [lemma, in Digraph.applications.k5.acn_arc_facts]
AC_mem_val [lemma, in Digraph.applications.k5.acn_arc_facts]
AC_wrapF [lemma, in Digraph.applications.acn_bands]
AC_vertex_transitive [lemma, in Digraph.constructions.circulant]
AC_arcE [lemma, in Digraph.constructions.circulant]
AC_total [lemma, in Digraph.constructions.circulant]
AC_irrefl [lemma, in Digraph.constructions.circulant]
AC.m' [variable, in Digraph.constructions.circulant]
AC.val_oppE [variable, in Digraph.constructions.circulant]
arc [definition, in Digraph.core.digraph]
arcC3E [lemma, in Digraph.core.tournament]
ArcFacts [section, in Digraph.applications.k5.acn_arc_facts]
ArcFacts.m' [variable, in Digraph.applications.k5.acn_arc_facts]
arcNarc [lemma, in Digraph.core.tournament]
arcTTE [lemma, in Digraph.core.tournament]
arcxx [lemma, in Digraph.core.tournament]
arc_pair_bound [lemma, in Digraph.core.oriented]
arc_asymm [definition, in Digraph.core.oriented]
arc_irrefl [definition, in Digraph.core.oriented]
arc_xorE [lemma, in Digraph.core.tournament]
arc_or [lemma, in Digraph.core.tournament]
arc_asym [lemma, in Digraph.core.tournament]
arc_neq [lemma, in Digraph.core.tournament]
arc_total [definition, in Digraph.core.tournament]
arc_closed [definition, in Digraph.invariants.strong]
autb [definition, in Digraph.constructions.automorphism]
autbP [lemma, in Digraph.constructions.automorphism]
autocorr_lo [lemma, in Digraph.applications.k5.acn_base]
autocorr_sym [lemma, in Digraph.applications.k5.acn_base]
autocorr2 [lemma, in Digraph.applications.k5.acn_base]
Automorphism [section, in Digraph.constructions.automorphism]
automorphism [library]
Automorphism.D [variable, in Digraph.constructions.automorphism]
B
backedge [definition, in Digraph.core.order]Backedge [section, in Digraph.core.order]
backedgeE [lemma, in Digraph.core.order]
backedge_qid_dist [lemma, in Digraph.applications.k5.acn_base]
backedge_arc_forward [lemma, in Digraph.core.order]
backedge_neq [lemma, in Digraph.core.order]
backedge_irrefl [lemma, in Digraph.core.order]
backedge_sym [lemma, in Digraph.core.order]
backedge_rel [definition, in Digraph.core.order]
Backedge.p [variable, in Digraph.core.order]
Backedge.T [variable, in Digraph.core.order]
band [definition, in Digraph.applications.acn_bands]
bands_neq [lemma, in Digraph.applications.k5.obstructions]
band_gap [lemma, in Digraph.applications.acn_bands]
band_le3 [lemma, in Digraph.applications.acn_bands]
band_ge1 [lemma, in Digraph.applications.acn_bands]
band1P [lemma, in Digraph.applications.acn_bands]
band12P [lemma, in Digraph.applications.acn_bands]
band2P [lemma, in Digraph.applications.acn_bands]
band3P [lemma, in Digraph.applications.acn_bands]
beatc [lemma, in Digraph.applications.k5.obstructions]
beat_inner [lemma, in Digraph.applications.k5.cells]
beat_blocks [lemma, in Digraph.applications.k5.cells]
beat_key [lemma, in Digraph.applications.k5.cells]
beat_innerD [lemma, in Digraph.applications.k4.k4_del]
beat_blocksD [lemma, in Digraph.applications.k4.k4_del]
beat_kd [lemma, in Digraph.applications.k4.k4_del]
beat_innerV [lemma, in Digraph.applications.k4.k4_value]
beat_blocksV [lemma, in Digraph.applications.k4.k4_value]
beat_kv [lemma, in Digraph.applications.k4.k4_value]
block_edgeE [lemma, in Digraph.invariants_advanced.substitution]
bucket_bound [lemma, in Digraph.applications.k5.acn_base]
Builders_1.Builders_Export_7 [module, in Digraph.core.tournament]
Builders_1.Builders_1_V__canonical__tournament_Tournament [definition, in Digraph.core.tournament]
Builders_1.HB_unnamed_factory_5 [definition, in Digraph.core.tournament]
Builders_1.Builders_1_V__canonical__oriented_Oriented [definition, in Digraph.core.tournament]
Builders_1.HB_unnamed_factory_3 [definition, in Digraph.core.tournament]
Builders_1.asymm [lemma, in Digraph.core.tournament]
Builders_1.arc_total [abbreviation, in Digraph.core.tournament]
Builders_1.arc_irrefl [abbreviation, in Digraph.core.tournament]
Builders_1.Builders_1.fresh_name_2 [variable, in Digraph.core.tournament]
Builders_1.Builders_1_V__canonical__digraph_DiGraph [definition, in Digraph.core.tournament]
Builders_1.Builders_1_V__canonical__fintype_Finite [definition, in Digraph.core.tournament]
Builders_1.Builders_1.local_mixin_fintype_isFinite [variable, in Digraph.core.tournament]
Builders_1.Builders_1_V__canonical__choice_Countable [definition, in Digraph.core.tournament]
Builders_1.Builders_1_V__canonical__choice_Choice [definition, in Digraph.core.tournament]
Builders_1.Builders_1_V__canonical__eqtype_Equality [definition, in Digraph.core.tournament]
Builders_1.Builders_1.local_mixin_eqtype_hasDecEq [variable, in Digraph.core.tournament]
Builders_1.Builders_1.local_mixin_choice_Choice_isCountable [variable, in Digraph.core.tournament]
Builders_1.Builders_1.local_mixin_choice_hasChoice [variable, in Digraph.core.tournament]
Builders_1.Builders_1_V__canonical__digraph_RelDigraph [definition, in Digraph.core.tournament]
Builders_1.Builders_1.local_mixin_digraph_HasArc [variable, in Digraph.core.tournament]
Builders_1.Builders_1.V [variable, in Digraph.core.tournament]
Builders_1.Builders_1.Builders_1 [section, in Digraph.core.tournament]
Builders_1.Super [module, in Digraph.core.tournament]
Builders_1 [module, in Digraph.core.tournament]
C
cardA [lemma, in Digraph.applications.k5.acn_base]cardN0 [lemma, in Digraph.applications.k5.acn_base]
card_TT [lemma, in Digraph.core.tournament]
card_C3 [lemma, in Digraph.core.tournament]
card_le2_transb [lemma, in Digraph.core.tournament]
card_lexprod [lemma, in Digraph.constructions.product]
card_clique_cidx [lemma, in Digraph.applications.k5.cells]
card_T5 [lemma, in Digraph.applications.k5.main]
card_shift [lemma, in Digraph.applications.k5.acn_base]
card_del [lemma, in Digraph.invariants.critical]
card_clique_didx [lemma, in Digraph.applications.k4.k4_del]
card_T4 [lemma, in Digraph.applications.k4.k4_main]
card_ord_seg [lemma, in Digraph.applications.ck3.lemma7]
card_ord_ltn [lemma, in Digraph.applications.ck3.lemma7]
card_clique_sidx [lemma, in Digraph.applications.k4.k4_value]
card_classes_inj [lemma, in Digraph.foundations.prelude]
card_classes [lemma, in Digraph.foundations.prelude]
card_AC [lemma, in Digraph.constructions.circulant]
cat_dipath_cont [lemma, in Digraph.core.dipath]
cat_dipath [lemma, in Digraph.core.dipath]
Cayley [section, in Digraph.constructions.cayley]
cayley [definition, in Digraph.constructions.cayley]
cayley [library]
cayley_vertex_transitive [lemma, in Digraph.constructions.cayley]
cayley_totalP [lemma, in Digraph.constructions.cayley]
cayley_irreflP [lemma, in Digraph.constructions.cayley]
cayley_arcE [lemma, in Digraph.constructions.cayley]
cayley_cayley__canonical__digraph_DiGraph [definition, in Digraph.constructions.cayley]
cayley_cayley__canonical__digraph_RelDigraph [definition, in Digraph.constructions.cayley]
cayley_cayley__canonical__fintype_Finite [definition, in Digraph.constructions.cayley]
cayley_cayley__canonical__choice_Countable [definition, in Digraph.constructions.cayley]
cayley_cayley__canonical__choice_Choice [definition, in Digraph.constructions.cayley]
cayley_cayley__canonical__eqtype_Equality [definition, in Digraph.constructions.cayley]
cayley_cayley__canonical__tournament_Tournament [definition, in Digraph.constructions.circulant]
cayley_cayley__canonical__oriented_Oriented [definition, in Digraph.constructions.circulant]
Cayley.A [variable, in Digraph.constructions.cayley]
Cayley.gT [variable, in Digraph.constructions.cayley]
Cells [section, in Digraph.applications.k5.cells]
cells [library]
Cells.InClique [section, in Digraph.applications.k5.cells]
Cells.InClique.K [variable, in Digraph.applications.k5.cells]
Cells.InClique.Kcl [variable, in Digraph.applications.k5.cells]
Cells.m' [variable, in Digraph.applications.k5.cells]
cidx [definition, in Digraph.applications.k5.cells]
cidx_inj_clique [lemma, in Digraph.applications.k5.cells]
cidx_mono [lemma, in Digraph.applications.k5.cells]
cidx_le8 [lemma, in Digraph.applications.k5.cells]
cidx_decode [lemma, in Digraph.applications.k5.cells]
circulant [library]
circulant_arcE [lemma, in Digraph.constructions.circulant]
ckB [definition, in Digraph.applications.ck3.lemma7]
ckC [definition, in Digraph.applications.ck3.lemma7]
ckCset [definition, in Digraph.applications.ck3.lemma7]
CKDefs [section, in Digraph.applications.ck3.lemma7]
CKDefs.D [variable, in Digraph.applications.ck3.lemma7]
ckS [definition, in Digraph.applications.ck3.lemma7]
ck_conj1_at_3 [lemma, in Digraph.applications.ck3.ck3_main]
ck_conj1_delta3_path [lemma, in Digraph.applications.ck3.ck3_main]
ck_conj1_delta3 [lemma, in Digraph.applications.ck3.ck3_main]
ck_conj1_delta2 [lemma, in Digraph.applications.ck3.lemma7]
ck_theorem4_oriented [lemma, in Digraph.applications.ck3.lemma7]
ck3_main [library]
clique_card_le3 [lemma, in Digraph.applications.k4.k4_del]
clique_card_le4 [lemma, in Digraph.applications.k4.k4_value]
clique_set1 [lemma, in Digraph.foundations.interop_graph_theory]
closed_connect [lemma, in Digraph.invariants.strong]
conjecture_5_10_at_k5 [lemma, in Digraph.applications.k5.main]
conjecture_5_10_at_345 [lemma, in Digraph.applications.unified]
conjecture_5_10_at_k3 [lemma, in Digraph.applications.unified]
conjecture_5_10_at_k4 [lemma, in Digraph.applications.k4.k4_main]
connect_cross [lemma, in Digraph.invariants.strong]
connect_induced_closed [lemma, in Digraph.invariants.strong]
converse [definition, in Digraph.core.digraph]
converse_arcE [lemma, in Digraph.core.digraph]
coverage [library]
coverage5 [lemma, in Digraph.applications.k5.coverage]
critical [library]
cross_edgeE [lemma, in Digraph.invariants_advanced.substitution]
C3 [definition, in Digraph.core.tournament]
C3 [section, in Digraph.core.tournament]
C3t [abbreviation, in Digraph.applications.k4.k4_del]
C3t [abbreviation, in Digraph.applications.k4.k4_main]
C3t [abbreviation, in Digraph.applications.k4.k4_value]
C3t [abbreviation, in Digraph.applications.k4.k4_lower]
C3_Ntransb [lemma, in Digraph.core.tournament]
C3_total [lemma, in Digraph.core.tournament]
C3_irrefl [lemma, in Digraph.core.tournament]
C3_kcritical2 [lemma, in Digraph.invariants.critical]
C3_pos [lemma, in Digraph.applications.k4.k4_lower]
C3_vertex_transitive [lemma, in Digraph.constructions.circulant]
D
dband [definition, in Digraph.applications.k4.k4_value]dband_le2 [lemma, in Digraph.applications.k4.k4_value]
dband_ge1 [lemma, in Digraph.applications.k4.k4_value]
dband1P [lemma, in Digraph.applications.k4.k4_value]
dband2P [lemma, in Digraph.applications.k4.k4_value]
del_tournament [definition, in Digraph.core.tournament]
del_aut_iso [lemma, in Digraph.invariants_advanced.transitive]
del_vertex [definition, in Digraph.core.digraph]
dgaut [definition, in Digraph.constructions.automorphism]
dgautE [lemma, in Digraph.constructions.automorphism]
dgautM [lemma, in Digraph.constructions.automorphism]
dgaut_group [definition, in Digraph.constructions.automorphism]
dgaut_group_set [lemma, in Digraph.constructions.automorphism]
dgaut1 [lemma, in Digraph.constructions.automorphism]
dgiso [definition, in Digraph.core.digraph]
dgiso_card [lemma, in Digraph.core.digraph]
dgiso_trans [lemma, in Digraph.core.digraph]
dgiso_sym [lemma, in Digraph.core.digraph]
dgiso_refl [lemma, in Digraph.core.digraph]
dicycle [definition, in Digraph.core.dipath]
dicycle_suffix [lemma, in Digraph.core.dipath]
dicycle_unroll [lemma, in Digraph.core.dipath]
dicycle_prev [lemma, in Digraph.core.dipath]
dicycle_next [lemma, in Digraph.core.dipath]
dicycle_rot [lemma, in Digraph.core.dipath]
didx_inj_clique [lemma, in Digraph.applications.k4.k4_del]
DiGraph [abbreviation, in Digraph.core.digraph]
DiGraph [module, in Digraph.core.digraph]
digraph [library]
DiGraphElpiOperations [module, in Digraph.core.digraph]
DiGraph_IsOriented [abbreviation, in Digraph.core.oriented]
DiGraph_IsOriented.Exports [module, in Digraph.core.oriented]
DiGraph_IsOriented.identity_builder [definition, in Digraph.core.oriented]
DiGraph_IsOriented.axioms [abbreviation, in Digraph.core.oriented]
DiGraph_IsOriented.phant_axioms [definition, in Digraph.core.oriented]
DiGraph_IsOriented.Build [abbreviation, in Digraph.core.oriented]
DiGraph_IsOriented.phant_Build [definition, in Digraph.core.oriented]
DiGraph_IsOriented.arc_asymm [projection, in Digraph.core.oriented]
DiGraph_IsOriented.arc_irrefl [projection, in Digraph.core.oriented]
DiGraph_IsOriented.axioms_ [record, in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented_V__canonical__digraph_DiGraph [definition, in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented_V__canonical__fintype_Finite [definition, in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented.local_mixin_fintype_isFinite [variable, in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented_V__canonical__choice_Countable [definition, in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented_V__canonical__choice_Choice [definition, in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented_V__canonical__eqtype_Equality [definition, in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented.local_mixin_eqtype_hasDecEq [variable, in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented.local_mixin_choice_Choice_isCountable [variable, in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented.local_mixin_choice_hasChoice [variable, in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented_V__canonical__digraph_RelDigraph [definition, in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented.local_mixin_digraph_HasArc [variable, in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented.V [variable, in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented.DiGraph_IsOriented [section, in Digraph.core.oriented]
DiGraph_IsOriented [module, in Digraph.core.oriented]
DiGraph_IsTournament [abbreviation, in Digraph.core.tournament]
DiGraph_IsTournament.Exports [module, in Digraph.core.tournament]
DiGraph_IsTournament.axioms [abbreviation, in Digraph.core.tournament]
DiGraph_IsTournament.phant_axioms [definition, in Digraph.core.tournament]
DiGraph_IsTournament.Build [abbreviation, in Digraph.core.tournament]
DiGraph_IsTournament.phant_Build [definition, in Digraph.core.tournament]
DiGraph_IsTournament.arc_total [projection, in Digraph.core.tournament]
DiGraph_IsTournament.arc_irrefl [projection, in Digraph.core.tournament]
DiGraph_IsTournament.axioms_ [record, in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament_V__canonical__digraph_DiGraph [definition, in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament_V__canonical__fintype_Finite [definition, in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament.local_mixin_fintype_isFinite [variable, in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament_V__canonical__choice_Countable [definition, in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament_V__canonical__choice_Choice [definition, in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament_V__canonical__eqtype_Equality [definition, in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament.local_mixin_eqtype_hasDecEq [variable, in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament.local_mixin_choice_Choice_isCountable [variable, in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament.local_mixin_choice_hasChoice [variable, in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament_V__canonical__digraph_RelDigraph [definition, in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament.local_mixin_digraph_HasArc [variable, in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament.V [variable, in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament.DiGraph_IsTournament [section, in Digraph.core.tournament]
DiGraph_IsTournament [module, in Digraph.core.tournament]
digraph_converse__canonical__digraph_DiGraph [definition, in Digraph.core.digraph]
digraph_converse__canonical__digraph_RelDigraph [definition, in Digraph.core.digraph]
digraph_converse__canonical__fintype_Finite [definition, in Digraph.core.digraph]
digraph_converse__canonical__choice_Countable [definition, in Digraph.core.digraph]
digraph_converse__canonical__choice_Choice [definition, in Digraph.core.digraph]
digraph_converse__canonical__eqtype_Equality [definition, in Digraph.core.digraph]
DiGraph.axioms_ [record, in Digraph.core.digraph]
DiGraph.choice_Choice_isCountable_mixin [projection, in Digraph.core.digraph]
DiGraph.choice_hasChoice_mixin [projection, in Digraph.core.digraph]
DiGraph.class [projection, in Digraph.core.digraph]
DiGraph.clone [abbreviation, in Digraph.core.digraph]
DiGraph.copy [abbreviation, in Digraph.core.digraph]
DiGraph.digraph_HasArc_mixin [projection, in Digraph.core.digraph]
DiGraph.eqtype_hasDecEq_mixin [projection, in Digraph.core.digraph]
DiGraph.Exports [module, in Digraph.core.digraph]
DiGraph.Exports.diGraphType [abbreviation, in Digraph.core.digraph]
DiGraph.Exports.digraph_DiGraph__to__fintype_Finite [definition, in Digraph.core.digraph]
DiGraph.Exports.digraph_DiGraph_class__to__fintype_Finite_class [definition, in Digraph.core.digraph]
DiGraph.Exports.digraph_DiGraph__to__choice_Countable [definition, in Digraph.core.digraph]
DiGraph.Exports.digraph_DiGraph_class__to__choice_Countable_class [definition, in Digraph.core.digraph]
DiGraph.Exports.digraph_DiGraph__to__choice_Choice [definition, in Digraph.core.digraph]
DiGraph.Exports.digraph_DiGraph_class__to__choice_Choice_class [definition, in Digraph.core.digraph]
DiGraph.Exports.digraph_DiGraph__to__eqtype_Equality [definition, in Digraph.core.digraph]
DiGraph.Exports.digraph_DiGraph_class__to__eqtype_Equality_class [definition, in Digraph.core.digraph]
DiGraph.Exports.digraph_DiGraph__to__digraph_RelDigraph [definition, in Digraph.core.digraph]
DiGraph.Exports.digraph_DiGraph_class__to__digraph_RelDigraph_class [definition, in Digraph.core.digraph]
DiGraph.Exports.join_digraph_DiGraph_between_fintype_Finite_and_digraph_RelDigraph [definition, in Digraph.core.digraph]
DiGraph.Exports.join_digraph_DiGraph_between_choice_Countable_and_digraph_RelDigraph [definition, in Digraph.core.digraph]
DiGraph.Exports.join_digraph_DiGraph_between_choice_Choice_and_digraph_RelDigraph [definition, in Digraph.core.digraph]
DiGraph.Exports.join_digraph_DiGraph_between_eqtype_Equality_and_digraph_RelDigraph [definition, in Digraph.core.digraph]
DiGraph.fintype_isFinite_mixin [projection, in Digraph.core.digraph]
DiGraph.on [abbreviation, in Digraph.core.digraph]
DiGraph.on_ [abbreviation, in Digraph.core.digraph]
DiGraph.pack_ [definition, in Digraph.core.digraph]
DiGraph.phant_on_ [definition, in Digraph.core.digraph]
DiGraph.phant_clone [definition, in Digraph.core.digraph]
DiGraph.sort [projection, in Digraph.core.digraph]
DiGraph.type [record, in Digraph.core.digraph]
dipath [definition, in Digraph.core.dipath]
dipath [library]
DiPathDef [section, in Digraph.core.dipath]
DiPathDef.D [variable, in Digraph.core.dipath]
dipath_map [lemma, in Digraph.core.dipath]
dipath_size [lemma, in Digraph.core.dipath]
dipath_arc_nth [lemma, in Digraph.core.dipath]
dipath_take [lemma, in Digraph.core.dipath]
dipath_drop [lemma, in Digraph.core.dipath]
dipath_cons [lemma, in Digraph.core.dipath]
dipath_rcons [lemma, in Digraph.core.dipath]
dipath_nil [lemma, in Digraph.core.dipath]
dipath_uniq [lemma, in Digraph.core.dipath]
dipath_path [lemma, in Digraph.core.dipath]
disjoint_cycles_path [lemma, in Digraph.invariants.strong]
dominatesb [definition, in Digraph.invariants.domination]
dominatesbP [lemma, in Digraph.invariants.domination]
dominatesb_setT [lemma, in Digraph.invariants.domination]
Domination [section, in Digraph.invariants.domination]
domination [library]
Domination.T [variable, in Digraph.invariants.domination]
domnum [definition, in Digraph.invariants.domination]
domnum_AC_ge3 [lemma, in Digraph.applications.k5.acn_base]
domnum_le_omegabar [lemma, in Digraph.invariants.domination]
domnum_witness [lemma, in Digraph.invariants.domination]
domnum_min [lemma, in Digraph.invariants.domination]
E
ell [definition, in Digraph.core.dipath]ellP [lemma, in Digraph.core.dipath]
ell_induced [lemma, in Digraph.core.dipath]
ell_outsel [lemma, in Digraph.core.dipath]
ell_embed [lemma, in Digraph.core.dipath]
ell_max [lemma, in Digraph.core.dipath]
emb_mem [lemma, in Digraph.applications.k5.k5_lower]
emb_mem [lemma, in Digraph.applications.k4.k4_lower]
endmax [definition, in Digraph.core.dipath]
endmax_ex [lemma, in Digraph.core.dipath]
endmax_dipath [lemma, in Digraph.core.dipath]
endmax_closure [lemma, in Digraph.core.dipath]
F
fintype_Finite__to__fintype_isFinite [definition, in Digraph.core.oriented]fintype_Finite__to__eqtype_hasDecEq [definition, in Digraph.core.oriented]
fintype_Finite__to__choice_Choice_isCountable [definition, in Digraph.core.oriented]
fintype_Finite__to__choice_hasChoice [definition, in Digraph.core.oriented]
fintype_Finite__to__fintype_isFinite__34 [definition, in Digraph.core.tournament]
fintype_Finite__to__eqtype_hasDecEq__32 [definition, in Digraph.core.tournament]
fintype_Finite__to__choice_Choice_isCountable__30 [definition, in Digraph.core.tournament]
fintype_Finite__to__choice_hasChoice__28 [definition, in Digraph.core.tournament]
fintype_Finite__to__fintype_isFinite [definition, in Digraph.core.tournament]
fintype_Finite__to__eqtype_hasDecEq [definition, in Digraph.core.tournament]
fintype_Finite__to__choice_Choice_isCountable [definition, in Digraph.core.tournament]
fintype_Finite__to__choice_hasChoice [definition, in Digraph.core.tournament]
fintype_Finite__to__fintype_isFinite [definition, in Digraph.constructions.product]
fintype_Finite__to__eqtype_hasDecEq [definition, in Digraph.constructions.product]
fintype_Finite__to__choice_Choice_isCountable [definition, in Digraph.constructions.product]
fintype_Finite__to__choice_hasChoice [definition, in Digraph.constructions.product]
fintype_Finite__to__fintype_isFinite [definition, in Digraph.constructions.cayley]
fintype_Finite__to__eqtype_hasDecEq [definition, in Digraph.constructions.cayley]
fintype_Finite__to__choice_Choice_isCountable [definition, in Digraph.constructions.cayley]
fintype_Finite__to__choice_hasChoice [definition, in Digraph.constructions.cayley]
fintype_Finite__to__fintype_isFinite [definition, in Digraph.core.digraph]
fintype_Finite__to__eqtype_hasDecEq [definition, in Digraph.core.digraph]
fintype_Finite__to__choice_Choice_isCountable [definition, in Digraph.core.digraph]
fintype_Finite__to__choice_hasChoice [definition, in Digraph.core.digraph]
f_arc [lemma, in Digraph.applications.k5.k5_lower]
f_inj [lemma, in Digraph.applications.k5.k5_lower]
f_arc [lemma, in Digraph.applications.k4.k4_lower]
f_inj [lemma, in Digraph.applications.k4.k4_lower]
G
greedy_clique_dom [lemma, in Digraph.invariants.domination]gval_bounds [lemma, in Digraph.applications.k5.in_neighbourhood]
H
HasArc [abbreviation, in Digraph.core.digraph]HasArc [module, in Digraph.core.digraph]
HasArc.arc [projection, in Digraph.core.digraph]
HasArc.axioms [abbreviation, in Digraph.core.digraph]
HasArc.axioms_ [record, in Digraph.core.digraph]
HasArc.Build [abbreviation, in Digraph.core.digraph]
HasArc.Exports [module, in Digraph.core.digraph]
HasArc.HasArc.HasArc [section, in Digraph.core.digraph]
HasArc.HasArc.V [variable, in Digraph.core.digraph]
HasArc.identity_builder [definition, in Digraph.core.digraph]
HasArc.phant_axioms [definition, in Digraph.core.digraph]
HasArc.phant_Build [definition, in Digraph.core.digraph]
has_dipathP [lemma, in Digraph.core.dipath]
has_dipath [definition, in Digraph.core.dipath]
HB_unnamed_factory_14 [definition, in Digraph.core.oriented]
HB_unnamed_factory_12 [definition, in Digraph.core.oriented]
HB_unnamed_mixin_11 [definition, in Digraph.core.oriented]
HB_unnamed_mixin_10 [definition, in Digraph.core.oriented]
HB_unnamed_mixin_9 [definition, in Digraph.core.oriented]
HB_unnamed_mixin_8 [definition, in Digraph.core.oriented]
HB_unnamed_factory_3 [definition, in Digraph.core.oriented]
HB_unnamed_factory_1 [definition, in Digraph.core.oriented]
HB_unnamed_mixin_47 [definition, in Digraph.core.tournament]
HB_unnamed_mixin_46 [definition, in Digraph.core.tournament]
HB_unnamed_factory_41 [definition, in Digraph.core.tournament]
HB_unnamed_factory_39 [definition, in Digraph.core.tournament]
HB_unnamed_mixin_38 [definition, in Digraph.core.tournament]
HB_unnamed_mixin_37 [definition, in Digraph.core.tournament]
HB_unnamed_mixin_36 [definition, in Digraph.core.tournament]
HB_unnamed_mixin_35 [definition, in Digraph.core.tournament]
HB_unnamed_factory_26 [definition, in Digraph.core.tournament]
HB_unnamed_mixin_25 [definition, in Digraph.core.tournament]
HB_unnamed_mixin_24 [definition, in Digraph.core.tournament]
HB_unnamed_factory_21 [definition, in Digraph.core.tournament]
HB_unnamed_factory_19 [definition, in Digraph.core.tournament]
HB_unnamed_mixin_18 [definition, in Digraph.core.tournament]
HB_unnamed_mixin_17 [definition, in Digraph.core.tournament]
HB_unnamed_mixin_16 [definition, in Digraph.core.tournament]
HB_unnamed_mixin_15 [definition, in Digraph.core.tournament]
HB_unnamed_factory_10 [definition, in Digraph.core.tournament]
HB_unnamed_factory_8 [definition, in Digraph.core.tournament]
HB_unnamed_mixin_16 [definition, in Digraph.constructions.product]
HB_unnamed_mixin_15 [definition, in Digraph.constructions.product]
HB_unnamed_factory_12 [definition, in Digraph.constructions.product]
HB_unnamed_factory_10 [definition, in Digraph.constructions.product]
HB_unnamed_mixin_9 [definition, in Digraph.constructions.product]
HB_unnamed_mixin_8 [definition, in Digraph.constructions.product]
HB_unnamed_mixin_7 [definition, in Digraph.constructions.product]
HB_unnamed_mixin_6 [definition, in Digraph.constructions.product]
HB_unnamed_factory_1 [definition, in Digraph.constructions.product]
HB_unnamed_factory_10 [definition, in Digraph.constructions.cayley]
HB_unnamed_mixin_9 [definition, in Digraph.constructions.cayley]
HB_unnamed_mixin_8 [definition, in Digraph.constructions.cayley]
HB_unnamed_mixin_7 [definition, in Digraph.constructions.cayley]
HB_unnamed_mixin_6 [definition, in Digraph.constructions.cayley]
HB_unnamed_factory_1 [definition, in Digraph.constructions.cayley]
HB_unnamed_factory_14 [definition, in Digraph.core.digraph]
HB_unnamed_factory_12 [definition, in Digraph.core.digraph]
hb_instance_11.D [variable, in Digraph.core.digraph]
hb_instance_11.hb_instance_11 [section, in Digraph.core.digraph]
HB_unnamed_mixin_10 [definition, in Digraph.core.digraph]
HB_unnamed_mixin_9 [definition, in Digraph.core.digraph]
HB_unnamed_mixin_8 [definition, in Digraph.core.digraph]
HB_unnamed_mixin_7 [definition, in Digraph.core.digraph]
HB_unnamed_factory_2 [definition, in Digraph.core.digraph]
hb_instance_1.D [variable, in Digraph.core.digraph]
hb_instance_1.hb_instance_1 [section, in Digraph.core.digraph]
HB_unnamed_mixin_5 [definition, in Digraph.constructions.circulant]
HB_unnamed_mixin_4 [definition, in Digraph.constructions.circulant]
HB_unnamed_factory_1 [definition, in Digraph.constructions.circulant]
hmin [definition, in Digraph.invariants_advanced.substitution]
H17 [section, in Digraph.applications.k5.in_neighbourhood]
H17_no_mixed [lemma, in Digraph.applications.k5.in_neighbourhood]
H17_side [lemma, in Digraph.applications.k5.in_neighbourhood]
H17_dichot [lemma, in Digraph.applications.k5.in_neighbourhood]
H17_xrange [lemma, in Digraph.applications.k5.in_neighbourhood]
H17.m' [variable, in Digraph.applications.k5.in_neighbourhood]
I
induced_oriented [definition, in Digraph.core.oriented]induced_digraph [definition, in Digraph.core.digraph]
interop_graph_theory [library]
in_neighbourhood [library]
K
kappa [definition, in Digraph.applications.k4.k4_value]kappa_sidx [lemma, in Digraph.applications.k4.k4_value]
kcritical [definition, in Digraph.invariants.critical]
kcriticalP [lemma, in Digraph.invariants.critical]
kcritical_proper_sub [lemma, in Digraph.invariants.critical]
kcritical2_uniq [lemma, in Digraph.invariants.critical]
kcritical2_card3 [lemma, in Digraph.invariants.critical]
kd [definition, in Digraph.applications.k4.k4_del]
kd_samesidx [lemma, in Digraph.applications.k4.k4_del]
kd_sidx_mono [lemma, in Digraph.applications.k4.k4_del]
kd_inj [lemma, in Digraph.applications.k4.k4_del]
Kernel [section, in Digraph.applications.ck3.lemma7]
kernel_S [lemma, in Digraph.applications.ck3.lemma7]
kernel_full [lemma, in Digraph.applications.ck3.lemma7]
Kernel.a [variable, in Digraph.applications.ck3.lemma7]
Kernel.AB_part [variable, in Digraph.applications.ck3.lemma7]
Kernel.aE [variable, in Digraph.applications.ck3.lemma7]
Kernel.aidx [variable, in Digraph.applications.ck3.lemma7]
Kernel.arc_w_a [variable, in Digraph.applications.ck3.lemma7]
Kernel.arc_y_a [variable, in Digraph.applications.ck3.lemma7]
Kernel.Aset [variable, in Digraph.applications.ck3.lemma7]
Kernel.A_le [variable, in Digraph.applications.ck3.lemma7]
Kernel.a_le [variable, in Digraph.applications.ck3.lemma7]
Kernel.a_ge1 [variable, in Digraph.applications.ck3.lemma7]
Kernel.a_min [variable, in Digraph.applications.ck3.lemma7]
Kernel.a_lt [variable, in Digraph.applications.ck3.lemma7]
Kernel.Bset [variable, in Digraph.applications.ck3.lemma7]
Kernel.BsetE [variable, in Digraph.applications.ck3.lemma7]
Kernel.claim11 [variable, in Digraph.applications.ck3.lemma7]
Kernel.claim12 [variable, in Digraph.applications.ck3.lemma7]
Kernel.countA [variable, in Digraph.applications.ck3.lemma7]
Kernel.countB [variable, in Digraph.applications.ck3.lemma7]
Kernel.Cs [variable, in Digraph.applications.ck3.lemma7]
Kernel.CsE [variable, in Digraph.applications.ck3.lemma7]
Kernel.dcC [variable, in Digraph.applications.ck3.lemma7]
Kernel.delta [variable, in Digraph.applications.ck3.lemma7]
Kernel.endclosure [variable, in Digraph.applications.ck3.lemma7]
Kernel.exMP [variable, in Digraph.applications.ck3.lemma7]
Kernel.H [variable, in Digraph.applications.ck3.lemma7]
Kernel.has_back [variable, in Digraph.applications.ck3.lemma7]
Kernel.Hd [variable, in Digraph.applications.ck3.lemma7]
Kernel.Hell [variable, in Digraph.applications.ck3.lemma7]
Kernel.Hn [variable, in Digraph.applications.ck3.lemma7]
Kernel.Hreg [variable, in Digraph.applications.ck3.lemma7]
Kernel.Hstr [variable, in Digraph.applications.ck3.lemma7]
Kernel.isMP [variable, in Digraph.applications.ck3.lemma7]
Kernel.mptype [variable, in Digraph.applications.ck3.lemma7]
Kernel.mp0 [variable, in Digraph.applications.ck3.lemma7]
Kernel.nbig [variable, in Digraph.applications.ck3.lemma7]
Kernel.prefC [variable, in Digraph.applications.ck3.lemma7]
Kernel.ps [variable, in Digraph.applications.ck3.lemma7]
Kernel.pstar [variable, in Digraph.applications.ck3.lemma7]
Kernel.pstarMP [variable, in Digraph.applications.ck3.lemma7]
Kernel.pstar_min [variable, in Digraph.applications.ck3.lemma7]
Kernel.s [variable, in Digraph.applications.ck3.lemma7]
Kernel.sL [variable, in Digraph.applications.ck3.lemma7]
Kernel.Sset [variable, in Digraph.applications.ck3.lemma7]
Kernel.szC [variable, in Digraph.applications.ck3.lemma7]
Kernel.S_sub_C [variable, in Digraph.applications.ck3.lemma7]
Kernel.S_card [variable, in Digraph.applications.ck3.lemma7]
Kernel.uC [variable, in Digraph.applications.ck3.lemma7]
Kernel.uP [variable, in Digraph.applications.ck3.lemma7]
Kernel.va_B [variable, in Digraph.applications.ck3.lemma7]
Kernel.w [variable, in Digraph.applications.ck3.lemma7]
Kernel.wP [variable, in Digraph.applications.ck3.lemma7]
Kernel.x [variable, in Digraph.applications.ck3.lemma7]
Kernel.y [variable, in Digraph.applications.ck3.lemma7]
Kernel.yS [variable, in Digraph.applications.ck3.lemma7]
key [definition, in Digraph.applications.k5.cells]
key_samecell [lemma, in Digraph.applications.k5.cells]
key_inj [lemma, in Digraph.applications.k5.cells]
ksel [definition, in Digraph.core.oriented]
KSelection [section, in Digraph.core.oriented]
KSelection.D [variable, in Digraph.core.oriented]
KSelection.k [variable, in Digraph.core.oriented]
ksel_card [lemma, in Digraph.core.oriented]
ksel_sub [lemma, in Digraph.core.oriented]
kv [definition, in Digraph.applications.k4.k4_value]
kv_samekappa [lemma, in Digraph.applications.k4.k4_value]
kv_lt_t [lemma, in Digraph.applications.k4.k4_value]
kv_kappa_mono [lemma, in Digraph.applications.k4.k4_value]
kv_inj [lemma, in Digraph.applications.k4.k4_value]
K2 [definition, in Digraph.foundations.interop_graph_theory]
K2_irrefl [lemma, in Digraph.foundations.interop_graph_theory]
K2_sym [lemma, in Digraph.foundations.interop_graph_theory]
K2_rel [definition, in Digraph.foundations.interop_graph_theory]
K4Del [section, in Digraph.applications.k4.k4_del]
K4Del.bool_finalD [variable, in Digraph.applications.k4.k4_del]
K4Del.hz [variable, in Digraph.applications.k4.k4_del]
K4Del.InCliqueD [section, in Digraph.applications.k4.k4_del]
K4Del.InCliqueD.K [variable, in Digraph.applications.k4.k4_del]
K4Del.InCliqueD.Kcl [variable, in Digraph.applications.k4.k4_del]
K4Del.InCliqueD.sum5 [variable, in Digraph.applications.k4.k4_del]
K4Del.m' [variable, in Digraph.applications.k4.k4_del]
K4Del.m3 [variable, in Digraph.applications.k4.k4_del]
K4Del.n_sub_ltm_gtSm [variable, in Digraph.applications.k4.k4_del]
K4Del.n_sub_Sm [variable, in Digraph.applications.k4.k4_del]
K4Del.o00 [variable, in Digraph.applications.k4.k4_del]
K4Del.rd [variable, in Digraph.applications.k4.k4_del]
K4Del.z0 [variable, in Digraph.applications.k4.k4_del]
K4Lower [section, in Digraph.applications.k4.k4_lower]
K4Lower.emb [variable, in Digraph.applications.k4.k4_lower]
K4Lower.f [variable, in Digraph.applications.k4.k4_lower]
K4Lower.h0 [variable, in Digraph.applications.k4.k4_lower]
K4Lower.h1 [variable, in Digraph.applications.k4.k4_lower]
K4Lower.m' [variable, in Digraph.applications.k4.k4_lower]
K4Lower.m3 [variable, in Digraph.applications.k4.k4_lower]
K4Lower.o00 [variable, in Digraph.applications.k4.k4_lower]
K4Lower.T4del [variable, in Digraph.applications.k4.k4_lower]
K4Lower.z0 [variable, in Digraph.applications.k4.k4_lower]
K4Value [section, in Digraph.applications.k4.k4_value]
K4Value.bool_final [variable, in Digraph.applications.k4.k4_value]
K4Value.InCliqueV [section, in Digraph.applications.k4.k4_value]
K4Value.InCliqueV.K [variable, in Digraph.applications.k4.k4_value]
K4Value.InCliqueV.Kcl [variable, in Digraph.applications.k4.k4_value]
K4Value.InCliqueV.sum6 [variable, in Digraph.applications.k4.k4_value]
K4Value.m' [variable, in Digraph.applications.k4.k4_value]
K4Value.m3 [variable, in Digraph.applications.k4.k4_value]
k4_del [library]
k4_lower [library]
k4_main [library]
k4_value [library]
K5Lower [section, in Digraph.applications.k5.k5_lower]
K5Lower.emb [variable, in Digraph.applications.k5.k5_lower]
K5Lower.f [variable, in Digraph.applications.k5.k5_lower]
K5Lower.m' [variable, in Digraph.applications.k5.k5_lower]
K5Lower.m3 [variable, in Digraph.applications.k5.k5_lower]
K5Lower.SD [variable, in Digraph.applications.k5.k5_lower]
K5Lower.T5del [variable, in Digraph.applications.k5.k5_lower]
K5Lower.z0 [variable, in Digraph.applications.k5.k5_lower]
K5Upper [section, in Digraph.applications.k5.k5_upper]
K5Upper.m' [variable, in Digraph.applications.k5.k5_upper]
K5Upper.o00 [variable, in Digraph.applications.k5.k5_upper]
K5Upper.qd [variable, in Digraph.applications.k5.k5_upper]
K5Upper.qdE [variable, in Digraph.applications.k5.k5_upper]
K5Upper.rd [variable, in Digraph.applications.k5.k5_upper]
K5Upper.sum9 [variable, in Digraph.applications.k5.k5_upper]
K5Upper.z0 [variable, in Digraph.applications.k5.k5_upper]
k5_lower [library]
k5_upper [library]
L
L [abbreviation, in Digraph.applications.ck3.lemma7]last_drop [lemma, in Digraph.core.dipath]
last_take [lemma, in Digraph.core.dipath]
lemma7 [lemma, in Digraph.applications.ck3.lemma7]
lemma7 [library]
lexprod [definition, in Digraph.constructions.product]
LexProd [section, in Digraph.constructions.product]
LexProdTournament [section, in Digraph.constructions.product]
LexProdTournament.T1 [variable, in Digraph.constructions.product]
LexProdTournament.T2 [variable, in Digraph.constructions.product]
LexProdVT [section, in Digraph.constructions.product]
LexProdVT.D1 [variable, in Digraph.constructions.product]
LexProdVT.D2 [variable, in Digraph.constructions.product]
lexprod_vertex_transitive [lemma, in Digraph.constructions.product]
lexprod_tournament [definition, in Digraph.constructions.product]
lexprod_total [lemma, in Digraph.constructions.product]
lexprod_irrefl [lemma, in Digraph.constructions.product]
lexprod_arcE [lemma, in Digraph.constructions.product]
LexProd.D1 [variable, in Digraph.constructions.product]
LexProd.D2 [variable, in Digraph.constructions.product]
le_r_trans [lemma, in Digraph.core.order]
le_r_total [lemma, in Digraph.core.order]
ltp [definition, in Digraph.core.order]
ltp_pullback [lemma, in Digraph.core.order]
ltp_realizeE [lemma, in Digraph.core.order]
ltp_asym [lemma, in Digraph.core.order]
ltp_total [lemma, in Digraph.core.order]
ltp_trans [lemma, in Digraph.core.order]
ltp_irrefl [lemma, in Digraph.core.order]
M
m [abbreviation, in Digraph.applications.k5.k5_lower]m [abbreviation, in Digraph.applications.k5.k5_upper]
m [abbreviation, in Digraph.applications.k5.cells]
m [abbreviation, in Digraph.applications.k5.main]
m [abbreviation, in Digraph.applications.k5.acn_base]
m [abbreviation, in Digraph.applications.k4.k4_del]
m [abbreviation, in Digraph.applications.k4.k4_main]
m [abbreviation, in Digraph.applications.k4.k4_value]
m [abbreviation, in Digraph.applications.k5.obstructions]
m [abbreviation, in Digraph.applications.k4.k4_lower]
m [abbreviation, in Digraph.applications.k5.acn_arc_facts]
m [abbreviation, in Digraph.applications.acn_bands]
m [abbreviation, in Digraph.applications.k5.in_neighbourhood]
m [abbreviation, in Digraph.constructions.circulant]
Main [section, in Digraph.applications.k5.main]
Main [section, in Digraph.applications.k4.k4_main]
main [library]
Main.hz [variable, in Digraph.applications.k4.k4_main]
Main.m' [variable, in Digraph.applications.k5.main]
Main.m' [variable, in Digraph.applications.k4.k4_main]
Main.m3 [variable, in Digraph.applications.k5.main]
Main.m3 [variable, in Digraph.applications.k4.k4_main]
Main.o00 [variable, in Digraph.applications.k5.main]
Main.o00 [variable, in Digraph.applications.k4.k4_main]
Main.z0 [variable, in Digraph.applications.k5.main]
Main.z0 [variable, in Digraph.applications.k4.k4_main]
maxpath_endclosure [lemma, in Digraph.core.dipath]
maxpath_no_loopback [lemma, in Digraph.invariants.strong]
mem_shift [lemma, in Digraph.applications.k5.acn_base]
mem_s [lemma, in Digraph.core.order]
mem_mid_F [lemma, in Digraph.applications.k4.k4_value]
mem_m_F [lemma, in Digraph.applications.k4.k4_value]
mem_sub_m_Hi [lemma, in Digraph.applications.k5.obstructions]
mem_sub_Hi_m [lemma, in Digraph.applications.k5.obstructions]
mem_sub_Hi1_Lo [lemma, in Digraph.applications.k5.obstructions]
mem_sub_Lo_Hi1 [lemma, in Digraph.applications.k5.obstructions]
mem0A [lemma, in Digraph.applications.k5.acn_base]
N
n [abbreviation, in Digraph.applications.k5.k5_lower]n [abbreviation, in Digraph.applications.k5.k5_upper]
n [abbreviation, in Digraph.applications.k5.cells]
n [abbreviation, in Digraph.applications.k5.main]
n [abbreviation, in Digraph.applications.k5.acn_base]
n [abbreviation, in Digraph.applications.k4.k4_del]
n [abbreviation, in Digraph.applications.k4.k4_main]
n [abbreviation, in Digraph.applications.k4.k4_value]
n [abbreviation, in Digraph.applications.k5.obstructions]
n [abbreviation, in Digraph.applications.k4.k4_lower]
n [abbreviation, in Digraph.applications.k5.acn_arc_facts]
n [abbreviation, in Digraph.applications.acn_bands]
n [abbreviation, in Digraph.applications.k5.in_neighbourhood]
n [abbreviation, in Digraph.constructions.circulant]
nat_n_split [lemma, in Digraph.applications.k5.obstructions]
no_short_strong3 [lemma, in Digraph.applications.ck3.ck3_main]
no_obstruction [lemma, in Digraph.applications.k5.obstructions]
ntransbP [lemma, in Digraph.core.tournament]
ntransb_card [lemma, in Digraph.core.tournament]
N_out_in_partition [lemma, in Digraph.core.tournament]
N_inE [lemma, in Digraph.core.tournament]
N_outE [lemma, in Digraph.core.tournament]
N_in [definition, in Digraph.core.tournament]
N_out [definition, in Digraph.core.tournament]
n_sub_eq_Sm [lemma, in Digraph.applications.k4.k4_value]
n_sub_gt_Sm [lemma, in Digraph.applications.k4.k4_value]
n_sub_ge_Sm [lemma, in Digraph.applications.k4.k4_value]
N0_0 [lemma, in Digraph.applications.k5.acn_base]
N0_val_in [lemma, in Digraph.applications.k5.acn_base]
O
obstrb [definition, in Digraph.applications.k5.obstructions]Obstructions [section, in Digraph.applications.k5.obstructions]
obstructions [library]
Obstructions.dbl_lt_addr [variable, in Digraph.applications.k5.obstructions]
Obstructions.m' [variable, in Digraph.applications.k5.obstructions]
Obstructions.WithClique [section, in Digraph.applications.k5.obstructions]
Obstructions.WithClique.A1 [variable, in Digraph.applications.k5.obstructions]
Obstructions.WithClique.K [variable, in Digraph.applications.k5.obstructions]
Obstructions.WithClique.Kcl [variable, in Digraph.applications.k5.obstructions]
occ [definition, in Digraph.applications.k5.cells]
occd [definition, in Digraph.applications.k4.k4_del]
occdP [lemma, in Digraph.applications.k4.k4_del]
occP [lemma, in Digraph.applications.k5.cells]
occv [definition, in Digraph.applications.k4.k4_value]
occvP [lemma, in Digraph.applications.k4.k4_value]
occ_and4F [lemma, in Digraph.applications.k5.obstructions]
occ_and3F [lemma, in Digraph.applications.k5.obstructions]
occ0134_F [lemma, in Digraph.applications.k4.k4_del]
occ023_F [lemma, in Digraph.applications.k4.k4_del]
occ124_F [lemma, in Digraph.applications.k4.k4_del]
occ24_1F [lemma, in Digraph.applications.k4.k4_value]
occ24_5F [lemma, in Digraph.applications.k4.k4_value]
occ24_block [lemma, in Digraph.applications.k4.k4_value]
occ5310_F [lemma, in Digraph.applications.k4.k4_value]
omegabar [definition, in Digraph.invariants.omegabar]
omegabar [library]
OmegaBarBasics [section, in Digraph.invariants.omegabar]
OmegaBarBasics.T [variable, in Digraph.invariants.omegabar]
omegabar_Tdel_ge4 [lemma, in Digraph.applications.k5.k5_lower]
omegabar_T_ge5 [lemma, in Digraph.applications.k5.k5_lower]
omegabar_Tdel_le4 [lemma, in Digraph.applications.k5.k5_upper]
omegabar_T_le5 [lemma, in Digraph.applications.k5.k5_upper]
omegabar_T5_del [lemma, in Digraph.applications.k5.main]
omegabar_T5 [lemma, in Digraph.applications.k5.main]
omegabar_AC_del [lemma, in Digraph.applications.k5.acn_base]
omegabar_ACdel0 [lemma, in Digraph.applications.k5.acn_base]
omegabar_AC [lemma, in Digraph.applications.k5.acn_base]
omegabar_ACdel_le2 [lemma, in Digraph.applications.k5.acn_base]
omegabar_AC_le3 [lemma, in Digraph.applications.k5.acn_base]
omegabar_lexprod_ge [lemma, in Digraph.invariants_advanced.substitution]
omegabar_T4del0 [lemma, in Digraph.applications.k4.k4_del]
omegabar_T4del_le3 [lemma, in Digraph.applications.k4.k4_del]
omegabar_del_vt [lemma, in Digraph.invariants_advanced.transitive]
omegabar_T4_del [lemma, in Digraph.applications.k4.k4_main]
omegabar_C3 [lemma, in Digraph.invariants.omegabar]
omegabar_TT [lemma, in Digraph.invariants.omegabar]
omegabar_card_le2 [lemma, in Digraph.invariants.omegabar]
omegabar_nil [lemma, in Digraph.invariants.omegabar]
omegabar_del [lemma, in Digraph.invariants.omegabar]
omegabar_sub [lemma, in Digraph.invariants.omegabar]
omegabar_dgiso [lemma, in Digraph.invariants.omegabar]
omegabar_embed [lemma, in Digraph.invariants.omegabar]
omegabar_transb [lemma, in Digraph.invariants.omegabar]
omegabar_le1 [lemma, in Digraph.invariants.omegabar]
omegabar_gt0 [lemma, in Digraph.invariants.omegabar]
omegabar_witness [lemma, in Digraph.invariants.omegabar]
omegabar_min [lemma, in Digraph.invariants.omegabar]
omegabar_T4 [lemma, in Digraph.applications.k4.k4_value]
omegabar_T4_le4 [lemma, in Digraph.applications.k4.k4_value]
omegabar_T4del_ge3 [lemma, in Digraph.applications.k4.k4_lower]
omegabar_T4_ge4 [lemma, in Digraph.applications.k4.k4_lower]
omegab_at_qd_le4 [lemma, in Digraph.applications.k5.k5_upper]
omegab_at_qk_le5 [lemma, in Digraph.applications.k5.k5_upper]
omegab_at_q0_le2 [lemma, in Digraph.applications.k5.acn_base]
omegab_at_qid_le3 [lemma, in Digraph.applications.k5.acn_base]
omegab_at_lexprod_ge [lemma, in Digraph.invariants_advanced.substitution]
omegab_at_qd_le3 [lemma, in Digraph.applications.k4.k4_del]
omegab_at_le1 [lemma, in Digraph.invariants.omegabar]
omegab_at [definition, in Digraph.invariants.omegabar]
omegab_at_qv_le4 [lemma, in Digraph.applications.k4.k4_value]
OmegaFacts [section, in Digraph.foundations.interop_graph_theory]
OmegaFacts.G [variable, in Digraph.foundations.interop_graph_theory]
omega_K2 [lemma, in Digraph.foundations.interop_graph_theory]
omega_hom [lemma, in Digraph.foundations.interop_graph_theory]
omega_ge2 [lemma, in Digraph.foundations.interop_graph_theory]
omega_le1 [lemma, in Digraph.foundations.interop_graph_theory]
omega_le_card [lemma, in Digraph.foundations.interop_graph_theory]
omega_ge1 [lemma, in Digraph.foundations.interop_graph_theory]
oppA_disjoint [lemma, in Digraph.applications.k5.acn_base]
opp_arcs_contra [lemma, in Digraph.applications.k5.obstructions]
order [library]
Oriented [abbreviation, in Digraph.core.oriented]
Oriented [module, in Digraph.core.oriented]
oriented [library]
OrientedCounting [section, in Digraph.core.oriented]
OrientedCounting.O [variable, in Digraph.core.oriented]
OrientedElpiOperations [module, in Digraph.core.oriented]
oriented_outsel__canonical__oriented_Oriented [definition, in Digraph.core.oriented]
oriented_outsel__canonical__digraph_DiGraph [definition, in Digraph.core.oriented]
oriented_outsel__canonical__digraph_RelDigraph [definition, in Digraph.core.oriented]
oriented_outsel__canonical__fintype_Finite [definition, in Digraph.core.oriented]
oriented_outsel__canonical__choice_Countable [definition, in Digraph.core.oriented]
oriented_outsel__canonical__choice_Choice [definition, in Digraph.core.oriented]
oriented_outsel__canonical__eqtype_Equality [definition, in Digraph.core.oriented]
oriented_card [lemma, in Digraph.core.oriented]
oriented_mindeg_card [lemma, in Digraph.core.oriented]
oriented_avg_bound [lemma, in Digraph.core.oriented]
oriented_arcs_bound [lemma, in Digraph.core.oriented]
Oriented_IsTournament [abbreviation, in Digraph.core.tournament]
Oriented_IsTournament.Exports [module, in Digraph.core.tournament]
Oriented_IsTournament.identity_builder [definition, in Digraph.core.tournament]
Oriented_IsTournament.axioms [abbreviation, in Digraph.core.tournament]
Oriented_IsTournament.phant_axioms [definition, in Digraph.core.tournament]
Oriented_IsTournament.Build [abbreviation, in Digraph.core.tournament]
Oriented_IsTournament.phant_Build [definition, in Digraph.core.tournament]
Oriented_IsTournament.arc_total [projection, in Digraph.core.tournament]
Oriented_IsTournament.axioms_ [record, in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament_V__canonical__oriented_Oriented [definition, in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament.local_mixin_oriented_DiGraph_IsOriented [variable, in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament_V__canonical__digraph_DiGraph [definition, in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament_V__canonical__fintype_Finite [definition, in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament.local_mixin_fintype_isFinite [variable, in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament_V__canonical__choice_Countable [definition, in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament_V__canonical__choice_Choice [definition, in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament_V__canonical__eqtype_Equality [definition, in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament.local_mixin_eqtype_hasDecEq [variable, in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament.local_mixin_choice_Choice_isCountable [variable, in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament.local_mixin_choice_hasChoice [variable, in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament_V__canonical__digraph_RelDigraph [definition, in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament.local_mixin_digraph_HasArc [variable, in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament.V [variable, in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament.Oriented_IsTournament [section, in Digraph.core.tournament]
Oriented_IsTournament [module, in Digraph.core.tournament]
Oriented.axioms_ [record, in Digraph.core.oriented]
Oriented.choice_Choice_isCountable_mixin [projection, in Digraph.core.oriented]
Oriented.choice_hasChoice_mixin [projection, in Digraph.core.oriented]
Oriented.class [projection, in Digraph.core.oriented]
Oriented.clone [abbreviation, in Digraph.core.oriented]
Oriented.copy [abbreviation, in Digraph.core.oriented]
Oriented.digraph_HasArc_mixin [projection, in Digraph.core.oriented]
Oriented.eqtype_hasDecEq_mixin [projection, in Digraph.core.oriented]
Oriented.Exports [module, in Digraph.core.oriented]
Oriented.Exports.orientedDigraph [abbreviation, in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented__to__digraph_DiGraph [definition, in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented_class__to__digraph_DiGraph_class [definition, in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented__to__fintype_Finite [definition, in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented_class__to__fintype_Finite_class [definition, in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented__to__choice_Countable [definition, in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented_class__to__choice_Countable_class [definition, in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented__to__choice_Choice [definition, in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented_class__to__choice_Choice_class [definition, in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented__to__eqtype_Equality [definition, in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented_class__to__eqtype_Equality_class [definition, in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented__to__digraph_RelDigraph [definition, in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented_class__to__digraph_RelDigraph_class [definition, in Digraph.core.oriented]
Oriented.fintype_isFinite_mixin [projection, in Digraph.core.oriented]
Oriented.on [abbreviation, in Digraph.core.oriented]
Oriented.on_ [abbreviation, in Digraph.core.oriented]
Oriented.oriented_DiGraph_IsOriented_mixin [projection, in Digraph.core.oriented]
Oriented.pack_ [definition, in Digraph.core.oriented]
Oriented.phant_on_ [definition, in Digraph.core.oriented]
Oriented.phant_clone [definition, in Digraph.core.oriented]
Oriented.sort [projection, in Digraph.core.oriented]
Oriented.type [record, in Digraph.core.oriented]
outdeg [definition, in Digraph.core.oriented]
OutDegree [section, in Digraph.core.oriented]
OutDegree.D [variable, in Digraph.core.oriented]
outdeg_induced [lemma, in Digraph.core.oriented]
outdeg_in_sumE [lemma, in Digraph.core.oriented]
outdeg_in_mono [lemma, in Digraph.core.oriented]
outdeg_in_le [lemma, in Digraph.core.oriented]
outdeg_inT [lemma, in Digraph.core.oriented]
outdeg_in [definition, in Digraph.core.oriented]
outdeg_closed [lemma, in Digraph.invariants.strong]
outsel [definition, in Digraph.core.oriented]
OutSelection [section, in Digraph.core.oriented]
OutSelectionOriented [section, in Digraph.core.oriented]
OutSelectionOriented.f [variable, in Digraph.core.oriented]
OutSelectionOriented.O [variable, in Digraph.core.oriented]
OutSelection.D [variable, in Digraph.core.oriented]
OutSelection.f [variable, in Digraph.core.oriented]
outsel_ksel_outdeg [lemma, in Digraph.core.oriented]
outsel_asymm [lemma, in Digraph.core.oriented]
outsel_irrefl [lemma, in Digraph.core.oriented]
outsel_arc_sub [lemma, in Digraph.core.oriented]
outsel_arcE [lemma, in Digraph.core.oriented]
P
PermOrder [section, in Digraph.core.order]PermOrder.Realize [section, in Digraph.core.order]
PermOrder.Realize.le_r [variable, in Digraph.core.order]
PermOrder.Realize.r [variable, in Digraph.core.order]
PermOrder.Realize.r_total [variable, in Digraph.core.order]
PermOrder.Realize.r_trans [variable, in Digraph.core.order]
PermOrder.Realize.r_irr [variable, in Digraph.core.order]
PermOrder.Realize.s [variable, in Digraph.core.order]
PermOrder.V [variable, in Digraph.core.order]
pos [abbreviation, in Digraph.invariants_advanced.substitution]
posmin [definition, in Digraph.invariants_advanced.substitution]
posmin_neq [lemma, in Digraph.invariants_advanced.substitution]
posmin_le [lemma, in Digraph.invariants_advanced.substitution]
pos_inj [lemma, in Digraph.invariants_advanced.substitution]
prelude [library]
prelude_ssr [lemma, in Digraph.foundations.prelude]
prelude_set [lemma, in Digraph.foundations.prelude]
prelude_classical [lemma, in Digraph.foundations.prelude]
prev_head [lemma, in Digraph.core.dipath]
product [library]
product_lexprod__canonical__tournament_Tournament [definition, in Digraph.constructions.product]
product_lexprod__canonical__oriented_Oriented [definition, in Digraph.constructions.product]
product_lexprod__canonical__digraph_DiGraph [definition, in Digraph.constructions.product]
product_lexprod__canonical__digraph_RelDigraph [definition, in Digraph.constructions.product]
product_lexprod__canonical__fintype_Finite [definition, in Digraph.constructions.product]
product_lexprod__canonical__choice_Countable [definition, in Digraph.constructions.product]
product_lexprod__canonical__choice_Choice [definition, in Digraph.constructions.product]
product_lexprod__canonical__eqtype_Equality [definition, in Digraph.constructions.product]
proper_sub_omegabar_le4 [lemma, in Digraph.applications.k5.main]
Q
qd [definition, in Digraph.applications.k4.k4_del]qdE [lemma, in Digraph.applications.k4.k4_del]
qk [definition, in Digraph.applications.k5.cells]
qkE [lemma, in Digraph.applications.k5.cells]
quad_D [lemma, in Digraph.applications.k5.obstructions]
quad_C [lemma, in Digraph.applications.k5.obstructions]
quad_B [lemma, in Digraph.applications.k5.obstructions]
quad_A [lemma, in Digraph.applications.k5.obstructions]
question_5_9_fails_at_k5 [lemma, in Digraph.applications.k5.main]
question_5_9_fails_at_k3 [lemma, in Digraph.applications.unified]
question_5_9_fails_at_k4 [lemma, in Digraph.applications.k4.k4_main]
qv [definition, in Digraph.applications.k4.k4_value]
qvE [lemma, in Digraph.applications.k4.k4_value]
R
radix_eq_inv [lemma, in Digraph.applications.acn_bands]radix_lt_inv [lemma, in Digraph.applications.acn_bands]
radix_ltA [lemma, in Digraph.applications.acn_bands]
rank_lt [lemma, in Digraph.core.order]
rd_total [lemma, in Digraph.applications.k5.k5_upper]
rd_trans [lemma, in Digraph.applications.k5.k5_upper]
rd_irr [lemma, in Digraph.applications.k5.k5_upper]
rd_total [lemma, in Digraph.applications.k4.k4_del]
rd_trans [lemma, in Digraph.applications.k4.k4_del]
rd_irr [lemma, in Digraph.applications.k4.k4_del]
realize [definition, in Digraph.core.order]
reduction [lemma, in Digraph.invariants.strong]
RelDigraph [abbreviation, in Digraph.core.digraph]
RelDigraph [module, in Digraph.core.digraph]
RelDigraphElpiOperations [module, in Digraph.core.digraph]
RelDigraph.axioms_ [record, in Digraph.core.digraph]
RelDigraph.class [projection, in Digraph.core.digraph]
RelDigraph.clone [abbreviation, in Digraph.core.digraph]
RelDigraph.copy [abbreviation, in Digraph.core.digraph]
RelDigraph.digraph_HasArc_mixin [projection, in Digraph.core.digraph]
RelDigraph.Exports [module, in Digraph.core.digraph]
RelDigraph.Exports.relDigraph [abbreviation, in Digraph.core.digraph]
RelDigraph.on [abbreviation, in Digraph.core.digraph]
RelDigraph.on_ [abbreviation, in Digraph.core.digraph]
RelDigraph.pack_ [definition, in Digraph.core.digraph]
RelDigraph.phant_on_ [definition, in Digraph.core.digraph]
RelDigraph.phant_clone [definition, in Digraph.core.digraph]
RelDigraph.sort [projection, in Digraph.core.digraph]
RelDigraph.type [record, in Digraph.core.digraph]
repA_band [lemma, in Digraph.applications.k5.obstructions]
rep_Z [lemma, in Digraph.applications.k5.obstructions]
rep_Lo [lemma, in Digraph.applications.k5.obstructions]
rep_Hi [lemma, in Digraph.applications.k5.obstructions]
rfun [definition, in Digraph.core.order]
rfun_inj [lemma, in Digraph.core.order]
rH_total [lemma, in Digraph.invariants_advanced.substitution]
rH_trans [lemma, in Digraph.invariants_advanced.substitution]
rH_irr [lemma, in Digraph.invariants_advanced.substitution]
rid_total [lemma, in Digraph.applications.k5.acn_base]
rid_trans [lemma, in Digraph.applications.k5.acn_base]
rid_irr [lemma, in Digraph.applications.k5.acn_base]
rk [definition, in Digraph.applications.k5.cells]
rk_total [lemma, in Digraph.applications.k5.cells]
rk_trans [lemma, in Digraph.applications.k5.cells]
rk_irr [lemma, in Digraph.applications.k5.cells]
rset [definition, in Digraph.invariants.strong]
rset_trans [lemma, in Digraph.invariants.strong]
rset_closed [lemma, in Digraph.invariants.strong]
rset_id [lemma, in Digraph.invariants.strong]
rS_total [lemma, in Digraph.invariants_advanced.substitution]
rS_trans [lemma, in Digraph.invariants_advanced.substitution]
rS_irr [lemma, in Digraph.invariants_advanced.substitution]
rv [definition, in Digraph.applications.k4.k4_value]
rv_total [lemma, in Digraph.applications.k4.k4_value]
rv_trans [lemma, in Digraph.applications.k4.k4_value]
rv_irr [lemma, in Digraph.applications.k4.k4_value]
r0_total [lemma, in Digraph.applications.k5.acn_base]
r0_trans [lemma, in Digraph.applications.k5.acn_base]
r0_irr [lemma, in Digraph.applications.k5.acn_base]
S
set1_cliques [lemma, in Digraph.foundations.interop_graph_theory]shiftI [lemma, in Digraph.applications.k5.acn_base]
shift_comp [lemma, in Digraph.applications.k5.acn_base]
shift0 [lemma, in Digraph.applications.k5.acn_base]
sidx [definition, in Digraph.applications.k4.k4_value]
sidx_del_le4 [lemma, in Digraph.applications.k4.k4_del]
sidx_inj_clique [lemma, in Digraph.applications.k4.k4_value]
sidx_le5 [lemma, in Digraph.applications.k4.k4_value]
sidx_decode [lemma, in Digraph.applications.k4.k4_value]
sink_exists [lemma, in Digraph.invariants.strong]
size_s [lemma, in Digraph.core.order]
sorted_s [lemma, in Digraph.core.order]
Specif_sig__canonical__oriented_Oriented [definition, in Digraph.core.oriented]
Specif_sig__canonical__tournament_Tournament [definition, in Digraph.core.tournament]
Specif_sig__canonical__digraph_DiGraph [definition, in Digraph.core.digraph]
Specif_sig__canonical__digraph_RelDigraph [definition, in Digraph.core.digraph]
square [lemma, in Digraph.applications.k5.obstructions]
Strong [section, in Digraph.invariants.strong]
strong [library]
strongb [definition, in Digraph.invariants.strong]
strongb_induced_closed [lemma, in Digraph.invariants.strong]
strongP [lemma, in Digraph.invariants.strong]
Strong.D [variable, in Digraph.invariants.strong]
SubDigraph [section, in Digraph.core.digraph]
SubDigraph.D [variable, in Digraph.core.digraph]
SubDigraph.P [variable, in Digraph.core.digraph]
SubOriented [section, in Digraph.core.oriented]
SubOriented.O [variable, in Digraph.core.oriented]
SubOriented.P [variable, in Digraph.core.oriented]
Substitution [section, in Digraph.invariants_advanced.substitution]
substitution [library]
Substitution.H [variable, in Digraph.invariants_advanced.substitution]
Substitution.Hpos [variable, in Digraph.invariants_advanced.substitution]
Substitution.S [variable, in Digraph.invariants_advanced.substitution]
Substitution.Spos [variable, in Digraph.invariants_advanced.substitution]
Substitution.WithOrder [section, in Digraph.invariants_advanced.substitution]
Substitution.WithOrder.h0 [variable, in Digraph.invariants_advanced.substitution]
Substitution.WithOrder.p [variable, in Digraph.invariants_advanced.substitution]
Substitution.WithOrder.qH [variable, in Digraph.invariants_advanced.substitution]
Substitution.WithOrder.qHE [variable, in Digraph.invariants_advanced.substitution]
Substitution.WithOrder.qS [variable, in Digraph.invariants_advanced.substitution]
Substitution.WithOrder.qSE [variable, in Digraph.invariants_advanced.substitution]
Substitution.WithOrder.rH [variable, in Digraph.invariants_advanced.substitution]
Substitution.WithOrder.rS [variable, in Digraph.invariants_advanced.substitution]
SubTournament [section, in Digraph.core.tournament]
SubTournament.P [variable, in Digraph.core.tournament]
SubTournament.T [variable, in Digraph.core.tournament]
sub_oarc_asymm [lemma, in Digraph.core.oriented]
sub_oarc_irrefl [lemma, in Digraph.core.oriented]
sub_tournament [definition, in Digraph.core.tournament]
sub_arc_total [lemma, in Digraph.core.tournament]
sub_eq_m [lemma, in Digraph.applications.k4.k4_value]
sub_arcE [lemma, in Digraph.core.digraph]
T
take_path_last [lemma, in Digraph.core.dipath]Tournament [abbreviation, in Digraph.core.tournament]
Tournament [module, in Digraph.core.tournament]
tournament [library]
TournamentElpiOperations [module, in Digraph.core.tournament]
TournamentTheory [section, in Digraph.core.tournament]
TournamentTheory.T [variable, in Digraph.core.tournament]
tournament_TT__canonical__tournament_Tournament [definition, in Digraph.core.tournament]
tournament_TT__canonical__oriented_Oriented [definition, in Digraph.core.tournament]
tournament_DiGraph_IsTournament__to__oriented_DiGraph_IsOriented__45 [definition, in Digraph.core.tournament]
tournament_DiGraph_IsTournament__to__tournament_Oriented_IsTournament__43 [definition, in Digraph.core.tournament]
tournament_TT__canonical__digraph_DiGraph [definition, in Digraph.core.tournament]
tournament_TT__canonical__digraph_RelDigraph [definition, in Digraph.core.tournament]
tournament_TT__canonical__fintype_Finite [definition, in Digraph.core.tournament]
tournament_TT__canonical__choice_Countable [definition, in Digraph.core.tournament]
tournament_TT__canonical__choice_Choice [definition, in Digraph.core.tournament]
tournament_TT__canonical__eqtype_Equality [definition, in Digraph.core.tournament]
tournament_C3__canonical__tournament_Tournament [definition, in Digraph.core.tournament]
tournament_C3__canonical__oriented_Oriented [definition, in Digraph.core.tournament]
tournament_DiGraph_IsTournament__to__oriented_DiGraph_IsOriented [definition, in Digraph.core.tournament]
tournament_DiGraph_IsTournament__to__tournament_Oriented_IsTournament [definition, in Digraph.core.tournament]
tournament_C3__canonical__digraph_DiGraph [definition, in Digraph.core.tournament]
tournament_C3__canonical__digraph_RelDigraph [definition, in Digraph.core.tournament]
tournament_C3__canonical__fintype_Finite [definition, in Digraph.core.tournament]
tournament_C3__canonical__choice_Countable [definition, in Digraph.core.tournament]
tournament_C3__canonical__choice_Choice [definition, in Digraph.core.tournament]
tournament_C3__canonical__eqtype_Equality [definition, in Digraph.core.tournament]
tournament_DiGraph_IsTournament__to__oriented_DiGraph_IsOriented [definition, in Digraph.constructions.product]
tournament_DiGraph_IsTournament__to__tournament_Oriented_IsTournament [definition, in Digraph.constructions.product]
tournament_DiGraph_IsTournament__to__oriented_DiGraph_IsOriented [definition, in Digraph.constructions.circulant]
tournament_DiGraph_IsTournament__to__tournament_Oriented_IsTournament [definition, in Digraph.constructions.circulant]
Tournament.axioms_ [record, in Digraph.core.tournament]
Tournament.choice_Choice_isCountable_mixin [projection, in Digraph.core.tournament]
Tournament.choice_hasChoice_mixin [projection, in Digraph.core.tournament]
Tournament.class [projection, in Digraph.core.tournament]
Tournament.clone [abbreviation, in Digraph.core.tournament]
Tournament.copy [abbreviation, in Digraph.core.tournament]
Tournament.digraph_HasArc_mixin [projection, in Digraph.core.tournament]
Tournament.eqtype_hasDecEq_mixin [projection, in Digraph.core.tournament]
Tournament.Exports [module, in Digraph.core.tournament]
Tournament.Exports.tournament [abbreviation, in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament__to__oriented_Oriented [definition, in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament_class__to__oriented_Oriented_class [definition, in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament__to__digraph_DiGraph [definition, in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament_class__to__digraph_DiGraph_class [definition, in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament__to__fintype_Finite [definition, in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament_class__to__fintype_Finite_class [definition, in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament__to__choice_Countable [definition, in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament_class__to__choice_Countable_class [definition, in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament__to__choice_Choice [definition, in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament_class__to__choice_Choice_class [definition, in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament__to__eqtype_Equality [definition, in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament_class__to__eqtype_Equality_class [definition, in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament__to__digraph_RelDigraph [definition, in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament_class__to__digraph_RelDigraph_class [definition, in Digraph.core.tournament]
Tournament.fintype_isFinite_mixin [projection, in Digraph.core.tournament]
Tournament.on [abbreviation, in Digraph.core.tournament]
Tournament.on_ [abbreviation, in Digraph.core.tournament]
Tournament.oriented_DiGraph_IsOriented_mixin [projection, in Digraph.core.tournament]
Tournament.pack_ [definition, in Digraph.core.tournament]
Tournament.phant_on_ [definition, in Digraph.core.tournament]
Tournament.phant_clone [definition, in Digraph.core.tournament]
Tournament.sort [projection, in Digraph.core.tournament]
Tournament.tournament_Oriented_IsTournament_mixin [projection, in Digraph.core.tournament]
Tournament.type [record, in Digraph.core.tournament]
to_GT [definition, in Digraph.core.digraph]
transb [definition, in Digraph.core.tournament]
transbP [lemma, in Digraph.core.tournament]
transitive [library]
translation [definition, in Digraph.constructions.cayley]
translationE [lemma, in Digraph.constructions.cayley]
translation_aut [lemma, in Digraph.constructions.cayley]
triple_B [lemma, in Digraph.applications.k5.obstructions]
triple_A [lemma, in Digraph.applications.k5.obstructions]
TT [definition, in Digraph.core.tournament]
TT [section, in Digraph.core.tournament]
TT_transb [lemma, in Digraph.core.tournament]
TT_total [lemma, in Digraph.core.tournament]
TT_irrefl [lemma, in Digraph.core.tournament]
TT.n [variable, in Digraph.core.tournament]
tv [abbreviation, in Digraph.applications.k4.k4_del]
T4 [abbreviation, in Digraph.applications.k4.k4_del]
T4 [abbreviation, in Digraph.applications.k4.k4_main]
T4 [abbreviation, in Digraph.applications.k4.k4_value]
T4 [abbreviation, in Digraph.applications.k4.k4_lower]
T4del [abbreviation, in Digraph.applications.k4.k4_del]
T4_kcritical4 [lemma, in Digraph.applications.k4.k4_main]
T4_vertex_transitive [lemma, in Digraph.applications.k4.k4_main]
T5 [abbreviation, in Digraph.applications.k5.k5_lower]
T5 [abbreviation, in Digraph.applications.k5.k5_upper]
T5 [abbreviation, in Digraph.applications.k5.cells]
T5 [abbreviation, in Digraph.applications.k5.main]
T5 [abbreviation, in Digraph.applications.k5.obstructions]
T5del [abbreviation, in Digraph.applications.k5.k5_upper]
T5_kcritical5 [lemma, in Digraph.applications.k5.main]
T5_vertex_transitive [lemma, in Digraph.applications.k5.main]
U
unified [library]UniformDeletion [section, in Digraph.invariants_advanced.transitive]
UniformDeletion.T [variable, in Digraph.invariants_advanced.transitive]
Uniqueness [section, in Digraph.invariants.critical]
Uniqueness.crit [variable, in Digraph.invariants.critical]
Uniqueness.cyc [variable, in Digraph.invariants.critical]
Uniqueness.del1 [variable, in Digraph.invariants.critical]
Uniqueness.Ntr [variable, in Digraph.invariants.critical]
Uniqueness.ob2 [variable, in Digraph.invariants.critical]
Uniqueness.T [variable, in Digraph.invariants.critical]
Uniqueness.Tpos [variable, in Digraph.invariants.critical]
V
vals12 [lemma, in Digraph.applications.k4.k4_value]val_zeta [lemma, in Digraph.applications.k5.acn_base]
val_sub_gt [lemma, in Digraph.applications.k5.acn_arc_facts]
val_sub_le [lemma, in Digraph.applications.k5.acn_arc_facts]
val_oppE [lemma, in Digraph.applications.k5.acn_arc_facts]
val_addE [lemma, in Digraph.applications.k5.acn_arc_facts]
val_Zp_opp [lemma, in Digraph.constructions.circulant]
val1 [lemma, in Digraph.applications.k5.acn_base]
vertex_transitivebP [lemma, in Digraph.constructions.automorphism]
vertex_transitiveb [definition, in Digraph.constructions.automorphism]
vt_kcritical [lemma, in Digraph.invariants_advanced.transitive]
Z
ZpGroupBridge [section, in Digraph.constructions.circulant]ZpGroupBridge.p [variable, in Digraph.constructions.circulant]
Zp_1gE [lemma, in Digraph.constructions.circulant]
Zp_invgE [lemma, in Digraph.constructions.circulant]
Zp_mulgE [lemma, in Digraph.constructions.circulant]
other
_ --> _ (digraph_scope) [notation, in Digraph.core.digraph]ω̄( _ ) [notation, in Digraph.invariants.omegabar]
Notation Index
other
_ --> _ (digraph_scope) [in Digraph.core.digraph]ω̄( _ ) [in Digraph.invariants.omegabar]
Module Index
B
Builders_1.Builders_Export_7 [in Digraph.core.tournament]Builders_1.Super [in Digraph.core.tournament]
Builders_1 [in Digraph.core.tournament]
D
DiGraph [in Digraph.core.digraph]DiGraphElpiOperations [in Digraph.core.digraph]
DiGraph_IsOriented.Exports [in Digraph.core.oriented]
DiGraph_IsOriented [in Digraph.core.oriented]
DiGraph_IsTournament.Exports [in Digraph.core.tournament]
DiGraph_IsTournament [in Digraph.core.tournament]
DiGraph.Exports [in Digraph.core.digraph]
H
HasArc [in Digraph.core.digraph]HasArc.Exports [in Digraph.core.digraph]
O
Oriented [in Digraph.core.oriented]OrientedElpiOperations [in Digraph.core.oriented]
Oriented_IsTournament.Exports [in Digraph.core.tournament]
Oriented_IsTournament [in Digraph.core.tournament]
Oriented.Exports [in Digraph.core.oriented]
R
RelDigraph [in Digraph.core.digraph]RelDigraphElpiOperations [in Digraph.core.digraph]
RelDigraph.Exports [in Digraph.core.digraph]
T
Tournament [in Digraph.core.tournament]TournamentElpiOperations [in Digraph.core.tournament]
Tournament.Exports [in Digraph.core.tournament]
Variable Index
A
ACBase.A [in Digraph.applications.k5.acn_base]ACBase.c1 [in Digraph.applications.k5.acn_base]
ACBase.c2 [in Digraph.applications.k5.acn_base]
ACBase.c3 [in Digraph.applications.k5.acn_base]
ACBase.m' [in Digraph.applications.k5.acn_base]
ACBase.N0 [in Digraph.applications.k5.acn_base]
ACBase.qid [in Digraph.applications.k5.acn_base]
ACBase.qidE [in Digraph.applications.k5.acn_base]
ACBase.q0 [in Digraph.applications.k5.acn_base]
ACBase.q0E [in Digraph.applications.k5.acn_base]
ACBase.rid [in Digraph.applications.k5.acn_base]
ACBase.r0 [in Digraph.applications.k5.acn_base]
ACBase.shift [in Digraph.applications.k5.acn_base]
ACBase.zeta [in Digraph.applications.k5.acn_base]
ACBase.z0 [in Digraph.applications.k5.acn_base]
AcnBands.dbl_lt_addr [in Digraph.applications.acn_bands]
AcnBands.lt_addl_pos [in Digraph.applications.acn_bands]
AcnBands.m' [in Digraph.applications.acn_bands]
AC.m' [in Digraph.constructions.circulant]
AC.val_oppE [in Digraph.constructions.circulant]
ArcFacts.m' [in Digraph.applications.k5.acn_arc_facts]
Automorphism.D [in Digraph.constructions.automorphism]
B
Backedge.p [in Digraph.core.order]Backedge.T [in Digraph.core.order]
Builders_1.Builders_1.fresh_name_2 [in Digraph.core.tournament]
Builders_1.Builders_1.local_mixin_fintype_isFinite [in Digraph.core.tournament]
Builders_1.Builders_1.local_mixin_eqtype_hasDecEq [in Digraph.core.tournament]
Builders_1.Builders_1.local_mixin_choice_Choice_isCountable [in Digraph.core.tournament]
Builders_1.Builders_1.local_mixin_choice_hasChoice [in Digraph.core.tournament]
Builders_1.Builders_1.local_mixin_digraph_HasArc [in Digraph.core.tournament]
Builders_1.Builders_1.V [in Digraph.core.tournament]
C
Cayley.A [in Digraph.constructions.cayley]Cayley.gT [in Digraph.constructions.cayley]
Cells.InClique.K [in Digraph.applications.k5.cells]
Cells.InClique.Kcl [in Digraph.applications.k5.cells]
Cells.m' [in Digraph.applications.k5.cells]
CKDefs.D [in Digraph.applications.ck3.lemma7]
D
DiGraph_IsOriented.DiGraph_IsOriented.local_mixin_fintype_isFinite [in Digraph.core.oriented]DiGraph_IsOriented.DiGraph_IsOriented.local_mixin_eqtype_hasDecEq [in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented.local_mixin_choice_Choice_isCountable [in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented.local_mixin_choice_hasChoice [in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented.local_mixin_digraph_HasArc [in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented.V [in Digraph.core.oriented]
DiGraph_IsTournament.DiGraph_IsTournament.local_mixin_fintype_isFinite [in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament.local_mixin_eqtype_hasDecEq [in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament.local_mixin_choice_Choice_isCountable [in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament.local_mixin_choice_hasChoice [in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament.local_mixin_digraph_HasArc [in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament.V [in Digraph.core.tournament]
DiPathDef.D [in Digraph.core.dipath]
Domination.T [in Digraph.invariants.domination]
H
HasArc.HasArc.V [in Digraph.core.digraph]hb_instance_11.D [in Digraph.core.digraph]
hb_instance_1.D [in Digraph.core.digraph]
H17.m' [in Digraph.applications.k5.in_neighbourhood]
K
Kernel.a [in Digraph.applications.ck3.lemma7]Kernel.AB_part [in Digraph.applications.ck3.lemma7]
Kernel.aE [in Digraph.applications.ck3.lemma7]
Kernel.aidx [in Digraph.applications.ck3.lemma7]
Kernel.arc_w_a [in Digraph.applications.ck3.lemma7]
Kernel.arc_y_a [in Digraph.applications.ck3.lemma7]
Kernel.Aset [in Digraph.applications.ck3.lemma7]
Kernel.A_le [in Digraph.applications.ck3.lemma7]
Kernel.a_le [in Digraph.applications.ck3.lemma7]
Kernel.a_ge1 [in Digraph.applications.ck3.lemma7]
Kernel.a_min [in Digraph.applications.ck3.lemma7]
Kernel.a_lt [in Digraph.applications.ck3.lemma7]
Kernel.Bset [in Digraph.applications.ck3.lemma7]
Kernel.BsetE [in Digraph.applications.ck3.lemma7]
Kernel.claim11 [in Digraph.applications.ck3.lemma7]
Kernel.claim12 [in Digraph.applications.ck3.lemma7]
Kernel.countA [in Digraph.applications.ck3.lemma7]
Kernel.countB [in Digraph.applications.ck3.lemma7]
Kernel.Cs [in Digraph.applications.ck3.lemma7]
Kernel.CsE [in Digraph.applications.ck3.lemma7]
Kernel.dcC [in Digraph.applications.ck3.lemma7]
Kernel.delta [in Digraph.applications.ck3.lemma7]
Kernel.endclosure [in Digraph.applications.ck3.lemma7]
Kernel.exMP [in Digraph.applications.ck3.lemma7]
Kernel.H [in Digraph.applications.ck3.lemma7]
Kernel.has_back [in Digraph.applications.ck3.lemma7]
Kernel.Hd [in Digraph.applications.ck3.lemma7]
Kernel.Hell [in Digraph.applications.ck3.lemma7]
Kernel.Hn [in Digraph.applications.ck3.lemma7]
Kernel.Hreg [in Digraph.applications.ck3.lemma7]
Kernel.Hstr [in Digraph.applications.ck3.lemma7]
Kernel.isMP [in Digraph.applications.ck3.lemma7]
Kernel.mptype [in Digraph.applications.ck3.lemma7]
Kernel.mp0 [in Digraph.applications.ck3.lemma7]
Kernel.nbig [in Digraph.applications.ck3.lemma7]
Kernel.prefC [in Digraph.applications.ck3.lemma7]
Kernel.ps [in Digraph.applications.ck3.lemma7]
Kernel.pstar [in Digraph.applications.ck3.lemma7]
Kernel.pstarMP [in Digraph.applications.ck3.lemma7]
Kernel.pstar_min [in Digraph.applications.ck3.lemma7]
Kernel.s [in Digraph.applications.ck3.lemma7]
Kernel.sL [in Digraph.applications.ck3.lemma7]
Kernel.Sset [in Digraph.applications.ck3.lemma7]
Kernel.szC [in Digraph.applications.ck3.lemma7]
Kernel.S_sub_C [in Digraph.applications.ck3.lemma7]
Kernel.S_card [in Digraph.applications.ck3.lemma7]
Kernel.uC [in Digraph.applications.ck3.lemma7]
Kernel.uP [in Digraph.applications.ck3.lemma7]
Kernel.va_B [in Digraph.applications.ck3.lemma7]
Kernel.w [in Digraph.applications.ck3.lemma7]
Kernel.wP [in Digraph.applications.ck3.lemma7]
Kernel.x [in Digraph.applications.ck3.lemma7]
Kernel.y [in Digraph.applications.ck3.lemma7]
Kernel.yS [in Digraph.applications.ck3.lemma7]
KSelection.D [in Digraph.core.oriented]
KSelection.k [in Digraph.core.oriented]
K4Del.bool_finalD [in Digraph.applications.k4.k4_del]
K4Del.hz [in Digraph.applications.k4.k4_del]
K4Del.InCliqueD.K [in Digraph.applications.k4.k4_del]
K4Del.InCliqueD.Kcl [in Digraph.applications.k4.k4_del]
K4Del.InCliqueD.sum5 [in Digraph.applications.k4.k4_del]
K4Del.m' [in Digraph.applications.k4.k4_del]
K4Del.m3 [in Digraph.applications.k4.k4_del]
K4Del.n_sub_ltm_gtSm [in Digraph.applications.k4.k4_del]
K4Del.n_sub_Sm [in Digraph.applications.k4.k4_del]
K4Del.o00 [in Digraph.applications.k4.k4_del]
K4Del.rd [in Digraph.applications.k4.k4_del]
K4Del.z0 [in Digraph.applications.k4.k4_del]
K4Lower.emb [in Digraph.applications.k4.k4_lower]
K4Lower.f [in Digraph.applications.k4.k4_lower]
K4Lower.h0 [in Digraph.applications.k4.k4_lower]
K4Lower.h1 [in Digraph.applications.k4.k4_lower]
K4Lower.m' [in Digraph.applications.k4.k4_lower]
K4Lower.m3 [in Digraph.applications.k4.k4_lower]
K4Lower.o00 [in Digraph.applications.k4.k4_lower]
K4Lower.T4del [in Digraph.applications.k4.k4_lower]
K4Lower.z0 [in Digraph.applications.k4.k4_lower]
K4Value.bool_final [in Digraph.applications.k4.k4_value]
K4Value.InCliqueV.K [in Digraph.applications.k4.k4_value]
K4Value.InCliqueV.Kcl [in Digraph.applications.k4.k4_value]
K4Value.InCliqueV.sum6 [in Digraph.applications.k4.k4_value]
K4Value.m' [in Digraph.applications.k4.k4_value]
K4Value.m3 [in Digraph.applications.k4.k4_value]
K5Lower.emb [in Digraph.applications.k5.k5_lower]
K5Lower.f [in Digraph.applications.k5.k5_lower]
K5Lower.m' [in Digraph.applications.k5.k5_lower]
K5Lower.m3 [in Digraph.applications.k5.k5_lower]
K5Lower.SD [in Digraph.applications.k5.k5_lower]
K5Lower.T5del [in Digraph.applications.k5.k5_lower]
K5Lower.z0 [in Digraph.applications.k5.k5_lower]
K5Upper.m' [in Digraph.applications.k5.k5_upper]
K5Upper.o00 [in Digraph.applications.k5.k5_upper]
K5Upper.qd [in Digraph.applications.k5.k5_upper]
K5Upper.qdE [in Digraph.applications.k5.k5_upper]
K5Upper.rd [in Digraph.applications.k5.k5_upper]
K5Upper.sum9 [in Digraph.applications.k5.k5_upper]
K5Upper.z0 [in Digraph.applications.k5.k5_upper]
L
LexProdTournament.T1 [in Digraph.constructions.product]LexProdTournament.T2 [in Digraph.constructions.product]
LexProdVT.D1 [in Digraph.constructions.product]
LexProdVT.D2 [in Digraph.constructions.product]
LexProd.D1 [in Digraph.constructions.product]
LexProd.D2 [in Digraph.constructions.product]
M
Main.hz [in Digraph.applications.k4.k4_main]Main.m' [in Digraph.applications.k5.main]
Main.m' [in Digraph.applications.k4.k4_main]
Main.m3 [in Digraph.applications.k5.main]
Main.m3 [in Digraph.applications.k4.k4_main]
Main.o00 [in Digraph.applications.k5.main]
Main.o00 [in Digraph.applications.k4.k4_main]
Main.z0 [in Digraph.applications.k5.main]
Main.z0 [in Digraph.applications.k4.k4_main]
O
Obstructions.dbl_lt_addr [in Digraph.applications.k5.obstructions]Obstructions.m' [in Digraph.applications.k5.obstructions]
Obstructions.WithClique.A1 [in Digraph.applications.k5.obstructions]
Obstructions.WithClique.K [in Digraph.applications.k5.obstructions]
Obstructions.WithClique.Kcl [in Digraph.applications.k5.obstructions]
OmegaBarBasics.T [in Digraph.invariants.omegabar]
OmegaFacts.G [in Digraph.foundations.interop_graph_theory]
OrientedCounting.O [in Digraph.core.oriented]
Oriented_IsTournament.Oriented_IsTournament.local_mixin_oriented_DiGraph_IsOriented [in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament.local_mixin_fintype_isFinite [in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament.local_mixin_eqtype_hasDecEq [in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament.local_mixin_choice_Choice_isCountable [in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament.local_mixin_choice_hasChoice [in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament.local_mixin_digraph_HasArc [in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament.V [in Digraph.core.tournament]
OutDegree.D [in Digraph.core.oriented]
OutSelectionOriented.f [in Digraph.core.oriented]
OutSelectionOriented.O [in Digraph.core.oriented]
OutSelection.D [in Digraph.core.oriented]
OutSelection.f [in Digraph.core.oriented]
P
PermOrder.Realize.le_r [in Digraph.core.order]PermOrder.Realize.r [in Digraph.core.order]
PermOrder.Realize.r_total [in Digraph.core.order]
PermOrder.Realize.r_trans [in Digraph.core.order]
PermOrder.Realize.r_irr [in Digraph.core.order]
PermOrder.Realize.s [in Digraph.core.order]
PermOrder.V [in Digraph.core.order]
S
Strong.D [in Digraph.invariants.strong]SubDigraph.D [in Digraph.core.digraph]
SubDigraph.P [in Digraph.core.digraph]
SubOriented.O [in Digraph.core.oriented]
SubOriented.P [in Digraph.core.oriented]
Substitution.H [in Digraph.invariants_advanced.substitution]
Substitution.Hpos [in Digraph.invariants_advanced.substitution]
Substitution.S [in Digraph.invariants_advanced.substitution]
Substitution.Spos [in Digraph.invariants_advanced.substitution]
Substitution.WithOrder.h0 [in Digraph.invariants_advanced.substitution]
Substitution.WithOrder.p [in Digraph.invariants_advanced.substitution]
Substitution.WithOrder.qH [in Digraph.invariants_advanced.substitution]
Substitution.WithOrder.qHE [in Digraph.invariants_advanced.substitution]
Substitution.WithOrder.qS [in Digraph.invariants_advanced.substitution]
Substitution.WithOrder.qSE [in Digraph.invariants_advanced.substitution]
Substitution.WithOrder.rH [in Digraph.invariants_advanced.substitution]
Substitution.WithOrder.rS [in Digraph.invariants_advanced.substitution]
SubTournament.P [in Digraph.core.tournament]
SubTournament.T [in Digraph.core.tournament]
T
TournamentTheory.T [in Digraph.core.tournament]TT.n [in Digraph.core.tournament]
U
UniformDeletion.T [in Digraph.invariants_advanced.transitive]Uniqueness.crit [in Digraph.invariants.critical]
Uniqueness.cyc [in Digraph.invariants.critical]
Uniqueness.del1 [in Digraph.invariants.critical]
Uniqueness.Ntr [in Digraph.invariants.critical]
Uniqueness.ob2 [in Digraph.invariants.critical]
Uniqueness.T [in Digraph.invariants.critical]
Uniqueness.Tpos [in Digraph.invariants.critical]
Z
ZpGroupBridge.p [in Digraph.constructions.circulant]Library Index
A
acn_bandsacn_arc_facts
acn_base
automorphism
C
cayleycells
circulant
ck3_main
coverage
critical
D
digraphdipath
domination
I
interop_graph_theoryin_neighbourhood
K
k4_delk4_lower
k4_main
k4_value
k5_lower
k5_upper
L
lemma7M
mainO
obstructionsomegabar
order
oriented
P
preludeproduct
S
strongsubstitution
T
tournamenttransitive
U
unifiedLemma Index
A
ACdel_pos [in Digraph.applications.k5.k5_lower]ACdel_Ntransb [in Digraph.applications.k5.acn_base]
ACm_pos [in Digraph.applications.k5.k5_lower]
ACm_pos [in Digraph.applications.k4.k4_lower]
ACset_cond [in Digraph.constructions.circulant]
AC_kcritical3 [in Digraph.applications.k5.acn_base]
AC_del_uniform [in Digraph.invariants_advanced.transitive]
AC_mem_Lo_opp [in Digraph.applications.k5.acn_arc_facts]
AC_mem_Lo [in Digraph.applications.k5.acn_arc_facts]
AC_mem_Hi_opp [in Digraph.applications.k5.acn_arc_facts]
AC_mem_Hi [in Digraph.applications.k5.acn_arc_facts]
AC_band_arc [in Digraph.applications.k5.acn_arc_facts]
AC_arc_gt [in Digraph.applications.k5.acn_arc_facts]
AC_arc_lt [in Digraph.applications.k5.acn_arc_facts]
AC_mem_val [in Digraph.applications.k5.acn_arc_facts]
AC_wrapF [in Digraph.applications.acn_bands]
AC_vertex_transitive [in Digraph.constructions.circulant]
AC_arcE [in Digraph.constructions.circulant]
AC_total [in Digraph.constructions.circulant]
AC_irrefl [in Digraph.constructions.circulant]
arcC3E [in Digraph.core.tournament]
arcNarc [in Digraph.core.tournament]
arcTTE [in Digraph.core.tournament]
arcxx [in Digraph.core.tournament]
arc_pair_bound [in Digraph.core.oriented]
arc_xorE [in Digraph.core.tournament]
arc_or [in Digraph.core.tournament]
arc_asym [in Digraph.core.tournament]
arc_neq [in Digraph.core.tournament]
autbP [in Digraph.constructions.automorphism]
autocorr_lo [in Digraph.applications.k5.acn_base]
autocorr_sym [in Digraph.applications.k5.acn_base]
autocorr2 [in Digraph.applications.k5.acn_base]
B
backedgeE [in Digraph.core.order]backedge_qid_dist [in Digraph.applications.k5.acn_base]
backedge_arc_forward [in Digraph.core.order]
backedge_neq [in Digraph.core.order]
backedge_irrefl [in Digraph.core.order]
backedge_sym [in Digraph.core.order]
bands_neq [in Digraph.applications.k5.obstructions]
band_gap [in Digraph.applications.acn_bands]
band_le3 [in Digraph.applications.acn_bands]
band_ge1 [in Digraph.applications.acn_bands]
band1P [in Digraph.applications.acn_bands]
band12P [in Digraph.applications.acn_bands]
band2P [in Digraph.applications.acn_bands]
band3P [in Digraph.applications.acn_bands]
beatc [in Digraph.applications.k5.obstructions]
beat_inner [in Digraph.applications.k5.cells]
beat_blocks [in Digraph.applications.k5.cells]
beat_key [in Digraph.applications.k5.cells]
beat_innerD [in Digraph.applications.k4.k4_del]
beat_blocksD [in Digraph.applications.k4.k4_del]
beat_kd [in Digraph.applications.k4.k4_del]
beat_innerV [in Digraph.applications.k4.k4_value]
beat_blocksV [in Digraph.applications.k4.k4_value]
beat_kv [in Digraph.applications.k4.k4_value]
block_edgeE [in Digraph.invariants_advanced.substitution]
bucket_bound [in Digraph.applications.k5.acn_base]
Builders_1.asymm [in Digraph.core.tournament]
C
cardA [in Digraph.applications.k5.acn_base]cardN0 [in Digraph.applications.k5.acn_base]
card_TT [in Digraph.core.tournament]
card_C3 [in Digraph.core.tournament]
card_le2_transb [in Digraph.core.tournament]
card_lexprod [in Digraph.constructions.product]
card_clique_cidx [in Digraph.applications.k5.cells]
card_T5 [in Digraph.applications.k5.main]
card_shift [in Digraph.applications.k5.acn_base]
card_del [in Digraph.invariants.critical]
card_clique_didx [in Digraph.applications.k4.k4_del]
card_T4 [in Digraph.applications.k4.k4_main]
card_ord_seg [in Digraph.applications.ck3.lemma7]
card_ord_ltn [in Digraph.applications.ck3.lemma7]
card_clique_sidx [in Digraph.applications.k4.k4_value]
card_classes_inj [in Digraph.foundations.prelude]
card_classes [in Digraph.foundations.prelude]
card_AC [in Digraph.constructions.circulant]
cat_dipath_cont [in Digraph.core.dipath]
cat_dipath [in Digraph.core.dipath]
cayley_vertex_transitive [in Digraph.constructions.cayley]
cayley_totalP [in Digraph.constructions.cayley]
cayley_irreflP [in Digraph.constructions.cayley]
cayley_arcE [in Digraph.constructions.cayley]
cidx_inj_clique [in Digraph.applications.k5.cells]
cidx_mono [in Digraph.applications.k5.cells]
cidx_le8 [in Digraph.applications.k5.cells]
cidx_decode [in Digraph.applications.k5.cells]
circulant_arcE [in Digraph.constructions.circulant]
ck_conj1_at_3 [in Digraph.applications.ck3.ck3_main]
ck_conj1_delta3_path [in Digraph.applications.ck3.ck3_main]
ck_conj1_delta3 [in Digraph.applications.ck3.ck3_main]
ck_conj1_delta2 [in Digraph.applications.ck3.lemma7]
ck_theorem4_oriented [in Digraph.applications.ck3.lemma7]
clique_card_le3 [in Digraph.applications.k4.k4_del]
clique_card_le4 [in Digraph.applications.k4.k4_value]
clique_set1 [in Digraph.foundations.interop_graph_theory]
closed_connect [in Digraph.invariants.strong]
conjecture_5_10_at_k5 [in Digraph.applications.k5.main]
conjecture_5_10_at_345 [in Digraph.applications.unified]
conjecture_5_10_at_k3 [in Digraph.applications.unified]
conjecture_5_10_at_k4 [in Digraph.applications.k4.k4_main]
connect_cross [in Digraph.invariants.strong]
connect_induced_closed [in Digraph.invariants.strong]
converse_arcE [in Digraph.core.digraph]
coverage5 [in Digraph.applications.k5.coverage]
cross_edgeE [in Digraph.invariants_advanced.substitution]
C3_Ntransb [in Digraph.core.tournament]
C3_total [in Digraph.core.tournament]
C3_irrefl [in Digraph.core.tournament]
C3_kcritical2 [in Digraph.invariants.critical]
C3_pos [in Digraph.applications.k4.k4_lower]
C3_vertex_transitive [in Digraph.constructions.circulant]
D
dband_le2 [in Digraph.applications.k4.k4_value]dband_ge1 [in Digraph.applications.k4.k4_value]
dband1P [in Digraph.applications.k4.k4_value]
dband2P [in Digraph.applications.k4.k4_value]
del_aut_iso [in Digraph.invariants_advanced.transitive]
dgautE [in Digraph.constructions.automorphism]
dgautM [in Digraph.constructions.automorphism]
dgaut_group_set [in Digraph.constructions.automorphism]
dgaut1 [in Digraph.constructions.automorphism]
dgiso_card [in Digraph.core.digraph]
dgiso_trans [in Digraph.core.digraph]
dgiso_sym [in Digraph.core.digraph]
dgiso_refl [in Digraph.core.digraph]
dicycle_suffix [in Digraph.core.dipath]
dicycle_unroll [in Digraph.core.dipath]
dicycle_prev [in Digraph.core.dipath]
dicycle_next [in Digraph.core.dipath]
dicycle_rot [in Digraph.core.dipath]
didx_inj_clique [in Digraph.applications.k4.k4_del]
dipath_map [in Digraph.core.dipath]
dipath_size [in Digraph.core.dipath]
dipath_arc_nth [in Digraph.core.dipath]
dipath_take [in Digraph.core.dipath]
dipath_drop [in Digraph.core.dipath]
dipath_cons [in Digraph.core.dipath]
dipath_rcons [in Digraph.core.dipath]
dipath_nil [in Digraph.core.dipath]
dipath_uniq [in Digraph.core.dipath]
dipath_path [in Digraph.core.dipath]
disjoint_cycles_path [in Digraph.invariants.strong]
dominatesbP [in Digraph.invariants.domination]
dominatesb_setT [in Digraph.invariants.domination]
domnum_AC_ge3 [in Digraph.applications.k5.acn_base]
domnum_le_omegabar [in Digraph.invariants.domination]
domnum_witness [in Digraph.invariants.domination]
domnum_min [in Digraph.invariants.domination]
E
ellP [in Digraph.core.dipath]ell_induced [in Digraph.core.dipath]
ell_outsel [in Digraph.core.dipath]
ell_embed [in Digraph.core.dipath]
ell_max [in Digraph.core.dipath]
emb_mem [in Digraph.applications.k5.k5_lower]
emb_mem [in Digraph.applications.k4.k4_lower]
endmax_ex [in Digraph.core.dipath]
endmax_dipath [in Digraph.core.dipath]
endmax_closure [in Digraph.core.dipath]
F
f_arc [in Digraph.applications.k5.k5_lower]f_inj [in Digraph.applications.k5.k5_lower]
f_arc [in Digraph.applications.k4.k4_lower]
f_inj [in Digraph.applications.k4.k4_lower]
G
greedy_clique_dom [in Digraph.invariants.domination]gval_bounds [in Digraph.applications.k5.in_neighbourhood]
H
has_dipathP [in Digraph.core.dipath]H17_no_mixed [in Digraph.applications.k5.in_neighbourhood]
H17_side [in Digraph.applications.k5.in_neighbourhood]
H17_dichot [in Digraph.applications.k5.in_neighbourhood]
H17_xrange [in Digraph.applications.k5.in_neighbourhood]
K
kappa_sidx [in Digraph.applications.k4.k4_value]kcriticalP [in Digraph.invariants.critical]
kcritical_proper_sub [in Digraph.invariants.critical]
kcritical2_uniq [in Digraph.invariants.critical]
kcritical2_card3 [in Digraph.invariants.critical]
kd_samesidx [in Digraph.applications.k4.k4_del]
kd_sidx_mono [in Digraph.applications.k4.k4_del]
kd_inj [in Digraph.applications.k4.k4_del]
kernel_S [in Digraph.applications.ck3.lemma7]
kernel_full [in Digraph.applications.ck3.lemma7]
key_samecell [in Digraph.applications.k5.cells]
key_inj [in Digraph.applications.k5.cells]
ksel_card [in Digraph.core.oriented]
ksel_sub [in Digraph.core.oriented]
kv_samekappa [in Digraph.applications.k4.k4_value]
kv_lt_t [in Digraph.applications.k4.k4_value]
kv_kappa_mono [in Digraph.applications.k4.k4_value]
kv_inj [in Digraph.applications.k4.k4_value]
K2_irrefl [in Digraph.foundations.interop_graph_theory]
K2_sym [in Digraph.foundations.interop_graph_theory]
L
last_drop [in Digraph.core.dipath]last_take [in Digraph.core.dipath]
lemma7 [in Digraph.applications.ck3.lemma7]
lexprod_vertex_transitive [in Digraph.constructions.product]
lexprod_total [in Digraph.constructions.product]
lexprod_irrefl [in Digraph.constructions.product]
lexprod_arcE [in Digraph.constructions.product]
le_r_trans [in Digraph.core.order]
le_r_total [in Digraph.core.order]
ltp_pullback [in Digraph.core.order]
ltp_realizeE [in Digraph.core.order]
ltp_asym [in Digraph.core.order]
ltp_total [in Digraph.core.order]
ltp_trans [in Digraph.core.order]
ltp_irrefl [in Digraph.core.order]
M
maxpath_endclosure [in Digraph.core.dipath]maxpath_no_loopback [in Digraph.invariants.strong]
mem_shift [in Digraph.applications.k5.acn_base]
mem_s [in Digraph.core.order]
mem_mid_F [in Digraph.applications.k4.k4_value]
mem_m_F [in Digraph.applications.k4.k4_value]
mem_sub_m_Hi [in Digraph.applications.k5.obstructions]
mem_sub_Hi_m [in Digraph.applications.k5.obstructions]
mem_sub_Hi1_Lo [in Digraph.applications.k5.obstructions]
mem_sub_Lo_Hi1 [in Digraph.applications.k5.obstructions]
mem0A [in Digraph.applications.k5.acn_base]
N
nat_n_split [in Digraph.applications.k5.obstructions]no_short_strong3 [in Digraph.applications.ck3.ck3_main]
no_obstruction [in Digraph.applications.k5.obstructions]
ntransbP [in Digraph.core.tournament]
ntransb_card [in Digraph.core.tournament]
N_out_in_partition [in Digraph.core.tournament]
N_inE [in Digraph.core.tournament]
N_outE [in Digraph.core.tournament]
n_sub_eq_Sm [in Digraph.applications.k4.k4_value]
n_sub_gt_Sm [in Digraph.applications.k4.k4_value]
n_sub_ge_Sm [in Digraph.applications.k4.k4_value]
N0_0 [in Digraph.applications.k5.acn_base]
N0_val_in [in Digraph.applications.k5.acn_base]
O
occdP [in Digraph.applications.k4.k4_del]occP [in Digraph.applications.k5.cells]
occvP [in Digraph.applications.k4.k4_value]
occ_and4F [in Digraph.applications.k5.obstructions]
occ_and3F [in Digraph.applications.k5.obstructions]
occ0134_F [in Digraph.applications.k4.k4_del]
occ023_F [in Digraph.applications.k4.k4_del]
occ124_F [in Digraph.applications.k4.k4_del]
occ24_1F [in Digraph.applications.k4.k4_value]
occ24_5F [in Digraph.applications.k4.k4_value]
occ24_block [in Digraph.applications.k4.k4_value]
occ5310_F [in Digraph.applications.k4.k4_value]
omegabar_Tdel_ge4 [in Digraph.applications.k5.k5_lower]
omegabar_T_ge5 [in Digraph.applications.k5.k5_lower]
omegabar_Tdel_le4 [in Digraph.applications.k5.k5_upper]
omegabar_T_le5 [in Digraph.applications.k5.k5_upper]
omegabar_T5_del [in Digraph.applications.k5.main]
omegabar_T5 [in Digraph.applications.k5.main]
omegabar_AC_del [in Digraph.applications.k5.acn_base]
omegabar_ACdel0 [in Digraph.applications.k5.acn_base]
omegabar_AC [in Digraph.applications.k5.acn_base]
omegabar_ACdel_le2 [in Digraph.applications.k5.acn_base]
omegabar_AC_le3 [in Digraph.applications.k5.acn_base]
omegabar_lexprod_ge [in Digraph.invariants_advanced.substitution]
omegabar_T4del0 [in Digraph.applications.k4.k4_del]
omegabar_T4del_le3 [in Digraph.applications.k4.k4_del]
omegabar_del_vt [in Digraph.invariants_advanced.transitive]
omegabar_T4_del [in Digraph.applications.k4.k4_main]
omegabar_C3 [in Digraph.invariants.omegabar]
omegabar_TT [in Digraph.invariants.omegabar]
omegabar_card_le2 [in Digraph.invariants.omegabar]
omegabar_nil [in Digraph.invariants.omegabar]
omegabar_del [in Digraph.invariants.omegabar]
omegabar_sub [in Digraph.invariants.omegabar]
omegabar_dgiso [in Digraph.invariants.omegabar]
omegabar_embed [in Digraph.invariants.omegabar]
omegabar_transb [in Digraph.invariants.omegabar]
omegabar_le1 [in Digraph.invariants.omegabar]
omegabar_gt0 [in Digraph.invariants.omegabar]
omegabar_witness [in Digraph.invariants.omegabar]
omegabar_min [in Digraph.invariants.omegabar]
omegabar_T4 [in Digraph.applications.k4.k4_value]
omegabar_T4_le4 [in Digraph.applications.k4.k4_value]
omegabar_T4del_ge3 [in Digraph.applications.k4.k4_lower]
omegabar_T4_ge4 [in Digraph.applications.k4.k4_lower]
omegab_at_qd_le4 [in Digraph.applications.k5.k5_upper]
omegab_at_qk_le5 [in Digraph.applications.k5.k5_upper]
omegab_at_q0_le2 [in Digraph.applications.k5.acn_base]
omegab_at_qid_le3 [in Digraph.applications.k5.acn_base]
omegab_at_lexprod_ge [in Digraph.invariants_advanced.substitution]
omegab_at_qd_le3 [in Digraph.applications.k4.k4_del]
omegab_at_le1 [in Digraph.invariants.omegabar]
omegab_at_qv_le4 [in Digraph.applications.k4.k4_value]
omega_K2 [in Digraph.foundations.interop_graph_theory]
omega_hom [in Digraph.foundations.interop_graph_theory]
omega_ge2 [in Digraph.foundations.interop_graph_theory]
omega_le1 [in Digraph.foundations.interop_graph_theory]
omega_le_card [in Digraph.foundations.interop_graph_theory]
omega_ge1 [in Digraph.foundations.interop_graph_theory]
oppA_disjoint [in Digraph.applications.k5.acn_base]
opp_arcs_contra [in Digraph.applications.k5.obstructions]
oriented_card [in Digraph.core.oriented]
oriented_mindeg_card [in Digraph.core.oriented]
oriented_avg_bound [in Digraph.core.oriented]
oriented_arcs_bound [in Digraph.core.oriented]
outdeg_induced [in Digraph.core.oriented]
outdeg_in_sumE [in Digraph.core.oriented]
outdeg_in_mono [in Digraph.core.oriented]
outdeg_in_le [in Digraph.core.oriented]
outdeg_inT [in Digraph.core.oriented]
outdeg_closed [in Digraph.invariants.strong]
outsel_ksel_outdeg [in Digraph.core.oriented]
outsel_asymm [in Digraph.core.oriented]
outsel_irrefl [in Digraph.core.oriented]
outsel_arc_sub [in Digraph.core.oriented]
outsel_arcE [in Digraph.core.oriented]
P
posmin_neq [in Digraph.invariants_advanced.substitution]posmin_le [in Digraph.invariants_advanced.substitution]
pos_inj [in Digraph.invariants_advanced.substitution]
prelude_ssr [in Digraph.foundations.prelude]
prelude_set [in Digraph.foundations.prelude]
prelude_classical [in Digraph.foundations.prelude]
prev_head [in Digraph.core.dipath]
proper_sub_omegabar_le4 [in Digraph.applications.k5.main]
Q
qdE [in Digraph.applications.k4.k4_del]qkE [in Digraph.applications.k5.cells]
quad_D [in Digraph.applications.k5.obstructions]
quad_C [in Digraph.applications.k5.obstructions]
quad_B [in Digraph.applications.k5.obstructions]
quad_A [in Digraph.applications.k5.obstructions]
question_5_9_fails_at_k5 [in Digraph.applications.k5.main]
question_5_9_fails_at_k3 [in Digraph.applications.unified]
question_5_9_fails_at_k4 [in Digraph.applications.k4.k4_main]
qvE [in Digraph.applications.k4.k4_value]
R
radix_eq_inv [in Digraph.applications.acn_bands]radix_lt_inv [in Digraph.applications.acn_bands]
radix_ltA [in Digraph.applications.acn_bands]
rank_lt [in Digraph.core.order]
rd_total [in Digraph.applications.k5.k5_upper]
rd_trans [in Digraph.applications.k5.k5_upper]
rd_irr [in Digraph.applications.k5.k5_upper]
rd_total [in Digraph.applications.k4.k4_del]
rd_trans [in Digraph.applications.k4.k4_del]
rd_irr [in Digraph.applications.k4.k4_del]
reduction [in Digraph.invariants.strong]
repA_band [in Digraph.applications.k5.obstructions]
rep_Z [in Digraph.applications.k5.obstructions]
rep_Lo [in Digraph.applications.k5.obstructions]
rep_Hi [in Digraph.applications.k5.obstructions]
rfun_inj [in Digraph.core.order]
rH_total [in Digraph.invariants_advanced.substitution]
rH_trans [in Digraph.invariants_advanced.substitution]
rH_irr [in Digraph.invariants_advanced.substitution]
rid_total [in Digraph.applications.k5.acn_base]
rid_trans [in Digraph.applications.k5.acn_base]
rid_irr [in Digraph.applications.k5.acn_base]
rk_total [in Digraph.applications.k5.cells]
rk_trans [in Digraph.applications.k5.cells]
rk_irr [in Digraph.applications.k5.cells]
rset_trans [in Digraph.invariants.strong]
rset_closed [in Digraph.invariants.strong]
rset_id [in Digraph.invariants.strong]
rS_total [in Digraph.invariants_advanced.substitution]
rS_trans [in Digraph.invariants_advanced.substitution]
rS_irr [in Digraph.invariants_advanced.substitution]
rv_total [in Digraph.applications.k4.k4_value]
rv_trans [in Digraph.applications.k4.k4_value]
rv_irr [in Digraph.applications.k4.k4_value]
r0_total [in Digraph.applications.k5.acn_base]
r0_trans [in Digraph.applications.k5.acn_base]
r0_irr [in Digraph.applications.k5.acn_base]
S
set1_cliques [in Digraph.foundations.interop_graph_theory]shiftI [in Digraph.applications.k5.acn_base]
shift_comp [in Digraph.applications.k5.acn_base]
shift0 [in Digraph.applications.k5.acn_base]
sidx_del_le4 [in Digraph.applications.k4.k4_del]
sidx_inj_clique [in Digraph.applications.k4.k4_value]
sidx_le5 [in Digraph.applications.k4.k4_value]
sidx_decode [in Digraph.applications.k4.k4_value]
sink_exists [in Digraph.invariants.strong]
size_s [in Digraph.core.order]
sorted_s [in Digraph.core.order]
square [in Digraph.applications.k5.obstructions]
strongb_induced_closed [in Digraph.invariants.strong]
strongP [in Digraph.invariants.strong]
sub_oarc_asymm [in Digraph.core.oriented]
sub_oarc_irrefl [in Digraph.core.oriented]
sub_arc_total [in Digraph.core.tournament]
sub_eq_m [in Digraph.applications.k4.k4_value]
sub_arcE [in Digraph.core.digraph]
T
take_path_last [in Digraph.core.dipath]transbP [in Digraph.core.tournament]
translationE [in Digraph.constructions.cayley]
translation_aut [in Digraph.constructions.cayley]
triple_B [in Digraph.applications.k5.obstructions]
triple_A [in Digraph.applications.k5.obstructions]
TT_transb [in Digraph.core.tournament]
TT_total [in Digraph.core.tournament]
TT_irrefl [in Digraph.core.tournament]
T4_kcritical4 [in Digraph.applications.k4.k4_main]
T4_vertex_transitive [in Digraph.applications.k4.k4_main]
T5_kcritical5 [in Digraph.applications.k5.main]
T5_vertex_transitive [in Digraph.applications.k5.main]
V
vals12 [in Digraph.applications.k4.k4_value]val_zeta [in Digraph.applications.k5.acn_base]
val_sub_gt [in Digraph.applications.k5.acn_arc_facts]
val_sub_le [in Digraph.applications.k5.acn_arc_facts]
val_oppE [in Digraph.applications.k5.acn_arc_facts]
val_addE [in Digraph.applications.k5.acn_arc_facts]
val_Zp_opp [in Digraph.constructions.circulant]
val1 [in Digraph.applications.k5.acn_base]
vertex_transitivebP [in Digraph.constructions.automorphism]
vt_kcritical [in Digraph.invariants_advanced.transitive]
Z
Zp_1gE [in Digraph.constructions.circulant]Zp_invgE [in Digraph.constructions.circulant]
Zp_mulgE [in Digraph.constructions.circulant]
Projection Index
D
DiGraph_IsOriented.arc_asymm [in Digraph.core.oriented]DiGraph_IsOriented.arc_irrefl [in Digraph.core.oriented]
DiGraph_IsTournament.arc_total [in Digraph.core.tournament]
DiGraph_IsTournament.arc_irrefl [in Digraph.core.tournament]
DiGraph.choice_Choice_isCountable_mixin [in Digraph.core.digraph]
DiGraph.choice_hasChoice_mixin [in Digraph.core.digraph]
DiGraph.class [in Digraph.core.digraph]
DiGraph.digraph_HasArc_mixin [in Digraph.core.digraph]
DiGraph.eqtype_hasDecEq_mixin [in Digraph.core.digraph]
DiGraph.fintype_isFinite_mixin [in Digraph.core.digraph]
DiGraph.sort [in Digraph.core.digraph]
H
HasArc.arc [in Digraph.core.digraph]O
Oriented_IsTournament.arc_total [in Digraph.core.tournament]Oriented.choice_Choice_isCountable_mixin [in Digraph.core.oriented]
Oriented.choice_hasChoice_mixin [in Digraph.core.oriented]
Oriented.class [in Digraph.core.oriented]
Oriented.digraph_HasArc_mixin [in Digraph.core.oriented]
Oriented.eqtype_hasDecEq_mixin [in Digraph.core.oriented]
Oriented.fintype_isFinite_mixin [in Digraph.core.oriented]
Oriented.oriented_DiGraph_IsOriented_mixin [in Digraph.core.oriented]
Oriented.sort [in Digraph.core.oriented]
R
RelDigraph.class [in Digraph.core.digraph]RelDigraph.digraph_HasArc_mixin [in Digraph.core.digraph]
RelDigraph.sort [in Digraph.core.digraph]
T
Tournament.choice_Choice_isCountable_mixin [in Digraph.core.tournament]Tournament.choice_hasChoice_mixin [in Digraph.core.tournament]
Tournament.class [in Digraph.core.tournament]
Tournament.digraph_HasArc_mixin [in Digraph.core.tournament]
Tournament.eqtype_hasDecEq_mixin [in Digraph.core.tournament]
Tournament.fintype_isFinite_mixin [in Digraph.core.tournament]
Tournament.oriented_DiGraph_IsOriented_mixin [in Digraph.core.tournament]
Tournament.sort [in Digraph.core.tournament]
Tournament.tournament_Oriented_IsTournament_mixin [in Digraph.core.tournament]
Section Index
A
AC [in Digraph.constructions.circulant]ACBase [in Digraph.applications.k5.acn_base]
AcnBands [in Digraph.applications.acn_bands]
ArcFacts [in Digraph.applications.k5.acn_arc_facts]
Automorphism [in Digraph.constructions.automorphism]
B
Backedge [in Digraph.core.order]Builders_1.Builders_1.Builders_1 [in Digraph.core.tournament]
C
Cayley [in Digraph.constructions.cayley]Cells [in Digraph.applications.k5.cells]
Cells.InClique [in Digraph.applications.k5.cells]
CKDefs [in Digraph.applications.ck3.lemma7]
C3 [in Digraph.core.tournament]
D
DiGraph_IsOriented.DiGraph_IsOriented.DiGraph_IsOriented [in Digraph.core.oriented]DiGraph_IsTournament.DiGraph_IsTournament.DiGraph_IsTournament [in Digraph.core.tournament]
DiPathDef [in Digraph.core.dipath]
Domination [in Digraph.invariants.domination]
H
HasArc.HasArc.HasArc [in Digraph.core.digraph]hb_instance_11.hb_instance_11 [in Digraph.core.digraph]
hb_instance_1.hb_instance_1 [in Digraph.core.digraph]
H17 [in Digraph.applications.k5.in_neighbourhood]
K
Kernel [in Digraph.applications.ck3.lemma7]KSelection [in Digraph.core.oriented]
K4Del [in Digraph.applications.k4.k4_del]
K4Del.InCliqueD [in Digraph.applications.k4.k4_del]
K4Lower [in Digraph.applications.k4.k4_lower]
K4Value [in Digraph.applications.k4.k4_value]
K4Value.InCliqueV [in Digraph.applications.k4.k4_value]
K5Lower [in Digraph.applications.k5.k5_lower]
K5Upper [in Digraph.applications.k5.k5_upper]
L
LexProd [in Digraph.constructions.product]LexProdTournament [in Digraph.constructions.product]
LexProdVT [in Digraph.constructions.product]
M
Main [in Digraph.applications.k5.main]Main [in Digraph.applications.k4.k4_main]
O
Obstructions [in Digraph.applications.k5.obstructions]Obstructions.WithClique [in Digraph.applications.k5.obstructions]
OmegaBarBasics [in Digraph.invariants.omegabar]
OmegaFacts [in Digraph.foundations.interop_graph_theory]
OrientedCounting [in Digraph.core.oriented]
Oriented_IsTournament.Oriented_IsTournament.Oriented_IsTournament [in Digraph.core.tournament]
OutDegree [in Digraph.core.oriented]
OutSelection [in Digraph.core.oriented]
OutSelectionOriented [in Digraph.core.oriented]
P
PermOrder [in Digraph.core.order]PermOrder.Realize [in Digraph.core.order]
S
Strong [in Digraph.invariants.strong]SubDigraph [in Digraph.core.digraph]
SubOriented [in Digraph.core.oriented]
Substitution [in Digraph.invariants_advanced.substitution]
Substitution.WithOrder [in Digraph.invariants_advanced.substitution]
SubTournament [in Digraph.core.tournament]
T
TournamentTheory [in Digraph.core.tournament]TT [in Digraph.core.tournament]
U
UniformDeletion [in Digraph.invariants_advanced.transitive]Uniqueness [in Digraph.invariants.critical]
Z
ZpGroupBridge [in Digraph.constructions.circulant]Abbreviation Index
A
ACdel [in Digraph.applications.k5.acn_base]ACm [in Digraph.applications.k5.k5_lower]
ACm [in Digraph.applications.k5.k5_upper]
ACm [in Digraph.applications.k5.cells]
ACm [in Digraph.applications.k5.main]
ACm [in Digraph.applications.k5.acn_base]
ACm [in Digraph.applications.k4.k4_del]
ACm [in Digraph.applications.k4.k4_main]
ACm [in Digraph.applications.k4.k4_value]
ACm [in Digraph.applications.k5.obstructions]
ACm [in Digraph.applications.k4.k4_lower]
ACm [in Digraph.applications.k5.acn_arc_facts]
B
Builders_1.arc_total [in Digraph.core.tournament]Builders_1.arc_irrefl [in Digraph.core.tournament]
C
C3t [in Digraph.applications.k4.k4_del]C3t [in Digraph.applications.k4.k4_main]
C3t [in Digraph.applications.k4.k4_value]
C3t [in Digraph.applications.k4.k4_lower]
D
DiGraph [in Digraph.core.digraph]DiGraph_IsOriented [in Digraph.core.oriented]
DiGraph_IsOriented.axioms [in Digraph.core.oriented]
DiGraph_IsOriented.Build [in Digraph.core.oriented]
DiGraph_IsTournament [in Digraph.core.tournament]
DiGraph_IsTournament.axioms [in Digraph.core.tournament]
DiGraph_IsTournament.Build [in Digraph.core.tournament]
DiGraph.clone [in Digraph.core.digraph]
DiGraph.copy [in Digraph.core.digraph]
DiGraph.Exports.diGraphType [in Digraph.core.digraph]
DiGraph.on [in Digraph.core.digraph]
DiGraph.on_ [in Digraph.core.digraph]
H
HasArc [in Digraph.core.digraph]HasArc.axioms [in Digraph.core.digraph]
HasArc.Build [in Digraph.core.digraph]
L
L [in Digraph.applications.ck3.lemma7]M
m [in Digraph.applications.k5.k5_lower]m [in Digraph.applications.k5.k5_upper]
m [in Digraph.applications.k5.cells]
m [in Digraph.applications.k5.main]
m [in Digraph.applications.k5.acn_base]
m [in Digraph.applications.k4.k4_del]
m [in Digraph.applications.k4.k4_main]
m [in Digraph.applications.k4.k4_value]
m [in Digraph.applications.k5.obstructions]
m [in Digraph.applications.k4.k4_lower]
m [in Digraph.applications.k5.acn_arc_facts]
m [in Digraph.applications.acn_bands]
m [in Digraph.applications.k5.in_neighbourhood]
m [in Digraph.constructions.circulant]
N
n [in Digraph.applications.k5.k5_lower]n [in Digraph.applications.k5.k5_upper]
n [in Digraph.applications.k5.cells]
n [in Digraph.applications.k5.main]
n [in Digraph.applications.k5.acn_base]
n [in Digraph.applications.k4.k4_del]
n [in Digraph.applications.k4.k4_main]
n [in Digraph.applications.k4.k4_value]
n [in Digraph.applications.k5.obstructions]
n [in Digraph.applications.k4.k4_lower]
n [in Digraph.applications.k5.acn_arc_facts]
n [in Digraph.applications.acn_bands]
n [in Digraph.applications.k5.in_neighbourhood]
n [in Digraph.constructions.circulant]
O
Oriented [in Digraph.core.oriented]Oriented_IsTournament [in Digraph.core.tournament]
Oriented_IsTournament.axioms [in Digraph.core.tournament]
Oriented_IsTournament.Build [in Digraph.core.tournament]
Oriented.clone [in Digraph.core.oriented]
Oriented.copy [in Digraph.core.oriented]
Oriented.Exports.orientedDigraph [in Digraph.core.oriented]
Oriented.on [in Digraph.core.oriented]
Oriented.on_ [in Digraph.core.oriented]
P
pos [in Digraph.invariants_advanced.substitution]R
RelDigraph [in Digraph.core.digraph]RelDigraph.clone [in Digraph.core.digraph]
RelDigraph.copy [in Digraph.core.digraph]
RelDigraph.Exports.relDigraph [in Digraph.core.digraph]
RelDigraph.on [in Digraph.core.digraph]
RelDigraph.on_ [in Digraph.core.digraph]
T
Tournament [in Digraph.core.tournament]Tournament.clone [in Digraph.core.tournament]
Tournament.copy [in Digraph.core.tournament]
Tournament.Exports.tournament [in Digraph.core.tournament]
Tournament.on [in Digraph.core.tournament]
Tournament.on_ [in Digraph.core.tournament]
tv [in Digraph.applications.k4.k4_del]
T4 [in Digraph.applications.k4.k4_del]
T4 [in Digraph.applications.k4.k4_main]
T4 [in Digraph.applications.k4.k4_value]
T4 [in Digraph.applications.k4.k4_lower]
T4del [in Digraph.applications.k4.k4_del]
T5 [in Digraph.applications.k5.k5_lower]
T5 [in Digraph.applications.k5.k5_upper]
T5 [in Digraph.applications.k5.cells]
T5 [in Digraph.applications.k5.main]
T5 [in Digraph.applications.k5.obstructions]
T5del [in Digraph.applications.k5.k5_upper]
Definition Index
A
AC [in Digraph.constructions.circulant]ACset [in Digraph.constructions.circulant]
arc [in Digraph.core.digraph]
arc_asymm [in Digraph.core.oriented]
arc_irrefl [in Digraph.core.oriented]
arc_total [in Digraph.core.tournament]
arc_closed [in Digraph.invariants.strong]
autb [in Digraph.constructions.automorphism]
B
backedge [in Digraph.core.order]backedge_rel [in Digraph.core.order]
band [in Digraph.applications.acn_bands]
Builders_1.Builders_1_V__canonical__tournament_Tournament [in Digraph.core.tournament]
Builders_1.HB_unnamed_factory_5 [in Digraph.core.tournament]
Builders_1.Builders_1_V__canonical__oriented_Oriented [in Digraph.core.tournament]
Builders_1.HB_unnamed_factory_3 [in Digraph.core.tournament]
Builders_1.Builders_1_V__canonical__digraph_DiGraph [in Digraph.core.tournament]
Builders_1.Builders_1_V__canonical__fintype_Finite [in Digraph.core.tournament]
Builders_1.Builders_1_V__canonical__choice_Countable [in Digraph.core.tournament]
Builders_1.Builders_1_V__canonical__choice_Choice [in Digraph.core.tournament]
Builders_1.Builders_1_V__canonical__eqtype_Equality [in Digraph.core.tournament]
Builders_1.Builders_1_V__canonical__digraph_RelDigraph [in Digraph.core.tournament]
C
cayley [in Digraph.constructions.cayley]cayley_cayley__canonical__digraph_DiGraph [in Digraph.constructions.cayley]
cayley_cayley__canonical__digraph_RelDigraph [in Digraph.constructions.cayley]
cayley_cayley__canonical__fintype_Finite [in Digraph.constructions.cayley]
cayley_cayley__canonical__choice_Countable [in Digraph.constructions.cayley]
cayley_cayley__canonical__choice_Choice [in Digraph.constructions.cayley]
cayley_cayley__canonical__eqtype_Equality [in Digraph.constructions.cayley]
cayley_cayley__canonical__tournament_Tournament [in Digraph.constructions.circulant]
cayley_cayley__canonical__oriented_Oriented [in Digraph.constructions.circulant]
cidx [in Digraph.applications.k5.cells]
ckB [in Digraph.applications.ck3.lemma7]
ckC [in Digraph.applications.ck3.lemma7]
ckCset [in Digraph.applications.ck3.lemma7]
ckS [in Digraph.applications.ck3.lemma7]
converse [in Digraph.core.digraph]
C3 [in Digraph.core.tournament]
D
dband [in Digraph.applications.k4.k4_value]del_tournament [in Digraph.core.tournament]
del_vertex [in Digraph.core.digraph]
dgaut [in Digraph.constructions.automorphism]
dgaut_group [in Digraph.constructions.automorphism]
dgiso [in Digraph.core.digraph]
dicycle [in Digraph.core.dipath]
DiGraph_IsOriented.identity_builder [in Digraph.core.oriented]
DiGraph_IsOriented.phant_axioms [in Digraph.core.oriented]
DiGraph_IsOriented.phant_Build [in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented_V__canonical__digraph_DiGraph [in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented_V__canonical__fintype_Finite [in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented_V__canonical__choice_Countable [in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented_V__canonical__choice_Choice [in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented_V__canonical__eqtype_Equality [in Digraph.core.oriented]
DiGraph_IsOriented.DiGraph_IsOriented_V__canonical__digraph_RelDigraph [in Digraph.core.oriented]
DiGraph_IsTournament.phant_axioms [in Digraph.core.tournament]
DiGraph_IsTournament.phant_Build [in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament_V__canonical__digraph_DiGraph [in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament_V__canonical__fintype_Finite [in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament_V__canonical__choice_Countable [in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament_V__canonical__choice_Choice [in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament_V__canonical__eqtype_Equality [in Digraph.core.tournament]
DiGraph_IsTournament.DiGraph_IsTournament_V__canonical__digraph_RelDigraph [in Digraph.core.tournament]
digraph_converse__canonical__digraph_DiGraph [in Digraph.core.digraph]
digraph_converse__canonical__digraph_RelDigraph [in Digraph.core.digraph]
digraph_converse__canonical__fintype_Finite [in Digraph.core.digraph]
digraph_converse__canonical__choice_Countable [in Digraph.core.digraph]
digraph_converse__canonical__choice_Choice [in Digraph.core.digraph]
digraph_converse__canonical__eqtype_Equality [in Digraph.core.digraph]
DiGraph.Exports.digraph_DiGraph__to__fintype_Finite [in Digraph.core.digraph]
DiGraph.Exports.digraph_DiGraph_class__to__fintype_Finite_class [in Digraph.core.digraph]
DiGraph.Exports.digraph_DiGraph__to__choice_Countable [in Digraph.core.digraph]
DiGraph.Exports.digraph_DiGraph_class__to__choice_Countable_class [in Digraph.core.digraph]
DiGraph.Exports.digraph_DiGraph__to__choice_Choice [in Digraph.core.digraph]
DiGraph.Exports.digraph_DiGraph_class__to__choice_Choice_class [in Digraph.core.digraph]
DiGraph.Exports.digraph_DiGraph__to__eqtype_Equality [in Digraph.core.digraph]
DiGraph.Exports.digraph_DiGraph_class__to__eqtype_Equality_class [in Digraph.core.digraph]
DiGraph.Exports.digraph_DiGraph__to__digraph_RelDigraph [in Digraph.core.digraph]
DiGraph.Exports.digraph_DiGraph_class__to__digraph_RelDigraph_class [in Digraph.core.digraph]
DiGraph.Exports.join_digraph_DiGraph_between_fintype_Finite_and_digraph_RelDigraph [in Digraph.core.digraph]
DiGraph.Exports.join_digraph_DiGraph_between_choice_Countable_and_digraph_RelDigraph [in Digraph.core.digraph]
DiGraph.Exports.join_digraph_DiGraph_between_choice_Choice_and_digraph_RelDigraph [in Digraph.core.digraph]
DiGraph.Exports.join_digraph_DiGraph_between_eqtype_Equality_and_digraph_RelDigraph [in Digraph.core.digraph]
DiGraph.pack_ [in Digraph.core.digraph]
DiGraph.phant_on_ [in Digraph.core.digraph]
DiGraph.phant_clone [in Digraph.core.digraph]
dipath [in Digraph.core.dipath]
dominatesb [in Digraph.invariants.domination]
domnum [in Digraph.invariants.domination]
E
ell [in Digraph.core.dipath]endmax [in Digraph.core.dipath]
F
fintype_Finite__to__fintype_isFinite [in Digraph.core.oriented]fintype_Finite__to__eqtype_hasDecEq [in Digraph.core.oriented]
fintype_Finite__to__choice_Choice_isCountable [in Digraph.core.oriented]
fintype_Finite__to__choice_hasChoice [in Digraph.core.oriented]
fintype_Finite__to__fintype_isFinite__34 [in Digraph.core.tournament]
fintype_Finite__to__eqtype_hasDecEq__32 [in Digraph.core.tournament]
fintype_Finite__to__choice_Choice_isCountable__30 [in Digraph.core.tournament]
fintype_Finite__to__choice_hasChoice__28 [in Digraph.core.tournament]
fintype_Finite__to__fintype_isFinite [in Digraph.core.tournament]
fintype_Finite__to__eqtype_hasDecEq [in Digraph.core.tournament]
fintype_Finite__to__choice_Choice_isCountable [in Digraph.core.tournament]
fintype_Finite__to__choice_hasChoice [in Digraph.core.tournament]
fintype_Finite__to__fintype_isFinite [in Digraph.constructions.product]
fintype_Finite__to__eqtype_hasDecEq [in Digraph.constructions.product]
fintype_Finite__to__choice_Choice_isCountable [in Digraph.constructions.product]
fintype_Finite__to__choice_hasChoice [in Digraph.constructions.product]
fintype_Finite__to__fintype_isFinite [in Digraph.constructions.cayley]
fintype_Finite__to__eqtype_hasDecEq [in Digraph.constructions.cayley]
fintype_Finite__to__choice_Choice_isCountable [in Digraph.constructions.cayley]
fintype_Finite__to__choice_hasChoice [in Digraph.constructions.cayley]
fintype_Finite__to__fintype_isFinite [in Digraph.core.digraph]
fintype_Finite__to__eqtype_hasDecEq [in Digraph.core.digraph]
fintype_Finite__to__choice_Choice_isCountable [in Digraph.core.digraph]
fintype_Finite__to__choice_hasChoice [in Digraph.core.digraph]
H
HasArc.identity_builder [in Digraph.core.digraph]HasArc.phant_axioms [in Digraph.core.digraph]
HasArc.phant_Build [in Digraph.core.digraph]
has_dipath [in Digraph.core.dipath]
HB_unnamed_factory_14 [in Digraph.core.oriented]
HB_unnamed_factory_12 [in Digraph.core.oriented]
HB_unnamed_mixin_11 [in Digraph.core.oriented]
HB_unnamed_mixin_10 [in Digraph.core.oriented]
HB_unnamed_mixin_9 [in Digraph.core.oriented]
HB_unnamed_mixin_8 [in Digraph.core.oriented]
HB_unnamed_factory_3 [in Digraph.core.oriented]
HB_unnamed_factory_1 [in Digraph.core.oriented]
HB_unnamed_mixin_47 [in Digraph.core.tournament]
HB_unnamed_mixin_46 [in Digraph.core.tournament]
HB_unnamed_factory_41 [in Digraph.core.tournament]
HB_unnamed_factory_39 [in Digraph.core.tournament]
HB_unnamed_mixin_38 [in Digraph.core.tournament]
HB_unnamed_mixin_37 [in Digraph.core.tournament]
HB_unnamed_mixin_36 [in Digraph.core.tournament]
HB_unnamed_mixin_35 [in Digraph.core.tournament]
HB_unnamed_factory_26 [in Digraph.core.tournament]
HB_unnamed_mixin_25 [in Digraph.core.tournament]
HB_unnamed_mixin_24 [in Digraph.core.tournament]
HB_unnamed_factory_21 [in Digraph.core.tournament]
HB_unnamed_factory_19 [in Digraph.core.tournament]
HB_unnamed_mixin_18 [in Digraph.core.tournament]
HB_unnamed_mixin_17 [in Digraph.core.tournament]
HB_unnamed_mixin_16 [in Digraph.core.tournament]
HB_unnamed_mixin_15 [in Digraph.core.tournament]
HB_unnamed_factory_10 [in Digraph.core.tournament]
HB_unnamed_factory_8 [in Digraph.core.tournament]
HB_unnamed_mixin_16 [in Digraph.constructions.product]
HB_unnamed_mixin_15 [in Digraph.constructions.product]
HB_unnamed_factory_12 [in Digraph.constructions.product]
HB_unnamed_factory_10 [in Digraph.constructions.product]
HB_unnamed_mixin_9 [in Digraph.constructions.product]
HB_unnamed_mixin_8 [in Digraph.constructions.product]
HB_unnamed_mixin_7 [in Digraph.constructions.product]
HB_unnamed_mixin_6 [in Digraph.constructions.product]
HB_unnamed_factory_1 [in Digraph.constructions.product]
HB_unnamed_factory_10 [in Digraph.constructions.cayley]
HB_unnamed_mixin_9 [in Digraph.constructions.cayley]
HB_unnamed_mixin_8 [in Digraph.constructions.cayley]
HB_unnamed_mixin_7 [in Digraph.constructions.cayley]
HB_unnamed_mixin_6 [in Digraph.constructions.cayley]
HB_unnamed_factory_1 [in Digraph.constructions.cayley]
HB_unnamed_factory_14 [in Digraph.core.digraph]
HB_unnamed_factory_12 [in Digraph.core.digraph]
HB_unnamed_mixin_10 [in Digraph.core.digraph]
HB_unnamed_mixin_9 [in Digraph.core.digraph]
HB_unnamed_mixin_8 [in Digraph.core.digraph]
HB_unnamed_mixin_7 [in Digraph.core.digraph]
HB_unnamed_factory_2 [in Digraph.core.digraph]
HB_unnamed_mixin_5 [in Digraph.constructions.circulant]
HB_unnamed_mixin_4 [in Digraph.constructions.circulant]
HB_unnamed_factory_1 [in Digraph.constructions.circulant]
hmin [in Digraph.invariants_advanced.substitution]
I
induced_oriented [in Digraph.core.oriented]induced_digraph [in Digraph.core.digraph]
K
kappa [in Digraph.applications.k4.k4_value]kcritical [in Digraph.invariants.critical]
kd [in Digraph.applications.k4.k4_del]
key [in Digraph.applications.k5.cells]
ksel [in Digraph.core.oriented]
kv [in Digraph.applications.k4.k4_value]
K2 [in Digraph.foundations.interop_graph_theory]
K2_rel [in Digraph.foundations.interop_graph_theory]
L
lexprod [in Digraph.constructions.product]lexprod_tournament [in Digraph.constructions.product]
ltp [in Digraph.core.order]
N
N_in [in Digraph.core.tournament]N_out [in Digraph.core.tournament]
O
obstrb [in Digraph.applications.k5.obstructions]occ [in Digraph.applications.k5.cells]
occd [in Digraph.applications.k4.k4_del]
occv [in Digraph.applications.k4.k4_value]
omegabar [in Digraph.invariants.omegabar]
omegab_at [in Digraph.invariants.omegabar]
oriented_outsel__canonical__oriented_Oriented [in Digraph.core.oriented]
oriented_outsel__canonical__digraph_DiGraph [in Digraph.core.oriented]
oriented_outsel__canonical__digraph_RelDigraph [in Digraph.core.oriented]
oriented_outsel__canonical__fintype_Finite [in Digraph.core.oriented]
oriented_outsel__canonical__choice_Countable [in Digraph.core.oriented]
oriented_outsel__canonical__choice_Choice [in Digraph.core.oriented]
oriented_outsel__canonical__eqtype_Equality [in Digraph.core.oriented]
Oriented_IsTournament.identity_builder [in Digraph.core.tournament]
Oriented_IsTournament.phant_axioms [in Digraph.core.tournament]
Oriented_IsTournament.phant_Build [in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament_V__canonical__oriented_Oriented [in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament_V__canonical__digraph_DiGraph [in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament_V__canonical__fintype_Finite [in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament_V__canonical__choice_Countable [in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament_V__canonical__choice_Choice [in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament_V__canonical__eqtype_Equality [in Digraph.core.tournament]
Oriented_IsTournament.Oriented_IsTournament_V__canonical__digraph_RelDigraph [in Digraph.core.tournament]
Oriented.Exports.oriented_Oriented__to__digraph_DiGraph [in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented_class__to__digraph_DiGraph_class [in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented__to__fintype_Finite [in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented_class__to__fintype_Finite_class [in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented__to__choice_Countable [in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented_class__to__choice_Countable_class [in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented__to__choice_Choice [in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented_class__to__choice_Choice_class [in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented__to__eqtype_Equality [in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented_class__to__eqtype_Equality_class [in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented__to__digraph_RelDigraph [in Digraph.core.oriented]
Oriented.Exports.oriented_Oriented_class__to__digraph_RelDigraph_class [in Digraph.core.oriented]
Oriented.pack_ [in Digraph.core.oriented]
Oriented.phant_on_ [in Digraph.core.oriented]
Oriented.phant_clone [in Digraph.core.oriented]
outdeg [in Digraph.core.oriented]
outdeg_in [in Digraph.core.oriented]
outsel [in Digraph.core.oriented]
P
posmin [in Digraph.invariants_advanced.substitution]product_lexprod__canonical__tournament_Tournament [in Digraph.constructions.product]
product_lexprod__canonical__oriented_Oriented [in Digraph.constructions.product]
product_lexprod__canonical__digraph_DiGraph [in Digraph.constructions.product]
product_lexprod__canonical__digraph_RelDigraph [in Digraph.constructions.product]
product_lexprod__canonical__fintype_Finite [in Digraph.constructions.product]
product_lexprod__canonical__choice_Countable [in Digraph.constructions.product]
product_lexprod__canonical__choice_Choice [in Digraph.constructions.product]
product_lexprod__canonical__eqtype_Equality [in Digraph.constructions.product]
Q
qd [in Digraph.applications.k4.k4_del]qk [in Digraph.applications.k5.cells]
qv [in Digraph.applications.k4.k4_value]
R
realize [in Digraph.core.order]RelDigraph.pack_ [in Digraph.core.digraph]
RelDigraph.phant_on_ [in Digraph.core.digraph]
RelDigraph.phant_clone [in Digraph.core.digraph]
rfun [in Digraph.core.order]
rk [in Digraph.applications.k5.cells]
rset [in Digraph.invariants.strong]
rv [in Digraph.applications.k4.k4_value]
S
sidx [in Digraph.applications.k4.k4_value]Specif_sig__canonical__oriented_Oriented [in Digraph.core.oriented]
Specif_sig__canonical__tournament_Tournament [in Digraph.core.tournament]
Specif_sig__canonical__digraph_DiGraph [in Digraph.core.digraph]
Specif_sig__canonical__digraph_RelDigraph [in Digraph.core.digraph]
strongb [in Digraph.invariants.strong]
sub_tournament [in Digraph.core.tournament]
T
tournament_TT__canonical__tournament_Tournament [in Digraph.core.tournament]tournament_TT__canonical__oriented_Oriented [in Digraph.core.tournament]
tournament_DiGraph_IsTournament__to__oriented_DiGraph_IsOriented__45 [in Digraph.core.tournament]
tournament_DiGraph_IsTournament__to__tournament_Oriented_IsTournament__43 [in Digraph.core.tournament]
tournament_TT__canonical__digraph_DiGraph [in Digraph.core.tournament]
tournament_TT__canonical__digraph_RelDigraph [in Digraph.core.tournament]
tournament_TT__canonical__fintype_Finite [in Digraph.core.tournament]
tournament_TT__canonical__choice_Countable [in Digraph.core.tournament]
tournament_TT__canonical__choice_Choice [in Digraph.core.tournament]
tournament_TT__canonical__eqtype_Equality [in Digraph.core.tournament]
tournament_C3__canonical__tournament_Tournament [in Digraph.core.tournament]
tournament_C3__canonical__oriented_Oriented [in Digraph.core.tournament]
tournament_DiGraph_IsTournament__to__oriented_DiGraph_IsOriented [in Digraph.core.tournament]
tournament_DiGraph_IsTournament__to__tournament_Oriented_IsTournament [in Digraph.core.tournament]
tournament_C3__canonical__digraph_DiGraph [in Digraph.core.tournament]
tournament_C3__canonical__digraph_RelDigraph [in Digraph.core.tournament]
tournament_C3__canonical__fintype_Finite [in Digraph.core.tournament]
tournament_C3__canonical__choice_Countable [in Digraph.core.tournament]
tournament_C3__canonical__choice_Choice [in Digraph.core.tournament]
tournament_C3__canonical__eqtype_Equality [in Digraph.core.tournament]
tournament_DiGraph_IsTournament__to__oriented_DiGraph_IsOriented [in Digraph.constructions.product]
tournament_DiGraph_IsTournament__to__tournament_Oriented_IsTournament [in Digraph.constructions.product]
tournament_DiGraph_IsTournament__to__oriented_DiGraph_IsOriented [in Digraph.constructions.circulant]
tournament_DiGraph_IsTournament__to__tournament_Oriented_IsTournament [in Digraph.constructions.circulant]
Tournament.Exports.tournament_Tournament__to__oriented_Oriented [in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament_class__to__oriented_Oriented_class [in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament__to__digraph_DiGraph [in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament_class__to__digraph_DiGraph_class [in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament__to__fintype_Finite [in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament_class__to__fintype_Finite_class [in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament__to__choice_Countable [in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament_class__to__choice_Countable_class [in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament__to__choice_Choice [in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament_class__to__choice_Choice_class [in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament__to__eqtype_Equality [in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament_class__to__eqtype_Equality_class [in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament__to__digraph_RelDigraph [in Digraph.core.tournament]
Tournament.Exports.tournament_Tournament_class__to__digraph_RelDigraph_class [in Digraph.core.tournament]
Tournament.pack_ [in Digraph.core.tournament]
Tournament.phant_on_ [in Digraph.core.tournament]
Tournament.phant_clone [in Digraph.core.tournament]
to_GT [in Digraph.core.digraph]
transb [in Digraph.core.tournament]
translation [in Digraph.constructions.cayley]
TT [in Digraph.core.tournament]
V
vertex_transitiveb [in Digraph.constructions.automorphism]Record Index
D
DiGraph_IsOriented.axioms_ [in Digraph.core.oriented]DiGraph_IsTournament.axioms_ [in Digraph.core.tournament]
DiGraph.axioms_ [in Digraph.core.digraph]
DiGraph.type [in Digraph.core.digraph]
H
HasArc.axioms_ [in Digraph.core.digraph]O
Oriented_IsTournament.axioms_ [in Digraph.core.tournament]Oriented.axioms_ [in Digraph.core.oriented]
Oriented.type [in Digraph.core.oriented]
R
RelDigraph.axioms_ [in Digraph.core.digraph]RelDigraph.type [in Digraph.core.digraph]
T
Tournament.axioms_ [in Digraph.core.tournament]Tournament.type [in Digraph.core.tournament]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1184 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (23 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (224 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (34 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (405 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (33 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (56 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (96 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (299 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
This page has been generated by coqdoc