| 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 | (355 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 | (25 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 | (93 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 | (4 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 | (124 entries) |
| Constructor 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) |
| 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 | (9 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 | (26 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 | (70 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 | (2 entries) |
Global Index
A
alpha [definition, in DomTheory.dom]alpha_eq_1 [lemma, in DomTheory.example]
alpha_w_eq_wh [lemma, in DomTheory.example]
alpha_leq_Gamma [lemma, in DomTheory.dom]
alpha_is_alpha1 [lemma, in DomTheory.dom]
alpha_w_leq_Gamma_w [lemma, in DomTheory.dom]
alpha_w [definition, in DomTheory.dom]
B
basics [library]Basic_Facts_Neighborhoods.D2 [variable, in DomTheory.basics]
Basic_Facts_Neighborhoods.D1 [variable, in DomTheory.basics]
Basic_Facts_Neighborhoods.G [variable, in DomTheory.basics]
Basic_Facts_Neighborhoods [section, in DomTheory.basics]
C
card_weight_1 [lemma, in DomTheory.dom]closed_neigh_set_subset [lemma, in DomTheory.basics]
closed_neigh_set [definition, in DomTheory.basics]
closed_neigh [definition, in DomTheory.basics]
clsg_clneigh [lemma, in DomTheory.basics]
cl_sg_refl [lemma, in DomTheory.basics]
cl_sg_sym [lemma, in DomTheory.basics]
cl_sedge [definition, in DomTheory.basics]
D
deg [definition, in DomTheory.basics]deg_minus_uv2 [lemma, in DomTheory.basics]
deg_minus_uv1 [lemma, in DomTheory.basics]
deg_minus_uv0 [lemma, in DomTheory.basics]
deg_isolate_graph [lemma, in DomTheory.basics]
dom [library]
dominated_belongs_to_closed_neigh_set [lemma, in DomTheory.basics]
dominated_belongs_to_open_neigh_set [lemma, in DomTheory.basics]
dominating [definition, in DomTheory.dom]
dominatingP [lemma, in DomTheory.dom]
Domination_Theory.Classic_domination_parameters.maximum_irr [variable, in DomTheory.dom]
Domination_Theory.Classic_domination_parameters.maximum_minimal_dom [variable, in DomTheory.dom]
Domination_Theory.Classic_domination_parameters.maximum_st [variable, in DomTheory.dom]
Domination_Theory.Classic_domination_parameters.minimum_st_dom [variable, in DomTheory.dom]
Domination_Theory.Classic_domination_parameters.minimum_dom [variable, in DomTheory.dom]
Domination_Theory.Classic_domination_parameters.minimum_maximal_irr [variable, in DomTheory.dom]
Domination_Theory.Classic_domination_parameters [section, in DomTheory.dom]
Domination_Theory.Argument_unweighted_sets.pbF [variable, in DomTheory.dom]
Domination_Theory.Argument_unweighted_sets.pF [variable, in DomTheory.dom]
Domination_Theory.Argument_unweighted_sets.F [variable, in DomTheory.dom]
Domination_Theory.Argument_unweighted_sets.pP [variable, in DomTheory.dom]
Domination_Theory.Argument_unweighted_sets.pb [variable, in DomTheory.dom]
Domination_Theory.Argument_unweighted_sets.p [variable, in DomTheory.dom]
Domination_Theory.Argument_unweighted_sets [section, in DomTheory.dom]
Domination_Theory.Unweighted_Sets.D [variable, in DomTheory.dom]
Domination_Theory.Unweighted_Sets.p [variable, in DomTheory.dom]
Domination_Theory.Unweighted_Sets [section, in DomTheory.dom]
Domination_Theory.Weighted_domination_parameters.maximum_irr [variable, in DomTheory.dom]
Domination_Theory.Weighted_domination_parameters.maximum_minimal_dom [variable, in DomTheory.dom]
Domination_Theory.Weighted_domination_parameters.maximum_st [variable, in DomTheory.dom]
Domination_Theory.Weighted_domination_parameters.minimum_st_dom [variable, in DomTheory.dom]
Domination_Theory.Weighted_domination_parameters.minimum_dom [variable, in DomTheory.dom]
Domination_Theory.Weighted_domination_parameters.minimum_maximal_irr [variable, in DomTheory.dom]
Domination_Theory.Weighted_domination_parameters.positive_weights [variable, in DomTheory.dom]
Domination_Theory.Weighted_domination_parameters.weight [variable, in DomTheory.dom]
Domination_Theory.Weighted_domination_parameters [section, in DomTheory.dom]
Domination_Theory.Argument_weighted_sets.pbF [variable, in DomTheory.dom]
Domination_Theory.Argument_weighted_sets.pF [variable, in DomTheory.dom]
Domination_Theory.Argument_weighted_sets.F [variable, in DomTheory.dom]
Domination_Theory.Argument_weighted_sets.pP [variable, in DomTheory.dom]
Domination_Theory.Argument_weighted_sets.pb [variable, in DomTheory.dom]
Domination_Theory.Argument_weighted_sets.p [variable, in DomTheory.dom]
Domination_Theory.Argument_weighted_sets.weight [variable, in DomTheory.dom]
Domination_Theory.Argument_weighted_sets [section, in DomTheory.dom]
Domination_Theory.Weighted_Sets.D [variable, in DomTheory.dom]
Domination_Theory.Weighted_Sets.p [variable, in DomTheory.dom]
Domination_Theory.Weighted_Sets.positive_weights [variable, in DomTheory.dom]
Domination_Theory.Weighted_Sets.weight [variable, in DomTheory.dom]
Domination_Theory.Weighted_Sets [section, in DomTheory.dom]
Domination_Theory.Existence_of_stable_dominating_irredundant_sets [section, in DomTheory.dom]
Domination_Theory.Relations_between_stable_dominating_irredundant_sets.D [variable, in DomTheory.dom]
Domination_Theory.Relations_between_stable_dominating_irredundant_sets [section, in DomTheory.dom]
Domination_Theory.Independence_system_properties.D [variable, in DomTheory.dom]
Domination_Theory.Independence_system_properties.p [variable, in DomTheory.dom]
Domination_Theory.Independence_system_properties [section, in DomTheory.dom]
Domination_Theory.Independence_system_definitions.p [variable, in DomTheory.dom]
Domination_Theory.Independence_system_definitions [section, in DomTheory.dom]
Domination_Theory.MaxMin_sets_existence.pbF [variable, in DomTheory.dom]
Domination_Theory.MaxMin_sets_existence.pF [variable, in DomTheory.dom]
Domination_Theory.MaxMin_sets_existence.F [variable, in DomTheory.dom]
Domination_Theory.MaxMin_sets_existence.pP [variable, in DomTheory.dom]
Domination_Theory.MaxMin_sets_existence.pb [variable, in DomTheory.dom]
Domination_Theory.MaxMin_sets_existence.D [variable, in DomTheory.dom]
Domination_Theory.MaxMin_sets_existence.p [variable, in DomTheory.dom]
Domination_Theory.MaxMin_sets_existence [section, in DomTheory.dom]
Domination_Theory.MaxMin_sets.pP [variable, in DomTheory.dom]
Domination_Theory.MaxMin_sets.pb [variable, in DomTheory.dom]
Domination_Theory.MaxMin_sets.D [variable, in DomTheory.dom]
Domination_Theory.MaxMin_sets.p [variable, in DomTheory.dom]
Domination_Theory.MaxMin_sets [section, in DomTheory.dom]
Domination_Theory.Irredundant_Set.D [variable, in DomTheory.dom]
Domination_Theory.Irredundant_Set [section, in DomTheory.dom]
Domination_Theory.Private_vertices.D [variable, in DomTheory.dom]
Domination_Theory.Private_vertices [section, in DomTheory.dom]
Domination_Theory.Dominating_Set.D [variable, in DomTheory.dom]
Domination_Theory.Dominating_Set [section, in DomTheory.dom]
Domination_Theory.Stable_Set.S [variable, in DomTheory.dom]
Domination_Theory.Stable_Set [section, in DomTheory.dom]
Domination_Theory.G [variable, in DomTheory.dom]
Domination_Theory [section, in DomTheory.dom]
dom_superhereditary [lemma, in DomTheory.dom]
dom_VG [lemma, in DomTheory.dom]
doubleton_eq_iff [lemma, in DomTheory.basics]
doubleton_eq_right [lemma, in DomTheory.basics]
doubleton_eq_left [lemma, in DomTheory.basics]
D_in_closed_neight_set [lemma, in DomTheory.basics]
E
edges_size_two [lemma, in DomTheory.basics]edge_set_minus_uv [lemma, in DomTheory.basics]
edge_setP [lemma, in DomTheory.basics]
edge_set [definition, in DomTheory.basics]
edge_set_predb [definition, in DomTheory.basics]
edge_set_pred [definition, in DomTheory.basics]
empty_set_zero_weight [lemma, in DomTheory.dom]
Example [section, in DomTheory.example]
example [library]
Example.complete_graph [variable, in DomTheory.example]
Example.h [variable, in DomTheory.example]
Example.max_weights [variable, in DomTheory.example]
Example.n [variable, in DomTheory.example]
Example.ngt0 [variable, in DomTheory.example]
Example.positive_weights [variable, in DomTheory.example]
Example.weight [variable, in DomTheory.example]
ex_minimal [definition, in DomTheory.dom]
ex_maximal [definition, in DomTheory.dom]
G
Gamma [definition, in DomTheory.dom]gamma [definition, in DomTheory.dom]
Gamma_Kn_eq_1 [definition, in DomTheory.example]
Gamma_w_Kn_eq_n [definition, in DomTheory.example]
Gamma_eq_1 [lemma, in DomTheory.example]
gamma_eq_1 [lemma, in DomTheory.example]
Gamma_w_eq_wh [lemma, in DomTheory.example]
Gamma_leq_IR [lemma, in DomTheory.dom]
gamma_leq_ii [lemma, in DomTheory.dom]
Gamma_is_Gamma1 [lemma, in DomTheory.dom]
gamma_is_gamma1 [lemma, in DomTheory.dom]
Gamma_w_leq_IR_w [lemma, in DomTheory.dom]
gamma_w_leq_ii_w [lemma, in DomTheory.dom]
Gamma_w [definition, in DomTheory.dom]
gamma_w [definition, in DomTheory.dom]
give_adj_uv_v [lemma, in DomTheory.basics]
give_adj_uv_u [lemma, in DomTheory.basics]
give_adj_uv [definition, in DomTheory.basics]
G_minus_uv [definition, in DomTheory.basics]
H
hereditary [definition, in DomTheory.dom]I
ii [definition, in DomTheory.dom]ii_eq_1 [lemma, in DomTheory.example]
ii_leq_alpha [lemma, in DomTheory.dom]
ii_is_ii1 [lemma, in DomTheory.dom]
ii_w_leq_alpha_w [lemma, in DomTheory.dom]
ii_w [definition, in DomTheory.dom]
inhb_max_irr [definition, in DomTheory.dom]
inhb_min_dom [definition, in DomTheory.dom]
inhb_st_dom [definition, in DomTheory.dom]
IR [definition, in DomTheory.dom]
ir [definition, in DomTheory.dom]
irredundant [definition, in DomTheory.dom]
irredundantP [lemma, in DomTheory.dom]
irr_size_1 [lemma, in DomTheory.example]
irr_hereditary [lemma, in DomTheory.dom]
irr_empty [lemma, in DomTheory.dom]
IR_eq_1 [lemma, in DomTheory.example]
ir_eq_1 [lemma, in DomTheory.example]
IR_leq_1 [lemma, in DomTheory.example]
ir_geq_1 [lemma, in DomTheory.example]
IR_w_eq_wh [lemma, in DomTheory.example]
IR_w_leq_wh [lemma, in DomTheory.example]
ir_leq_gamma [lemma, in DomTheory.dom]
IR_is_IR1 [lemma, in DomTheory.dom]
ir_is_ir1 [lemma, in DomTheory.dom]
ir_w_leq_gamma_w [lemma, in DomTheory.dom]
IR_w [definition, in DomTheory.dom]
ir_w [definition, in DomTheory.dom]
isolate_graph [definition, in DomTheory.basics]
K
Kn [definition, in DomTheory.example]M
maximal [definition, in DomTheory.dom]maximalb [definition, in DomTheory.dom]
maximalP [lemma, in DomTheory.dom]
maximal_st_is_minimal_dom [lemma, in DomTheory.dom]
maximal_st_iff_st_dom [lemma, in DomTheory.dom]
maximal_altdef [lemma, in DomTheory.dom]
maximal_exists [lemma, in DomTheory.dom]
maximum [definition, in DomTheory.dom]
maximum_set_card [definition, in DomTheory.dom]
maximum_card_is_maximal [lemma, in DomTheory.dom]
maximum_card [definition, in DomTheory.dom]
maximum_set_welldefined [lemma, in DomTheory.dom]
maximum_set_p [lemma, in DomTheory.dom]
maximum_set [definition, in DomTheory.dom]
maximum_is_maximal [lemma, in DomTheory.dom]
maximum1 [lemma, in DomTheory.dom]
max_card_weight_1 [lemma, in DomTheory.dom]
max_irr [definition, in DomTheory.dom]
max_irrP [lemma, in DomTheory.dom]
minimal [definition, in DomTheory.dom]
minimalb [definition, in DomTheory.dom]
minimalP [lemma, in DomTheory.dom]
minimal_dom_is_maximal_irr [lemma, in DomTheory.dom]
minimal_dom_iff_dom_irr [lemma, in DomTheory.dom]
minimal_altdef [lemma, in DomTheory.dom]
minimal_exists [lemma, in DomTheory.dom]
minimum [definition, in DomTheory.dom]
minimum_set_card [definition, in DomTheory.dom]
minimum_card_is_minimal [lemma, in DomTheory.dom]
minimum_card [definition, in DomTheory.dom]
minimum_set_welldefined [lemma, in DomTheory.dom]
minimum_set_p [lemma, in DomTheory.dom]
minimum_set [definition, in DomTheory.dom]
minimum_is_minimal [lemma, in DomTheory.dom]
minimum1 [lemma, in DomTheory.dom]
min_card_weight_1 [lemma, in DomTheory.dom]
min_dom [definition, in DomTheory.dom]
min_domP [lemma, in DomTheory.dom]
N
Neighborhoods_definitions.D [variable, in DomTheory.basics]N[ _ ] [notation, in DomTheory.basics]
N( _ ) [notation, in DomTheory.basics]
Neighborhoods_definitions.G [variable, in DomTheory.basics]
Neighborhoods_definitions [section, in DomTheory.basics]
O
ones [definition, in DomTheory.dom]open_neigh_set_subset_closed_neigh_set [lemma, in DomTheory.basics]
open_neigh_set [definition, in DomTheory.basics]
open_neigh [definition, in DomTheory.basics]
op_neigh_minus_uv1 [lemma, in DomTheory.basics]
op_neigh_minus_uv0 [lemma, in DomTheory.basics]
op_neigh_minus_uv_empty [lemma, in DomTheory.basics]
P
pair_card2_exists [lemma, in DomTheory.basics]pair_neq_card2 [lemma, in DomTheory.basics]
pair_commute [lemma, in DomTheory.basics]
pair_absorb [lemma, in DomTheory.basics]
pb_max_irr [definition, in DomTheory.dom]
pb_min_dom [definition, in DomTheory.dom]
pb_st_dom [definition, in DomTheory.dom]
pb_irredundant [definition, in DomTheory.dom]
pb_dominating [definition, in DomTheory.dom]
pb_stable [definition, in DomTheory.dom]
pinh_max_irr [lemma, in DomTheory.dom]
pinh_min_dom [lemma, in DomTheory.dom]
pinh_st_dom [lemma, in DomTheory.dom]
Preliminaries1 [section, in DomTheory.basics]
Preliminaries1.A [variable, in DomTheory.basics]
Preliminaries1.B [variable, in DomTheory.basics]
Preliminaries1.T [variable, in DomTheory.basics]
Preliminaries1.u [variable, in DomTheory.basics]
Preliminaries1.v [variable, in DomTheory.basics]
Preliminaries2 [section, in DomTheory.basics]
Preliminaries2.T [variable, in DomTheory.basics]
private [definition, in DomTheory.dom]
privateb [definition, in DomTheory.dom]
privateP [lemma, in DomTheory.dom]
private_set [definition, in DomTheory.dom]
proper_sets_weight [lemma, in DomTheory.dom]
p_max_irr [definition, in DomTheory.dom]
p_min_dom [definition, in DomTheory.dom]
p_st_dom [definition, in DomTheory.dom]
p_irredundant [definition, in DomTheory.dom]
p_dominating [definition, in DomTheory.dom]
p_stable [definition, in DomTheory.dom]
R
Remove_edge.sg_irrefl' [variable, in DomTheory.basics]Remove_edge.sg_sym' [variable, in DomTheory.basics]
Remove_edge.sedge' [variable, in DomTheory.basics]
Remove_edge.adjuv [variable, in DomTheory.basics]
Remove_edge.v [variable, in DomTheory.basics]
Remove_edge.u [variable, in DomTheory.basics]
Remove_edge.G [variable, in DomTheory.basics]
Remove_edge [section, in DomTheory.basics]
S
sedge [projection, in DomTheory.sgraph]set_minus_union1 [lemma, in DomTheory.basics]
set_pair_disjoint [lemma, in DomTheory.basics]
set_minus_disjoint [lemma, in DomTheory.basics]
set_minus_union [lemma, in DomTheory.basics]
set21_subset [lemma, in DomTheory.basics]
set22_subset [lemma, in DomTheory.basics]
sgP [definition, in DomTheory.sgraph]
sgraph [record, in DomTheory.sgraph]
SGraph [constructor, in DomTheory.sgraph]
sgraph [library]
sg_edgeNeq [lemma, in DomTheory.sgraph]
sg_irrefl [projection, in DomTheory.sgraph]
sg_sym [projection, in DomTheory.sgraph]
sg_implies_sg [lemma, in DomTheory.basics]
sg_xy_sg [lemma, in DomTheory.basics]
sg_uv_false [lemma, in DomTheory.basics]
sg_isolate_graph [lemma, in DomTheory.basics]
sg_in_edge_set [lemma, in DomTheory.basics]
sg_opneigh [lemma, in DomTheory.basics]
stable [definition, in DomTheory.dom]
stableP [lemma, in DomTheory.dom]
stable_refl [lemma, in DomTheory.dom]
st_dom [definition, in DomTheory.dom]
st_domP [lemma, in DomTheory.dom]
st_hereditary [lemma, in DomTheory.dom]
st_empty [lemma, in DomTheory.dom]
subsets_weight [lemma, in DomTheory.dom]
subset_opneigh_minus_uv [lemma, in DomTheory.basics]
subset_inter [lemma, in DomTheory.basics]
sumdeg_2E [lemma, in DomTheory.basics]
Sum_degrees_eq_twice_edges [section, in DomTheory.basics]
sum_singleton [lemma, in DomTheory.basics]
sum_empty [lemma, in DomTheory.basics]
sum_disjoint_union [lemma, in DomTheory.basics]
superhereditary [definition, in DomTheory.dom]
svertex [projection, in DomTheory.sgraph]
S_is_maximal_irredundant [lemma, in DomTheory.example]
S_weights_wh [lemma, in DomTheory.example]
S_is_stable [lemma, in DomTheory.example]
U
Unweighted_complete.S [variable, in DomTheory.example]Unweighted_complete.h_heaviest [variable, in DomTheory.example]
Unweighted_complete.positive_weights [variable, in DomTheory.example]
Unweighted_complete.weight [variable, in DomTheory.example]
Unweighted_complete.complete_graph [variable, in DomTheory.example]
Unweighted_complete.h [variable, in DomTheory.example]
Unweighted_complete.G [variable, in DomTheory.example]
Unweighted_complete [section, in DomTheory.example]
V
VeqVminusepluse [lemma, in DomTheory.basics]VertexSetProperty [constructor, in DomTheory.dom]
vsbool [projection, in DomTheory.dom]
vsinhb [projection, in DomTheory.dom]
vspinh [projection, in DomTheory.dom]
vsprop [projection, in DomTheory.dom]
vsproperty [record, in DomTheory.dom]
vsrefl [projection, in DomTheory.dom]
W
Weighted_complete.S [variable, in DomTheory.example]Weighted_complete.complete_graph [variable, in DomTheory.example]
Weighted_complete.h_heaviest [variable, in DomTheory.example]
Weighted_complete.wh [variable, in DomTheory.example]
Weighted_complete.h [variable, in DomTheory.example]
Weighted_complete.positive_weights [variable, in DomTheory.example]
Weighted_complete.weight [variable, in DomTheory.example]
Weighted_complete.G [variable, in DomTheory.example]
Weighted_complete [section, in DomTheory.example]
weight_set_natural [lemma, in DomTheory.dom]
weight_set [definition, in DomTheory.dom]
wh_leq_alpha_w [lemma, in DomTheory.example]
other
_ ⊂ _ [notation, in DomTheory.sgraph]_ ⊆ _ [notation, in DomTheory.sgraph]
_ ∉ _ [notation, in DomTheory.sgraph]
_ ∈ _ [notation, in DomTheory.sgraph]
_ -- _ [notation, in DomTheory.sgraph]
_ -*- _ [notation, in DomTheory.basics]
E( _ ) [notation, in DomTheory.basics]
NS( _ ) [notation, in DomTheory.basics]
NS( _ ; _ ) [notation, in DomTheory.basics]
NS[ _ ] [notation, in DomTheory.basics]
NS[ _ ; _ ] [notation, in DomTheory.basics]
N( _ ) [notation, in DomTheory.basics]
N( _ ; _ ) [notation, in DomTheory.basics]
N[ _ ] [notation, in DomTheory.basics]
N[ _ ; _ ] [notation, in DomTheory.basics]
V( _ ) [notation, in DomTheory.basics]
∅ [notation, in DomTheory.sgraph]
⋃ ( _ in _ | _ ) _ [notation, in DomTheory.sgraph]
❴ _ ; _ ; .. ; _ ❵ [notation, in DomTheory.sgraph]
❴ _ | _ ❵ [notation, in DomTheory.sgraph]
❴ _ ❵ [notation, in DomTheory.sgraph]
Σ ( _ in _ | _ ) _ [notation, in DomTheory.sgraph]
Σ ( _ in _ ) _ [notation, in DomTheory.sgraph]
Notation Index
N
N[ _ ] [in DomTheory.basics]N( _ ) [in DomTheory.basics]
other
_ ⊂ _ [in DomTheory.sgraph]_ ⊆ _ [in DomTheory.sgraph]
_ ∉ _ [in DomTheory.sgraph]
_ ∈ _ [in DomTheory.sgraph]
_ -- _ [in DomTheory.sgraph]
_ -*- _ [in DomTheory.basics]
E( _ ) [in DomTheory.basics]
NS( _ ) [in DomTheory.basics]
NS( _ ; _ ) [in DomTheory.basics]
NS[ _ ] [in DomTheory.basics]
NS[ _ ; _ ] [in DomTheory.basics]
N( _ ) [in DomTheory.basics]
N( _ ; _ ) [in DomTheory.basics]
N[ _ ] [in DomTheory.basics]
N[ _ ; _ ] [in DomTheory.basics]
V( _ ) [in DomTheory.basics]
∅ [in DomTheory.sgraph]
⋃ ( _ in _ | _ ) _ [in DomTheory.sgraph]
❴ _ ; _ ; .. ; _ ❵ [in DomTheory.sgraph]
❴ _ | _ ❵ [in DomTheory.sgraph]
❴ _ ❵ [in DomTheory.sgraph]
Σ ( _ in _ | _ ) _ [in DomTheory.sgraph]
Σ ( _ in _ ) _ [in DomTheory.sgraph]
Variable Index
B
Basic_Facts_Neighborhoods.D2 [in DomTheory.basics]Basic_Facts_Neighborhoods.D1 [in DomTheory.basics]
Basic_Facts_Neighborhoods.G [in DomTheory.basics]
D
Domination_Theory.Classic_domination_parameters.maximum_irr [in DomTheory.dom]Domination_Theory.Classic_domination_parameters.maximum_minimal_dom [in DomTheory.dom]
Domination_Theory.Classic_domination_parameters.maximum_st [in DomTheory.dom]
Domination_Theory.Classic_domination_parameters.minimum_st_dom [in DomTheory.dom]
Domination_Theory.Classic_domination_parameters.minimum_dom [in DomTheory.dom]
Domination_Theory.Classic_domination_parameters.minimum_maximal_irr [in DomTheory.dom]
Domination_Theory.Argument_unweighted_sets.pbF [in DomTheory.dom]
Domination_Theory.Argument_unweighted_sets.pF [in DomTheory.dom]
Domination_Theory.Argument_unweighted_sets.F [in DomTheory.dom]
Domination_Theory.Argument_unweighted_sets.pP [in DomTheory.dom]
Domination_Theory.Argument_unweighted_sets.pb [in DomTheory.dom]
Domination_Theory.Argument_unweighted_sets.p [in DomTheory.dom]
Domination_Theory.Unweighted_Sets.D [in DomTheory.dom]
Domination_Theory.Unweighted_Sets.p [in DomTheory.dom]
Domination_Theory.Weighted_domination_parameters.maximum_irr [in DomTheory.dom]
Domination_Theory.Weighted_domination_parameters.maximum_minimal_dom [in DomTheory.dom]
Domination_Theory.Weighted_domination_parameters.maximum_st [in DomTheory.dom]
Domination_Theory.Weighted_domination_parameters.minimum_st_dom [in DomTheory.dom]
Domination_Theory.Weighted_domination_parameters.minimum_dom [in DomTheory.dom]
Domination_Theory.Weighted_domination_parameters.minimum_maximal_irr [in DomTheory.dom]
Domination_Theory.Weighted_domination_parameters.positive_weights [in DomTheory.dom]
Domination_Theory.Weighted_domination_parameters.weight [in DomTheory.dom]
Domination_Theory.Argument_weighted_sets.pbF [in DomTheory.dom]
Domination_Theory.Argument_weighted_sets.pF [in DomTheory.dom]
Domination_Theory.Argument_weighted_sets.F [in DomTheory.dom]
Domination_Theory.Argument_weighted_sets.pP [in DomTheory.dom]
Domination_Theory.Argument_weighted_sets.pb [in DomTheory.dom]
Domination_Theory.Argument_weighted_sets.p [in DomTheory.dom]
Domination_Theory.Argument_weighted_sets.weight [in DomTheory.dom]
Domination_Theory.Weighted_Sets.D [in DomTheory.dom]
Domination_Theory.Weighted_Sets.p [in DomTheory.dom]
Domination_Theory.Weighted_Sets.positive_weights [in DomTheory.dom]
Domination_Theory.Weighted_Sets.weight [in DomTheory.dom]
Domination_Theory.Relations_between_stable_dominating_irredundant_sets.D [in DomTheory.dom]
Domination_Theory.Independence_system_properties.D [in DomTheory.dom]
Domination_Theory.Independence_system_properties.p [in DomTheory.dom]
Domination_Theory.Independence_system_definitions.p [in DomTheory.dom]
Domination_Theory.MaxMin_sets_existence.pbF [in DomTheory.dom]
Domination_Theory.MaxMin_sets_existence.pF [in DomTheory.dom]
Domination_Theory.MaxMin_sets_existence.F [in DomTheory.dom]
Domination_Theory.MaxMin_sets_existence.pP [in DomTheory.dom]
Domination_Theory.MaxMin_sets_existence.pb [in DomTheory.dom]
Domination_Theory.MaxMin_sets_existence.D [in DomTheory.dom]
Domination_Theory.MaxMin_sets_existence.p [in DomTheory.dom]
Domination_Theory.MaxMin_sets.pP [in DomTheory.dom]
Domination_Theory.MaxMin_sets.pb [in DomTheory.dom]
Domination_Theory.MaxMin_sets.D [in DomTheory.dom]
Domination_Theory.MaxMin_sets.p [in DomTheory.dom]
Domination_Theory.Irredundant_Set.D [in DomTheory.dom]
Domination_Theory.Private_vertices.D [in DomTheory.dom]
Domination_Theory.Dominating_Set.D [in DomTheory.dom]
Domination_Theory.Stable_Set.S [in DomTheory.dom]
Domination_Theory.G [in DomTheory.dom]
E
Example.complete_graph [in DomTheory.example]Example.h [in DomTheory.example]
Example.max_weights [in DomTheory.example]
Example.n [in DomTheory.example]
Example.ngt0 [in DomTheory.example]
Example.positive_weights [in DomTheory.example]
Example.weight [in DomTheory.example]
N
Neighborhoods_definitions.D [in DomTheory.basics]Neighborhoods_definitions.G [in DomTheory.basics]
P
Preliminaries1.A [in DomTheory.basics]Preliminaries1.B [in DomTheory.basics]
Preliminaries1.T [in DomTheory.basics]
Preliminaries1.u [in DomTheory.basics]
Preliminaries1.v [in DomTheory.basics]
Preliminaries2.T [in DomTheory.basics]
R
Remove_edge.sg_irrefl' [in DomTheory.basics]Remove_edge.sg_sym' [in DomTheory.basics]
Remove_edge.sedge' [in DomTheory.basics]
Remove_edge.adjuv [in DomTheory.basics]
Remove_edge.v [in DomTheory.basics]
Remove_edge.u [in DomTheory.basics]
Remove_edge.G [in DomTheory.basics]
U
Unweighted_complete.S [in DomTheory.example]Unweighted_complete.h_heaviest [in DomTheory.example]
Unweighted_complete.positive_weights [in DomTheory.example]
Unweighted_complete.weight [in DomTheory.example]
Unweighted_complete.complete_graph [in DomTheory.example]
Unweighted_complete.h [in DomTheory.example]
Unweighted_complete.G [in DomTheory.example]
W
Weighted_complete.S [in DomTheory.example]Weighted_complete.complete_graph [in DomTheory.example]
Weighted_complete.h_heaviest [in DomTheory.example]
Weighted_complete.wh [in DomTheory.example]
Weighted_complete.h [in DomTheory.example]
Weighted_complete.positive_weights [in DomTheory.example]
Weighted_complete.weight [in DomTheory.example]
Weighted_complete.G [in DomTheory.example]
Library Index
B
basicsD
domE
exampleS
sgraphLemma Index
A
alpha_eq_1 [in DomTheory.example]alpha_w_eq_wh [in DomTheory.example]
alpha_leq_Gamma [in DomTheory.dom]
alpha_is_alpha1 [in DomTheory.dom]
alpha_w_leq_Gamma_w [in DomTheory.dom]
C
card_weight_1 [in DomTheory.dom]closed_neigh_set_subset [in DomTheory.basics]
clsg_clneigh [in DomTheory.basics]
cl_sg_refl [in DomTheory.basics]
cl_sg_sym [in DomTheory.basics]
D
deg_minus_uv2 [in DomTheory.basics]deg_minus_uv1 [in DomTheory.basics]
deg_minus_uv0 [in DomTheory.basics]
deg_isolate_graph [in DomTheory.basics]
dominated_belongs_to_closed_neigh_set [in DomTheory.basics]
dominated_belongs_to_open_neigh_set [in DomTheory.basics]
dominatingP [in DomTheory.dom]
dom_superhereditary [in DomTheory.dom]
dom_VG [in DomTheory.dom]
doubleton_eq_iff [in DomTheory.basics]
doubleton_eq_right [in DomTheory.basics]
doubleton_eq_left [in DomTheory.basics]
D_in_closed_neight_set [in DomTheory.basics]
E
edges_size_two [in DomTheory.basics]edge_set_minus_uv [in DomTheory.basics]
edge_setP [in DomTheory.basics]
empty_set_zero_weight [in DomTheory.dom]
G
Gamma_eq_1 [in DomTheory.example]gamma_eq_1 [in DomTheory.example]
Gamma_w_eq_wh [in DomTheory.example]
Gamma_leq_IR [in DomTheory.dom]
gamma_leq_ii [in DomTheory.dom]
Gamma_is_Gamma1 [in DomTheory.dom]
gamma_is_gamma1 [in DomTheory.dom]
Gamma_w_leq_IR_w [in DomTheory.dom]
gamma_w_leq_ii_w [in DomTheory.dom]
give_adj_uv_v [in DomTheory.basics]
give_adj_uv_u [in DomTheory.basics]
I
ii_eq_1 [in DomTheory.example]ii_leq_alpha [in DomTheory.dom]
ii_is_ii1 [in DomTheory.dom]
ii_w_leq_alpha_w [in DomTheory.dom]
irredundantP [in DomTheory.dom]
irr_size_1 [in DomTheory.example]
irr_hereditary [in DomTheory.dom]
irr_empty [in DomTheory.dom]
IR_eq_1 [in DomTheory.example]
ir_eq_1 [in DomTheory.example]
IR_leq_1 [in DomTheory.example]
ir_geq_1 [in DomTheory.example]
IR_w_eq_wh [in DomTheory.example]
IR_w_leq_wh [in DomTheory.example]
ir_leq_gamma [in DomTheory.dom]
IR_is_IR1 [in DomTheory.dom]
ir_is_ir1 [in DomTheory.dom]
ir_w_leq_gamma_w [in DomTheory.dom]
M
maximalP [in DomTheory.dom]maximal_st_is_minimal_dom [in DomTheory.dom]
maximal_st_iff_st_dom [in DomTheory.dom]
maximal_altdef [in DomTheory.dom]
maximal_exists [in DomTheory.dom]
maximum_card_is_maximal [in DomTheory.dom]
maximum_set_welldefined [in DomTheory.dom]
maximum_set_p [in DomTheory.dom]
maximum_is_maximal [in DomTheory.dom]
maximum1 [in DomTheory.dom]
max_card_weight_1 [in DomTheory.dom]
max_irrP [in DomTheory.dom]
minimalP [in DomTheory.dom]
minimal_dom_is_maximal_irr [in DomTheory.dom]
minimal_dom_iff_dom_irr [in DomTheory.dom]
minimal_altdef [in DomTheory.dom]
minimal_exists [in DomTheory.dom]
minimum_card_is_minimal [in DomTheory.dom]
minimum_set_welldefined [in DomTheory.dom]
minimum_set_p [in DomTheory.dom]
minimum_is_minimal [in DomTheory.dom]
minimum1 [in DomTheory.dom]
min_card_weight_1 [in DomTheory.dom]
min_domP [in DomTheory.dom]
O
open_neigh_set_subset_closed_neigh_set [in DomTheory.basics]op_neigh_minus_uv1 [in DomTheory.basics]
op_neigh_minus_uv0 [in DomTheory.basics]
op_neigh_minus_uv_empty [in DomTheory.basics]
P
pair_card2_exists [in DomTheory.basics]pair_neq_card2 [in DomTheory.basics]
pair_commute [in DomTheory.basics]
pair_absorb [in DomTheory.basics]
pinh_max_irr [in DomTheory.dom]
pinh_min_dom [in DomTheory.dom]
pinh_st_dom [in DomTheory.dom]
privateP [in DomTheory.dom]
proper_sets_weight [in DomTheory.dom]
S
set_minus_union1 [in DomTheory.basics]set_pair_disjoint [in DomTheory.basics]
set_minus_disjoint [in DomTheory.basics]
set_minus_union [in DomTheory.basics]
set21_subset [in DomTheory.basics]
set22_subset [in DomTheory.basics]
sg_edgeNeq [in DomTheory.sgraph]
sg_implies_sg [in DomTheory.basics]
sg_xy_sg [in DomTheory.basics]
sg_uv_false [in DomTheory.basics]
sg_isolate_graph [in DomTheory.basics]
sg_in_edge_set [in DomTheory.basics]
sg_opneigh [in DomTheory.basics]
stableP [in DomTheory.dom]
stable_refl [in DomTheory.dom]
st_domP [in DomTheory.dom]
st_hereditary [in DomTheory.dom]
st_empty [in DomTheory.dom]
subsets_weight [in DomTheory.dom]
subset_opneigh_minus_uv [in DomTheory.basics]
subset_inter [in DomTheory.basics]
sumdeg_2E [in DomTheory.basics]
sum_singleton [in DomTheory.basics]
sum_empty [in DomTheory.basics]
sum_disjoint_union [in DomTheory.basics]
S_is_maximal_irredundant [in DomTheory.example]
S_weights_wh [in DomTheory.example]
S_is_stable [in DomTheory.example]
V
VeqVminusepluse [in DomTheory.basics]W
weight_set_natural [in DomTheory.dom]wh_leq_alpha_w [in DomTheory.example]
Constructor Index
S
SGraph [in DomTheory.sgraph]V
VertexSetProperty [in DomTheory.dom]Projection Index
S
sedge [in DomTheory.sgraph]sg_irrefl [in DomTheory.sgraph]
sg_sym [in DomTheory.sgraph]
svertex [in DomTheory.sgraph]
V
vsbool [in DomTheory.dom]vsinhb [in DomTheory.dom]
vspinh [in DomTheory.dom]
vsprop [in DomTheory.dom]
vsrefl [in DomTheory.dom]
Section Index
B
Basic_Facts_Neighborhoods [in DomTheory.basics]D
Domination_Theory.Classic_domination_parameters [in DomTheory.dom]Domination_Theory.Argument_unweighted_sets [in DomTheory.dom]
Domination_Theory.Unweighted_Sets [in DomTheory.dom]
Domination_Theory.Weighted_domination_parameters [in DomTheory.dom]
Domination_Theory.Argument_weighted_sets [in DomTheory.dom]
Domination_Theory.Weighted_Sets [in DomTheory.dom]
Domination_Theory.Existence_of_stable_dominating_irredundant_sets [in DomTheory.dom]
Domination_Theory.Relations_between_stable_dominating_irredundant_sets [in DomTheory.dom]
Domination_Theory.Independence_system_properties [in DomTheory.dom]
Domination_Theory.Independence_system_definitions [in DomTheory.dom]
Domination_Theory.MaxMin_sets_existence [in DomTheory.dom]
Domination_Theory.MaxMin_sets [in DomTheory.dom]
Domination_Theory.Irredundant_Set [in DomTheory.dom]
Domination_Theory.Private_vertices [in DomTheory.dom]
Domination_Theory.Dominating_Set [in DomTheory.dom]
Domination_Theory.Stable_Set [in DomTheory.dom]
Domination_Theory [in DomTheory.dom]
E
Example [in DomTheory.example]N
Neighborhoods_definitions [in DomTheory.basics]P
Preliminaries1 [in DomTheory.basics]Preliminaries2 [in DomTheory.basics]
R
Remove_edge [in DomTheory.basics]S
Sum_degrees_eq_twice_edges [in DomTheory.basics]U
Unweighted_complete [in DomTheory.example]W
Weighted_complete [in DomTheory.example]Definition Index
A
alpha [in DomTheory.dom]alpha_w [in DomTheory.dom]
C
closed_neigh_set [in DomTheory.basics]closed_neigh [in DomTheory.basics]
cl_sedge [in DomTheory.basics]
D
deg [in DomTheory.basics]dominating [in DomTheory.dom]
E
edge_set [in DomTheory.basics]edge_set_predb [in DomTheory.basics]
edge_set_pred [in DomTheory.basics]
ex_minimal [in DomTheory.dom]
ex_maximal [in DomTheory.dom]
G
Gamma [in DomTheory.dom]gamma [in DomTheory.dom]
Gamma_Kn_eq_1 [in DomTheory.example]
Gamma_w_Kn_eq_n [in DomTheory.example]
Gamma_w [in DomTheory.dom]
gamma_w [in DomTheory.dom]
give_adj_uv [in DomTheory.basics]
G_minus_uv [in DomTheory.basics]
H
hereditary [in DomTheory.dom]I
ii [in DomTheory.dom]ii_w [in DomTheory.dom]
inhb_max_irr [in DomTheory.dom]
inhb_min_dom [in DomTheory.dom]
inhb_st_dom [in DomTheory.dom]
IR [in DomTheory.dom]
ir [in DomTheory.dom]
irredundant [in DomTheory.dom]
IR_w [in DomTheory.dom]
ir_w [in DomTheory.dom]
isolate_graph [in DomTheory.basics]
K
Kn [in DomTheory.example]M
maximal [in DomTheory.dom]maximalb [in DomTheory.dom]
maximum [in DomTheory.dom]
maximum_set_card [in DomTheory.dom]
maximum_card [in DomTheory.dom]
maximum_set [in DomTheory.dom]
max_irr [in DomTheory.dom]
minimal [in DomTheory.dom]
minimalb [in DomTheory.dom]
minimum [in DomTheory.dom]
minimum_set_card [in DomTheory.dom]
minimum_card [in DomTheory.dom]
minimum_set [in DomTheory.dom]
min_dom [in DomTheory.dom]
O
ones [in DomTheory.dom]open_neigh_set [in DomTheory.basics]
open_neigh [in DomTheory.basics]
P
pb_max_irr [in DomTheory.dom]pb_min_dom [in DomTheory.dom]
pb_st_dom [in DomTheory.dom]
pb_irredundant [in DomTheory.dom]
pb_dominating [in DomTheory.dom]
pb_stable [in DomTheory.dom]
private [in DomTheory.dom]
privateb [in DomTheory.dom]
private_set [in DomTheory.dom]
p_max_irr [in DomTheory.dom]
p_min_dom [in DomTheory.dom]
p_st_dom [in DomTheory.dom]
p_irredundant [in DomTheory.dom]
p_dominating [in DomTheory.dom]
p_stable [in DomTheory.dom]
S
sgP [in DomTheory.sgraph]stable [in DomTheory.dom]
st_dom [in DomTheory.dom]
superhereditary [in DomTheory.dom]
W
weight_set [in DomTheory.dom]Record Index
S
sgraph [in DomTheory.sgraph]V
vsproperty [in DomTheory.dom]| 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 | (355 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 | (25 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 | (93 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 | (4 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 | (124 entries) |
| Constructor 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) |
| 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 | (9 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 | (26 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 | (70 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 | (2 entries) |