| 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 | (1091 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 | (3 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 | (1 entry) |
| 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 | (713 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 | (23 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 | (18 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 | (22 entries) |
| Inductive 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 | (15 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 | (141 entries) |
| Axiom 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) |
| 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 | (105 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 | (38 entries) |
Global Index
A
a [projection, in Chaos]AbelianGroup [definition, in Groups]
AlistIndec [lemma, in ListFacts]
anomalybug [library]
app [definition, in Array]
appaux [definition, in Array]
AppendCommuteDimensions [lemma, in Matrix_base]
AppendCommuteDimensions_RC [lemma, in Matrix_base]
AppendCommuteDimensions_R [lemma, in Matrix_base]
appending [inductive, in Array]
appending_intro [constructor, in Array]
appending_nil [constructor, in Array]
apply_func_intersection [lemma, in EnsembleFacts]
apply_func_singleton [lemma, in EnsembleFacts]
apply_func_add [lemma, in EnsembleFacts]
apply_func_finite [lemma, in EnsembleFacts]
apply_func_rec [lemma, in EnsembleFacts]
apply_func [inductive, in EnsembleFacts]
apply_func_empty [lemma, in EnsembleFacts]
apply_func_equation [lemma, in EnsembleFacts]
apply_func_couple [lemma, in EnsembleFacts]
app_headS [lemma, in Array]
app_from_appending [lemma, in Array]
app_ass [lemma, in Array]
app_nil_r [lemma, in Array]
app_single_l [lemma, in Array]
app_is_appending [lemma, in Array]
app_S [lemma, in Array]
app_tailS [lemma, in Array]
app_headS_tailS [lemma, in Array]
app_equality [lemma, in Array]
app_nil_l [lemma, in Array]
app_nth_right [lemma, in Array]
app_nth_left [lemma, in Array]
Arith [section, in Matrix_arith]
Arith [section, in Vector]
Arith.add [variable, in Vector]
Arith.add [variable, in Matrix_arith]
Arith.add_ass [variable, in Vector]
Arith.add_comm [variable, in Matrix_arith]
Arith.add_ass [variable, in Matrix_arith]
Arith.add_comm [variable, in Vector]
Arith.distributive_left [variable, in Vector]
Arith.distributive_left [variable, in Matrix_arith]
Arith.distributive_right [variable, in Matrix_arith]
Arith.distributive_right [variable, in Vector]
Arith.dotproduct [variable, in Vector]
Arith.one [variable, in Vector]
Arith.one [variable, in Matrix_arith]
Arith.oneL [variable, in Vector]
Arith.oneL [variable, in Matrix_arith]
Arith.oneR [variable, in Matrix_arith]
Arith.oneR [variable, in Vector]
Arith.prod [variable, in Vector]
Arith.prod [variable, in Matrix_arith]
Arith.prod_ass [variable, in Matrix_arith]
Arith.prod_comm [variable, in Matrix_arith]
Arith.prod_zero_r [variable, in Vector]
Arith.prod_zero_l [variable, in Matrix_arith]
Arith.prod_zero_r [variable, in Matrix_arith]
Arith.prod_comm [variable, in Vector]
Arith.prod_ass [variable, in Vector]
Arith.prod_zero_l [variable, in Vector]
Arith.summatory [variable, in Matrix_arith]
Arith.summatory [variable, in Vector]
Arith.summatoryv [variable, in Matrix_arith]
Arith.U [variable, in Matrix_arith]
Arith.U [variable, in Vector]
Arith.unitcol [variable, in Matrix_arith]
Arith.unitrow [variable, in Matrix_arith]
Arith.unitvector [variable, in Vector]
Arith.unitvector [variable, in Matrix_arith]
Arith.zero [variable, in Matrix_arith]
Arith.zero [variable, in Vector]
Arith.zeroL [variable, in Matrix_arith]
Arith.zeroL [variable, in Vector]
Arith.zeroR [variable, in Vector]
Arith.zeroR [variable, in Matrix_arith]
Arith.zerovector [variable, in Matrix_arith]
Arith.zerovector [variable, in Vector]
_ + _ [notation, in Vector]
_ * _ [notation, in Matrix_arith]
_ :* _ [notation, in Matrix_arith]
_ :+ _ [notation, in Matrix_arith]
_ + _ [notation, in Matrix_arith]
_ \u00b7 _ [notation, in Vector]
_ ^T [notation, in Matrix_arith]
_ * _ [notation, in Matrix_arith]
_ * _ [notation, in Vector]
_ + _ [notation, in Matrix_arith]
array [inductive, in Array]
Array [library]
arrayapp [definition, in Array]
arraycons [definition, in Array]
arraynil [definition, in Array]
Arrays [section, in Array]
arrays_lists [section, in Array]
array_from_func_eq [lemma, in Array]
array_from_func_aux [definition, in Array]
array_homogeneous_nth_range [lemma, in Array]
array_typeequality_down [axiom, in Array]
array_homogeneous [definition, in Array]
array_from_func [definition, in Array]
array_from_func_nth_aux [lemma, in Array]
array_from_funcrange_aux_H [lemma, in Array]
array_from_funcrange_nth_range [lemma, in Array]
array_from_funcrange_aux_head_eq [lemma, in Array]
array_from_func_nth_range [lemma, in Array]
array_0_nil [lemma, in Array]
array_from_funcrange_nth_error [lemma, in Array]
array_from_funcrange_nth_range_aux2 [lemma, in Array]
array_from_func_back [lemma, in Array]
array_destruct [lemma, in Array]
array_from_funcrange_nth_error_aux [lemma, in Array]
array_list_app [lemma, in Array]
array_homogeneous_nth_same [lemma, in Array]
array_single [lemma, in Array]
array_from_func_aux_eq [lemma, in Array]
array_from_func_nth_error_aux [lemma, in Array]
array_homogeneous_nth [lemma, in Array]
array_rewrite_dependent_Prop [lemma, in Array]
array_S_ht [lemma, in Array]
array_from_func_nth_error [lemma, in Array]
array_from_funcrange_back [lemma, in Array]
array_to_arrayfromfunc [lemma, in Array]
array_from_funcrange_aux_destructS [lemma, in Array]
array_from_funcrange_nth_range_aux [lemma, in Array]
array_rewrite_dependent [lemma, in Array]
array_single_type [lemma, in Array]
array_as_list [definition, in Array]
array_1_head [lemma, in Array]
array_from_funcrange_aux_head2 [definition, in Array]
array_typeequality_up [lemma, in Array]
array_from_funcrange_extensionality [lemma, in Array]
array_noninhabited [lemma, in Array]
array_from_func_extensionality [lemma, in Array]
array_destructS [lemma, in Array]
array_as_list_cero [lemma, in Array]
array_list_cons [lemma, in Array]
array_from_funcrange_extensionalityR [lemma, in Array]
array_nil_n0 [lemma, in Array]
array_typeequality [lemma, in Array]
array_homogeneous_app [lemma, in Array]
array_from_func_nth [lemma, in Array]
array_Function0 [lemma, in Array]
array_cut [lemma, in Array]
array_n0_nil [lemma, in Array]
array_to_arrayfromfuncrange [lemma, in Array]
array_from_funcrange_aux_destruct0 [lemma, in Array]
array_from_funcrange_aux_head [definition, in Array]
array_from_funcrange [definition, in Array]
array_app_nil_l [definition, in Array]
array_FunctionS [lemma, in Array]
array_assoc [lemma, in Array]
Array_old_eqtype [library]
array2D [definition, in Matrix_base]
array2D_typeequality_down_H [axiom, in Matrix_base]
array2D_rewrite_dependent_H_Prop [lemma, in Matrix_base]
array2D_0_nilC [lemma, in Matrix_base]
array2D_1_Column [lemma, in Matrix_base]
array2D_rewrite_dependent_H [lemma, in Matrix_base]
array2D_typeequality_down_V [lemma, in Matrix_base]
Associativity [definition, in EnsembleFacts]
axiomtypes [library]
B
b [projection, in Chaos]BigIntersection [inductive, in EnsembleAsType]
BigIntersection_intro [constructor, in EnsembleAsType]
BigIntersection_pair [lemma, in EnsembleAsType]
BigUnion [inductive, in EnsembleAsType]
BigUnion_intro [constructor, in EnsembleAsType]
BigUnion_pair [lemma, in EnsembleAsType]
BijectionComposition [lemma, in EnsembleFacts]
BijectionSimplify [lemma, in EnsembleFacts]
Bijective [definition, in EnsembleFacts]
Bijective_rev [lemma, in EnsembleFacts]
bijective_eqcardinal [lemma, in EnsembleFacts]
bool_choice [lemma, in types_base]
C
CayAbel_wont4c_transcomm [lemma, in CayleyGraph]CayAbel_addrightisiso [lemma, in CayleyGraph]
CayAbel_wont4c_ft [lemma, in CayleyGraph]
CayAbel_inversioniso [lemma, in CayleyGraph]
CayAbel_wont4c_common [lemma, in CayleyGraph]
CayAbel_wont4c_edgecomm_iso [lemma, in CayleyGraph]
CayAbel_without_nontrivial4cycles [definition, in CayleyGraph]
CayleyGraph [inductive, in CayleyGraph]
CayleyGraph [library]
CayleyGraphs [section, in CayleyGraph]
CayleyGraph_opp_rec [lemma, in CayleyGraph]
CayleyGraph_isoadjacencies [lemma, in CayleyGraph]
CayleyGraph_vertexsymmetric [lemma, in CayleyGraph]
CayleyGraph_isoIn [lemma, in CayleyGraph]
CayleyGraph_opp [lemma, in CayleyGraph]
CayleyGraph_addleftisiso [lemma, in CayleyGraph]
CayleyGraph_CommonNeighborhood [lemma, in CayleyGraph]
CayleyGraph_StronglyConnected [lemma, in CayleyGraph]
chaos [lemma, in Chaos]
Chaos [section, in Chaos]
Chaos [library]
Chaos_begin [section, in Chaos]
chaos_prev_rev [lemma, in Chaos]
Chaos_begin.suprayectiva [variable, in Chaos]
Chaos_begin.f [variable, in Chaos]
Chaos_begin.continua [variable, in Chaos]
Chaos_begin.f_01_01 [variable, in Chaos]
chaos_prev [lemma, in Chaos]
Chaos.continua [variable, in Chaos]
Chaos.f [variable, in Chaos]
Chaos.f_01_01 [variable, in Chaos]
Chaos.suprayectiva [variable, in Chaos]
Choice [lemma, in types_base]
ChoiceT_lemmas.bool_choice_aux2 [variable, in types_base]
ChoiceT_lemmas.R1 [variable, in types_base]
ChoiceT_lemmas.Choice2_aux [variable, in types_base]
ChoiceT_lemmas.R [variable, in types_base]
ChoiceT_lemmas.bool_choice_aux [variable, in types_base]
ChoiceT_lemmas.Choice_aux [variable, in types_base]
ChoiceT_lemmas.T [variable, in types_base]
ChoiceT_lemmas.Choice_aux2 [variable, in types_base]
ChoiceT_lemmas [section, in types_base]
ChoiceT_lemmas.T' [variable, in types_base]
ChoiceT_lemmas.Choice2_aux2 [variable, in types_base]
ChoiceT_lemmas.R' [variable, in types_base]
ChoiceT_lemmas.R2 [variable, in types_base]
Choice2 [lemma, in types_base]
circulant [library]
classicaltypes [library]
closed_set_half_down [lemma, in Chaos]
closed_set_half [lemma, in Chaos]
closed_set_intersection [lemma, in Chaos]
ColumnCons_HeadS_TailS [lemma, in Matrix_base]
ColumnDestructS [lemma, in Matrix_base]
ColumnHeadS_Column [lemma, in Matrix_base]
ColumnHeadS_Transpose [lemma, in Matrix_base]
ColumnHeadS_nil [lemma, in Matrix_base]
ColumnTailS_Transpose [lemma, in Matrix_base]
ColumnTailS_Column [lemma, in Matrix_base]
ColumnTailS_nil [lemma, in Matrix_base]
Column_ijth [lemma, in Matrix_base]
Column_headS [lemma, in Matrix_base]
Column_nth [lemma, in Matrix_base]
Column_eq_Transpose [lemma, in Matrix_base]
Column_tailS [lemma, in Matrix_base]
Column_cons [lemma, in Matrix_base]
Column_ijth_error [lemma, in Matrix_base]
CommonNeighborhood [definition, in graphs]
Commutativity [definition, in EnsembleFacts]
complementary_intersection [lemma, in Chaos]
compose [definition, in types_base]
Compose [definition, in EnsembleFacts]
composition_injective [lemma, in types]
cons [constructor, in Array]
consapp_ass [lemma, in Array]
cons_to_app [lemma, in Chaos]
cons_untype [lemma, in Array]
cons_type [lemma, in Array]
cons_in [lemma, in ListFacts]
cons_maptype [lemma, in Array]
cons_JMeq_length [lemma, in Array]
cons_JMeq_type [lemma, in Array]
cons_hd_tail [lemma, in Array]
cons_headS_tailS [lemma, in Array]
cons_different [lemma, in ListFacts]
cons_maptype_apply [lemma, in Array]
cons2D [definition, in Matrix_base]
contenido [definition, in Chaos]
contenido_self [lemma, in Chaos]
contenido_Intcontenido [lemma, in Chaos]
contenido_map_rangeInt [lemma, in Chaos]
contenido_map_rangeInt_rev [lemma, in Chaos]
continuity_identity [lemma, in Chaos]
count_occ_le [lemma, in ListFacts]
count_occ_app [lemma, in ListFacts]
CoupleComm [lemma, in EnsembleFacts]
Cutting [section, in Array]
Cutting.A [variable, in Array]
D
decons [lemma, in Array]decons_tail [lemma, in Array]
decons_head [lemma, in Array]
DependentChoice [lemma, in types_base]
DependentChoice_lemmas [section, in types_base]
DependentChoice_lemmas.DependentChoice_aux2 [variable, in types_base]
DependentChoice_lemmas.DependentChoice2_aux [variable, in types_base]
DependentChoice_lemmas.T [variable, in types_base]
DependentChoice_lemmas.R [variable, in types_base]
DependentChoice_lemmas.g [variable, in types_base]
DependentChoice_lemmas.DependentChoice2_aux2 [variable, in types_base]
DependentChoice_lemmas.R' [variable, in types_base]
DependentChoice_lemmas.DependentChoice_aux [variable, in types_base]
DependentChoice2 [lemma, in types_base]
DifferentAdd_Empty [lemma, in EnsembleFacts]
diff_comm [lemma, in Chaos]
diff_2_0 [lemma, in Chaos]
disc_destruct_up [lemma, in Chaos]
disc_destruct_down [lemma, in Chaos]
DisjointAddElim [lemma, in EnsembleFacts]
DisjointAddEquation [lemma, in EnsembleFacts]
DisjointAddEquationCommon [lemma, in EnsembleFacts]
DisjointAddEquationElim [lemma, in EnsembleFacts]
dtype [definition, in graphs]
E
EAT [definition, in EnsembleAsType]EAT_out_InA [lemma, in EnsembleAsType]
EAT_ex1set [definition, in EnsembleAsType]
EAT_out_in [lemma, in EnsembleAsType]
EAT_fout_simplify [lemma, in EnsembleAsType]
EAT_ex1 [definition, in EnsembleAsType]
EAT_in_exists [lemma, in EnsembleAsType]
EAT_out_intro [lemma, in EnsembleAsType]
EAT_existence [lemma, in EnsembleAsType]
EAT_ex2 [lemma, in EnsembleAsType]
EAT_in_fout [lemma, in EnsembleAsType]
EAT_in [definition, in EnsembleAsType]
EAT_in_out [lemma, in EnsembleAsType]
EAT_fout_InA [lemma, in EnsembleAsType]
EAT_out [definition, in EnsembleAsType]
EAT_fout [definition, in EnsembleAsType]
EAT_fout_in [lemma, in EnsembleAsType]
EAT_anyhypothesis [lemma, in EnsembleAsType]
ej1 [definition, in Vector]
ej2 [definition, in Vector]
ej3 [definition, in Vector]
ElementPartition [lemma, in EnsembleAsType]
ElementProduct_zero_l [lemma, in Vector]
ElementProduct_unit_diff [lemma, in Vector]
ElementProduct_zero_r [lemma, in Vector]
ElementProduct_unit_same [lemma, in Vector]
ElementProduct_unit_r [lemma, in Vector]
ElementProduct_unit_l [lemma, in Vector]
EnsembleAddComm [lemma, in EnsembleFacts]
EnsembleAddEmptyIsSingleton [lemma, in EnsembleFacts]
EnsembleAddIncludes [lemma, in EnsembleFacts]
EnsembleAddInto [lemma, in EnsembleFacts]
EnsembleAddToSub [lemma, in EnsembleFacts]
EnsembleApplyReduction [inductive, in EnsembleFacts]
EnsembleApplyReductionExistence [lemma, in EnsembleFacts]
EnsembleApplyReduction_empty [constructor, in EnsembleFacts]
EnsembleApplyReduction_add [constructor, in EnsembleFacts]
EnsembleAsType [section, in EnsembleAsType]
EnsembleAsType [inductive, in EnsembleAsType]
EnsembleAsType [library]
EnsembleAsTypeIntro [constructor, in EnsembleAsType]
EnsembleAsTypeOut [definition, in EnsembleAsType]
EnsembleAsTypeOut_isout [lemma, in EnsembleAsType]
EnsembleFacts [section, in EnsembleFacts]
EnsembleFacts [library]
EnsembleReduction [inductive, in EnsembleFacts]
EnsembleReductionExistence [lemma, in EnsembleFacts]
EnsembleReduction_add [constructor, in EnsembleFacts]
EnsembleReduction_empty [constructor, in EnsembleFacts]
EnsembleReduction_unique [lemma, in EnsembleFacts]
EnsemblesSingletonEqAdd [lemma, in EnsembleFacts]
EnsemblesSingletonEqDisjAdd [lemma, in EnsembleFacts]
EnsembleSubCardinal [lemma, in EnsembleFacts]
EnsembleSubFinite [lemma, in EnsembleFacts]
eqtype_ind_self [lemma, in classicaltypes]
eqtype_to_eq [lemma, in classicaltypes]
eqtype_to_eq [lemma, in axiomtypes]
eqtype_rect_self [lemma, in classicaltypes]
EqualCouples [lemma, in EnsembleFacts]
EquivalenceFormsPartition [lemma, in EnsembleAsType]
EquivalenceFromPartition [inductive, in EnsembleAsType]
EquivalenceFromPartition_equiv [lemma, in EnsembleAsType]
EquivalenceFromPartition_intro [constructor, in EnsembleAsType]
eq_closedset [lemma, in Chaos]
eq_JMeq [lemma, in JMeqmaptype]
eq_leibnitz [lemma, in types_base]
eq_injective [lemma, in types]
eq_rect_eq_nat [lemma, in Range]
eq_undo [lemma, in classicaltypes]
Examples [section, in JMeqmaptype]
Examples.app [variable, in JMeqmaptype]
Examples.ej1 [variable, in JMeqmaptype]
Examples.Emn [variable, in JMeqmaptype]
Examples.Exy [variable, in JMeqmaptype]
Examples.m [variable, in JMeqmaptype]
Examples.n [variable, in JMeqmaptype]
Examples.p [variable, in JMeqmaptype]
Examples.q [variable, in JMeqmaptype]
Examples.t [variable, in JMeqmaptype]
Examples.u [variable, in JMeqmaptype]
Examples.v [variable, in JMeqmaptype]
Examples.x [variable, in JMeqmaptype]
Examples.y [variable, in JMeqmaptype]
_ ++ _ [notation, in JMeqmaptype]
existsfunctions [lemma, in EnsembleFacts]
ExistsInverseOfBijective [lemma, in EnsembleFacts]
existsunique_to_function [lemma, in types_base]
exists_injective [lemma, in types]
Extensionality_Ensembles_rec [lemma, in EnsembleFacts]
F
Fold_Left_Recursor.B [variable, in Vector]fold_right_add_unit [lemma, in Vector]
Fold_Right_Recursor.B [variable, in Vector]
fold_right_ScalarProdVector [lemma, in Vector]
fold_right_VectorProdScalar [lemma, in Vector]
Fold_Left_Recursor.f [variable, in Vector]
fold_right_array_from_func_back [lemma, in Vector]
Fold_Right_Recursor.f [variable, in Vector]
Fold_Left_Recursor.A [variable, in Vector]
Fold_Right_Recursor.A [variable, in Vector]
fold_right_add_zero [lemma, in Vector]
fold_right_add_UnitVector [lemma, in Vector]
Fold_Right_Recursor [section, in Vector]
fold_left [definition, in Vector]
fold_right [definition, in Vector]
fold_right_app [lemma, in Vector]
fold_right_array_from_funcrange_back [lemma, in Vector]
Fold_Left_Recursor [section, in Vector]
fold_left_app [lemma, in Vector]
fold_right_shift [lemma, in Vector]
formulae_typeeq [lemma, in types]
function_typeeq [lemma, in types]
Function_bug [library]
f_repeat_commS [lemma, in Chaos]
f_JMequal_dependent_Prop [lemma, in JMeqmaptype]
f_JMequal_dependent_gs [lemma, in JMeqmaptype]
f_repeat [definition, in Chaos]
f_JMequal_dependent_g [lemma, in JMeqmaptype]
f_JMequal_dependent [lemma, in JMeqmaptype]
f_repeat_plus [lemma, in Chaos]
f_JMequal [lemma, in JMeqmaptype]
f_repeat_comm [lemma, in Chaos]
f_repeat_continua [lemma, in Chaos]
f_JMequal_dependent_base [lemma, in JMeqmaptype]
f_JMequal_dependent_g_Prop [lemma, in JMeqmaptype]
f2_JMequal_s [lemma, in JMeqmaptype]
f2_JMequal [lemma, in JMeqmaptype]
f3_JMequal2 [lemma, in JMeqmaptype]
f3_JMequal3 [lemma, in JMeqmaptype]
f3_JMequal4 [lemma, in JMeqmaptype]
f3_JMequal [lemma, in JMeqmaptype]
G
Geometry [library]glb_closed [lemma, in Chaos]
godel [library]
Graph [definition, in graphs]
graphs [section, in graphs]
graphs [library]
Graph_isominverse [lemma, in graphs]
Graph_isocomposition [lemma, in graphs]
Group [definition, in Groups]
Groups [section, in Groups]
Groups [library]
Groups.f [variable, in Groups]
Groups.U [variable, in Groups]
Group_AddMult_Shift [lemma, in Groups]
Group_additioninverse [lemma, in Groups]
Group_ShiftLeftTerm [lemma, in Groups]
Group_inversesref [lemma, in Groups]
Group_inversescommute [lemma, in Groups]
Group_is_Monoid [lemma, in Groups]
Group_indentityinverse [lemma, in Groups]
Group_identityfrominverses [lemma, in Groups]
Group_Inversion [definition, in Groups]
Group_rightsimplifyinverses [lemma, in Groups]
Group_SimplifyInversion [lemma, in Groups]
Group_leftsimplifyinverses [lemma, in Groups]
Group_existsidentity [lemma, in Groups]
Group_ShiftInversion [lemma, in Groups]
Group_ElimInverseIdentity [lemma, in Groups]
Group_inversesareidentity [lemma, in Groups]
Group_ShiftRightTerm [lemma, in Groups]
Group_leftsimplify [lemma, in Groups]
Group_DoubleInversion [lemma, in Groups]
Group_InversionOfAdd [lemma, in Groups]
Group_AddMult [definition, in Groups]
Group_leftadd [lemma, in Groups]
Group_AddMult_Extract [lemma, in Groups]
Group_InversionFromInverses [lemma, in Groups]
Group_inversesidentity [lemma, in Groups]
Group_InversionIsBijection [lemma, in Groups]
Group_InversionAsInverses [lemma, in Groups]
Group_refinverses [lemma, in Groups]
Group_rightadd [lemma, in Groups]
Group_ElimInversesRight [lemma, in Groups]
Group_existsInversion [lemma, in Groups]
Group_ElimInversesLeft [lemma, in Groups]
Group_uniqueinverse [lemma, in Groups]
Group_uniqueidentity [lemma, in Groups]
Group_existsinverse [lemma, in Groups]
Group_addrightisbijection [lemma, in Groups]
Group_addleftisbijection [lemma, in Groups]
Group_AddMult_Step [lemma, in Groups]
Group_rightsimplify [lemma, in Groups]
H
HasIdentity [definition, in Groups]HasInverses [definition, in Groups]
hd [definition, in Array]
head [definition, in Array]
headS [definition, in Array]
headS_ColumnTailS [lemma, in Matrix_base]
headS_Transpose [lemma, in Matrix_base]
headS_hd [lemma, in Array]
headS_ColumnHeadS [lemma, in Matrix_base]
head_hd [lemma, in Array]
head_and_body [lemma, in Array]
HorizontalAppend_nil2D [lemma, in Matrix_base]
HorizontalAppend_commuteC [lemma, in Matrix_base]
HorizontalAppend_ColumnTailS_C [lemma, in Matrix_base]
HorizontalAppend_ColumnHeadS [lemma, in Matrix_base]
HorizontalAppend_ijth_right [lemma, in Matrix_base]
HorizontalAppend_commute_tailS [lemma, in Matrix_base]
HorizontalAppend_nil_l [lemma, in Matrix_base]
HorizontalAppend_nthC_left [lemma, in Matrix_base]
HorizontalAppend_associative [lemma, in Matrix_base]
HorizontalAppend_ColumnTailS [lemma, in Matrix_base]
HorizontalAppend_ColumnHeadS_C [lemma, in Matrix_base]
HorizontalAppend_commute [lemma, in Matrix_base]
HorizontalAppend_commute_headS [lemma, in Matrix_base]
HorizontalAppend_nil_r [lemma, in Matrix_base]
HorizontalAppend_type [lemma, in Matrix_base]
HorizontalAppend_nthC_right [lemma, in Matrix_base]
HorizontalAppend_ijth_left [lemma, in Matrix_base]
HorizontalAppend_associativeC [lemma, in Matrix_base]
hurry [library]
I
Identity [definition, in Groups]IdentityMatrix [definition, in Matrix_base]
IdentityMatrix_Transpose [lemma, in Matrix_base]
IdentityMatrix_ijth_range [lemma, in Matrix_base]
IdentityMatrix_ijth [lemma, in Matrix_base]
IdentityMatrix_Symmetric [lemma, in Matrix_base]
idInterval [definition, in Chaos]
id_injective [lemma, in types]
ijth [definition, in Matrix_base]
ijth_error_nth_error_D [lemma, in Matrix_base]
ijth_nth_d [lemma, in Matrix_base]
ijth_range_eq [lemma, in Matrix_base]
ijth_error_tailS [lemma, in Matrix_base]
ijth_error [definition, in Matrix_base]
ijth_error_headS [lemma, in Matrix_base]
ijth_range_error_eq [lemma, in Matrix_base]
ijth_out [lemma, in Matrix_base]
ijth_range [definition, in Matrix_base]
ijth_headS [lemma, in Matrix_base]
ijth_nth [lemma, in Matrix_base]
ijth_equality [lemma, in Matrix_base]
ijth_error_nth_error_d [lemma, in Matrix_base]
ijth_tailS [lemma, in Matrix_base]
ijth_range_equality [lemma, in Matrix_base]
ijth_error_eq [lemma, in Matrix_base]
illtypebug [library]
injective [definition, in types]
inrange [definition, in Chaos]
Intcontenido [definition, in Chaos]
Intcontenido_contenido [lemma, in Chaos]
Intcontenido_self [lemma, in Chaos]
Interval [record, in Chaos]
Inverse [definition, in Groups]
InverseFunction [definition, in EnsembleFacts]
InverseOfBijectiveIsBijective [lemma, in EnsembleFacts]
In_CayleyGraph_recgroup [lemma, in CayleyGraph]
In_CayleyGraph [constructor, in CayleyGraph]
In_CayleyGraph_rec [lemma, in CayleyGraph]
In_nth [lemma, in ListFacts]
In_apply_func [constructor, in EnsembleFacts]
In_Neighborhood [constructor, in graphs]
Isomorph [definition, in graphs]
Isomorphism [definition, in graphs]
Isomorphism_In_rec [lemma, in graphs]
Isomorphism_In [lemma, in graphs]
isom_commonneighbor [lemma, in graphs]
isom_outdegree [lemma, in graphs]
isom_neighbor [lemma, in graphs]
is_lower_bound [definition, in Chaos]
is_glb [definition, in Chaos]
IVT_any [lemma, in Chaos]
IVT_any_rev [lemma, in Chaos]
J
JMeqmaptype [library]JMeq_maptype_eq [lemma, in JMeqmaptype]
JMeq_dependent_g [lemma, in JMeqmaptype]
JMeq_maptype [lemma, in JMeqmaptype]
JMeq_typeeq [lemma, in JMeqmaptype]
JMex [lemma, in JMeqmaptype]
JMfunctional_extensionality [lemma, in JMeqmaptype]
JMfunctional2_extensionality [lemma, in JMeqmaptype]
JMfunctional3_extensionality_dep [lemma, in JMeqmaptype]
JMfunctional3_extensionality [lemma, in JMeqmaptype]
K
Kronecker_delta_diff [lemma, in Vector]Kronecker_delta_refl [lemma, in Vector]
Kronecker_delta [definition, in Vector]
Kronecker_delta_sym [lemma, in Vector]
K_nat [lemma, in Range]
L
lbound [definition, in Chaos]lcompleteness [lemma, in Chaos]
le [projection, in Chaos]
LeftIdentity [definition, in Groups]
LeftInverse [definition, in Groups]
lema0 [lemma, in Chaos]
lema1 [lemma, in Chaos]
lema2 [lemma, in Chaos]
Lema2 [section, in Chaos]
lema2a [lemma, in Chaos]
lema2eq [lemma, in Chaos]
Lema2.continua [variable, in Chaos]
Lema2.f [variable, in Chaos]
length [definition, in Array]
le_lowrange [definition, in Range]
le_lowrange_in [lemma, in Range]
le_uniqueness_proof [lemma, in Range]
listcons [definition, in Array]
ListFacts [library]
listnil [definition, in Array]
listpairs [definition, in ListFacts]
listpairscycle [definition, in ListFacts]
listpairscycle_last [lemma, in ListFacts]
listpairscycle_fst [lemma, in ListFacts]
listpairscycle_consecutive [lemma, in ListFacts]
listpairscycle_length [lemma, in ListFacts]
listpairscycle_Inexbef [lemma, in ListFacts]
listpairscycle_head [lemma, in ListFacts]
listpairscycle_nth [lemma, in ListFacts]
listpairscycle_doublesame [lemma, in ListFacts]
listpairscycle_break [lemma, in ListFacts]
listpairscycle_double [lemma, in ListFacts]
listpairs_length [lemma, in ListFacts]
listpairs_nth [lemma, in ListFacts]
listpairs_double [lemma, in ListFacts]
listpairs_Inexbef [lemma, in ListFacts]
listpairs_cons [lemma, in ListFacts]
listpairs_app [lemma, in ListFacts]
list_eq_nth_to_ntherror [lemma, in ListFacts]
list_ntherror_inR [lemma, in ListFacts]
list_last_cons2 [lemma, in ListFacts]
list_last_Incons [lemma, in ListFacts]
list_lastelim [lemma, in graphs]
list_last_In [lemma, in ListFacts]
list_ntherror_nth [lemma, in ListFacts]
list_lastpushback [lemma, in graphs]
list_inpushbackrev [lemma, in graphs]
list_ntherror_out [lemma, in ListFacts]
list_hderror_ntherror [lemma, in ListFacts]
list_zerolength [lemma, in graphs]
list_pushbacknotnil [lemma, in graphs]
list_last_cons [lemma, in ListFacts]
list_inpushbacknew [lemma, in graphs]
list_last_nth [lemma, in ListFacts]
list_nth_out [lemma, in ListFacts]
list_lengthpushback [lemma, in graphs]
list_pushback [definition, in graphs]
list_hdpushbackrev [lemma, in graphs]
list_inpushback [lemma, in graphs]
list_nonzerolengthback [lemma, in graphs]
list_nonzerolength [lemma, in graphs]
list_eq_ntherror_to_nth [lemma, in ListFacts]
list_ntherror_outR [lemma, in ListFacts]
list_foldleft_pushback [lemma, in graphs]
list_hdpushback [lemma, in graphs]
list_hdchangebase [lemma, in graphs]
list_last_other [lemma, in ListFacts]
list_last_app [lemma, in ListFacts]
list_ntherror_inL [lemma, in ListFacts]
list_hd_nth [lemma, in ListFacts]
lowrange [definition, in Range]
lowrange_prevfunc_injective [lemma, in Range]
lowrange_prevfunc [definition, in Range]
lowrange_identity [definition, in Range]
lowrange_injective_P_func_aux2 [lemma, in Range]
lowrange_injective_S [lemma, in Range]
lowrange_eq [lemma, in Range]
lowrange_injective_P_func [definition, in Range]
lowrange_injective_S_func_aux [lemma, in Range]
lowrange_injective_n0 [lemma, in Range]
lowrange_0_unique [lemma, in Range]
lowrange_exist_eq [lemma, in Range]
lowrange_lowrangtS_identity [definition, in Range]
lowrange_injective_le [lemma, in Range]
lowrange_injective_n [lemma, in Range]
lowrange_S_pair [lemma, in Range]
lowrange_identity_injective [lemma, in Range]
lowrange_lowrangtS_identity_injective [lemma, in Range]
lowrange_injective_P_func_aux [lemma, in Range]
lowrange_injective_le_fun [definition, in Range]
lowrange_injective_S_func [definition, in Range]
lowrange_discr [lemma, in Range]
lowrange_injective_P [definition, in Range]
lowrange_identity_le [lemma, in Range]
lowrangt [definition, in Range]
lowrangtS_lowrange_identity [definition, in Range]
lowrangtS_lowrange_identity_injective [lemma, in Range]
lowrangt_0_nonihabited [lemma, in Range]
lowrangt_exist_eq [lemma, in Range]
lowrangt_S_ihabited [lemma, in Range]
lowrangt_lowrange_identity [definition, in Range]
lowrangt_lowrange_identity_injective [lemma, in Range]
lowrangt_prevfunc [definition, in Range]
lowrangt_injective_0 [lemma, in Range]
lowrangt_injective_n [lemma, in Range]
lowrangt_injective_Sn [lemma, in Range]
lowrangt_identity [definition, in Range]
lowrangt_discr [lemma, in Range]
lt_uniqueness_proof [lemma, in Range]
lub_closed [lemma, in Chaos]
M
makevar_tactic [definition, in types_base]map [definition, in Chaos]
maprepeat_idInterval [lemma, in Chaos]
maptype [definition, in JMeqmaptype]
maptypeconstruct [library]
maptype_compose [lemma, in JMeqmaptype]
maptype_application_t [lemma, in JMeqmaptype]
maptype_selfany [lemma, in axiomtypes]
maptype_rect [lemma, in axiomtypes]
maptype_combine_l [lemma, in JMeqmaptype]
maptype_ind_t [lemma, in axiomtypes]
maptype_square [lemma, in JMeqmaptype]
maptype_dependent [lemma, in JMeqmaptype]
maptype_square2 [lemma, in JMeqmaptype]
maptype_fun [lemma, in JMeqmaptype]
maptype_selfany [lemma, in classicaltypes]
maptype_mapproduct [lemma, in axiomtypes]
maptype_dependent_g [lemma, in axiomtypes]
maptype_sym [lemma, in axiomtypes]
maptype_trans [lemma, in JMeqmaptype]
maptype_mapproduct [lemma, in JMeqmaptype]
maptype_application [axiom, in axiomtypes]
maptype_pi [definition, in JMeqmaptype]
maptype_rect_r [lemma, in axiomtypes]
maptype_rectX [lemma, in axiomtypes]
maptype_returnpi [lemma, in JMeqmaptype]
maptype_constant [lemma, in axiomtypes]
maptype_combine_r [lemma, in JMeqmaptype]
maptype_pi [lemma, in classicaltypes]
maptype_dependent_g [lemma, in JMeqmaptype]
maptype_identity [lemma, in axiomtypes]
maptype_binary [lemma, in JMeqmaptype]
maptype_rect_tr [lemma, in axiomtypes]
maptype_square [lemma, in axiomtypes]
maptype_undo [lemma, in JMeqmaptype]
maptype_fun_t [lemma, in JMeqmaptype]
maptype_returnpi [lemma, in axiomtypes]
maptype_ind [lemma, in axiomtypes]
maptype_JMeq_g [lemma, in JMeqmaptype]
maptype_JMeq [lemma, in JMeqmaptype]
maptype_undo [lemma, in axiomtypes]
maptype_selfany [lemma, in JMeqmaptype]
maptype_rect_t [lemma, in axiomtypes]
maptype_proof_irrelevance [lemma, in JMeqmaptype]
maptype_preserveidentity [lemma, in JMeqmaptype]
maptype_trans [axiom, in axiomtypes]
maptype_application_t [axiom, in axiomtypes]
maptype_identity [lemma, in JMeqmaptype]
maptype_proof_irrelevance [lemma, in axiomtypes]
maptype_fun [lemma, in axiomtypes]
maptype_sym [lemma, in JMeqmaptype]
maptype_application [lemma, in JMeqmaptype]
maptype_fun_t [lemma, in axiomtypes]
maptype_dependent [lemma, in axiomtypes]
maptype_standard [library]
map_repeat_to_f_repeat [lemma, in Chaos]
map_repeat [definition, in Chaos]
map_idInterval [lemma, in Chaos]
map_repeat_comm [lemma, in Chaos]
map_repeat_cons [lemma, in Chaos]
match_boolunique [lemma, in types]
Matrix [library]
MatrixAdd [definition, in Matrix_arith]
MatrixAdd_ijth [lemma, in Matrix_arith]
MatrixAdd_nil [lemma, in Matrix_arith]
MatrixAdd_associativity [lemma, in Matrix_arith]
MatrixAdd_single [lemma, in Matrix_arith]
MatrixAdd_d [definition, in Matrix_arith]
MatrixAdd_d_nil [lemma, in Matrix_arith]
MatrixAdd_d_single [lemma, in Matrix_arith]
MatrixAdd_commutativity [lemma, in Matrix_arith]
MatrixProduct [definition, in Matrix_arith]
MatrixProduct_Zero_l [lemma, in Matrix_arith]
MatrixProduct_summatory [lemma, in Matrix_arith]
MatrixProduct_Zero_r [lemma, in Matrix_arith]
MatrixProduct_associativity [lemma, in Matrix_arith]
MatrixSymmetric [definition, in Matrix_base]
MatrixSymmetric_ijth [lemma, in Matrix_base]
MatrixSymmetric_ijth_range [lemma, in Matrix_base]
matrix_from_funcrange_extensionalityR [lemma, in Matrix_base]
matrix_from_func_ijth [lemma, in Matrix_base]
matrix_from_funcrange_ijth_range [lemma, in Matrix_base]
Matrix_col_summatory [lemma, in Matrix_arith]
matrix_from_funcrange [definition, in Matrix_base]
matrix_from_func [definition, in Matrix_base]
matrix_from_func_ijth_error [lemma, in Matrix_base]
Matrix_row_summatory [lemma, in Matrix_arith]
matrix_from_func_extensionality [lemma, in Matrix_base]
Matrix_arith [library]
Matrix_base [library]
minperiod [definition, in Chaos]
minperiod_f [lemma, in Chaos]
minperiod0 [lemma, in Chaos]
mkInt [constructor, in Chaos]
Monoid [definition, in Groups]
Monoid_uniqueinverse [lemma, in Groups]
N
natfunc_lowrange_Prop [definition, in Range]natfunc_lowrange [definition, in Range]
natfunc_lowrangt [definition, in Range]
nat_destruct [lemma, in types]
nat_firsts_def [constructor, in Zfacts]
nat_firsts [inductive, in Zfacts]
Neighborhood [inductive, in graphs]
neighbor_cardinal [constructor, in graphs]
Network [library]
nil [constructor, in Array]
nilC [definition, in Matrix_base]
nil2D [definition, in Matrix_base]
NonEmptyAsAdd [lemma, in EnsembleFacts]
nth [definition, in Array]
nthC [definition, in Matrix_base]
nthC_out [lemma, in Matrix_base]
nthC_error_out [lemma, in Matrix_base]
nthC_range_ColumnHeadS [lemma, in Matrix_base]
nthC_range_matrix_from_funcrange [lemma, in Matrix_base]
nthC_error_ColumnHeadS [lemma, in Matrix_base]
nthC_range_eq [lemma, in Matrix_base]
nthC_nth [lemma, in Matrix_base]
nthC_headS [lemma, in Matrix_base]
nthC_error_eq [lemma, in Matrix_base]
nthC_error_ColumnTailS [lemma, in Matrix_base]
nthC_anydefault [lemma, in Matrix_base]
nthC_range_ColumnTailS [lemma, in Matrix_base]
nthC_range [definition, in Matrix_base]
nthC_range_nth_range [lemma, in Matrix_base]
nthC_ColumnTailS [lemma, in Matrix_base]
nthC_nth_R [lemma, in Matrix_base]
nthC_matrix_from_func [lemma, in Matrix_base]
nthC_ColumnHeadS [lemma, in Matrix_base]
nthC_type [definition, in Matrix_base]
nthC_tailS [lemma, in Matrix_base]
nthC_error [definition, in Matrix_base]
nth_range_summatoryv [lemma, in Matrix_arith]
nth_out [lemma, in Array]
nth_error_tailS [lemma, in Array]
nth_error_headS [lemma, in Array]
nth_range_matrix_from_funcrange [lemma, in Matrix_base]
nth_range_tailS [lemma, in Array]
nth_ColumnTailS [lemma, in Matrix_base]
nth_range_equality [lemma, in Array]
nth_range_headS [lemma, in Array]
nth_tailS [lemma, in Array]
nth_error_eq [lemma, in Array]
nth_range_eq [lemma, in Array]
nth_ColumnHeadS [lemma, in Matrix_base]
nth_error_out [lemma, in Array]
nth_range_JMequality [lemma, in Array]
nth_error [definition, in Array]
nth_equality [lemma, in Array]
nth_error_equality [lemma, in Array]
nth_headS [lemma, in Array]
nth_range [definition, in Array]
nth_anydefault [lemma, in Array]
O
Operation [definition, in EnsembleFacts]outdegree [inductive, in graphs]
outregular [definition, in graphs]
P
Partition [definition, in EnsembleAsType]PartitionExlusive [lemma, in EnsembleAsType]
PartitionFromEquivalence [definition, in EnsembleAsType]
PartitionFromEquivalence_out [lemma, in EnsembleAsType]
PartitionFromEquivalence_intro [lemma, in EnsembleAsType]
Path [inductive, in graphs]
PathExtractBack [lemma, in graphs]
Path_nonemptyback [lemma, in graphs]
Path_nonempty [constructor, in graphs]
Path_empty [constructor, in graphs]
Path_single [constructor, in graphs]
period [definition, in Chaos]
period_f_rev [lemma, in Chaos]
period_f [lemma, in Chaos]
positivereduced [library]
posreal_destruct [lemma, in Chaos]
Preimage [definition, in Chaos]
preimage_closed [lemma, in Chaos]
preimage_complementary [lemma, in Chaos]
Product_unit_l [lemma, in Matrix_arith]
Product_nil_l [lemma, in Matrix_arith]
Product_unit_r [lemma, in Matrix_arith]
Product_nil_r [lemma, in Matrix_arith]
Product_nil_c [lemma, in Matrix_arith]
Q
QuotientGroup [library]R
range [definition, in Range]Range [library]
rangeInt [definition, in Chaos]
rangeInt_b [lemma, in Chaos]
rangeInt_a [lemma, in Chaos]
rangt [definition, in Range]
RealLemmas [section, in Chaos]
RealLemmas' [section, in Chaos]
RealLemmas'.continua [variable, in Chaos]
RealLemmas'.f [variable, in Chaos]
RealLemmas'.f_01_01 [variable, in Chaos]
RealLemmas'.suprayectiva [variable, in Chaos]
RealLemmas.continua [variable, in Chaos]
RealLemmas.f [variable, in Chaos]
RealLemmas.f_01_01 [variable, in Chaos]
RealLemmas.suprayectiva [variable, in Chaos]
real_le_signchange_r [lemma, in Chaos]
real_le_signchange_l [lemma, in Chaos]
real_glb_eq2 [lemma, in Chaos]
real_glb_eq [lemma, in Chaos]
real_lub_eq2 [lemma, in Chaos]
real_lub_eq [lemma, in Chaos]
real_middlepoint [lemma, in Chaos]
RelatedByEquivalence [lemma, in EnsembleAsType]
RelatedElements [inductive, in EnsembleAsType]
RelatedElements_intro [constructor, in EnsembleAsType]
removelast_different [lemma, in ListFacts]
removelast_length [lemma, in ListFacts]
removelast_lengthle [lemma, in ListFacts]
RightIdentity [definition, in Groups]
RightInverse [definition, in Groups]
Rings [library]
rotatelist [definition, in ListFacts]
rotatelistn [definition, in ListFacts]
rotatelistn_ntherror [lemma, in ListFacts]
rotatelistn_InL [lemma, in ListFacts]
rotatelistn_cons [lemma, in ListFacts]
rotatelistn_plus [lemma, in ListFacts]
rotatelistn_nil [lemma, in ListFacts]
rotatelistn_InR [lemma, in ListFacts]
rotatelistn_periodic [lemma, in ListFacts]
rotatelistn_length [lemma, in ListFacts]
rotatelistn_count [lemma, in ListFacts]
rotatelistn_listpairscycle [lemma, in ListFacts]
rotatelistn_app [lemma, in ListFacts]
rotatelistn_rotatelist [lemma, in ListFacts]
rotatelistn_nilinv [lemma, in ListFacts]
rotatelistn_hderror [lemma, in ListFacts]
rotatelistn_single [lemma, in ListFacts]
rotatelistn_comm [lemma, in ListFacts]
rotatelist_InL [lemma, in ListFacts]
rotatelist_listpairscycle [lemma, in ListFacts]
rotatelist_nilinv [lemma, in ListFacts]
rotatelist_hderror [lemma, in ListFacts]
rotatelist_ntherrorS [lemma, in ListFacts]
rotatelist_cons [lemma, in ListFacts]
rotatelist_InR [lemma, in ListFacts]
rotatelist_topair [lemma, in ListFacts]
rotatelist_ntherror [lemma, in ListFacts]
rotatelist_to [lemma, in ListFacts]
rotatelist_count [lemma, in ListFacts]
rotatelist_length [lemma, in ListFacts]
S
SameCouple [lemma, in EnsembleFacts]ScalarProduct_unit_diff [lemma, in Vector]
ScalarProduct_cons [lemma, in Vector]
ScalarProduct_unit_l [lemma, in Vector]
ScalarProduct_app [lemma, in Vector]
ScalarProduct_zero_l [lemma, in Vector]
ScalarProduct_unit_r [lemma, in Vector]
ScalarProduct_ScalarProdVector_l [lemma, in Vector]
ScalarProduct_zero_r [lemma, in Vector]
ScalarProduct_summatory_r [lemma, in Matrix_arith]
ScalarProduct_single [lemma, in Vector]
ScalarProduct_as_fold [lemma, in Vector]
ScalarProduct_comm [lemma, in Matrix_arith]
ScalarProduct_VectorProdScalar_r [lemma, in Vector]
ScalarProduct_as_summatory [lemma, in Vector]
ScalarProduct_summatory_l [lemma, in Matrix_arith]
ScalarProduct_nil [lemma, in Vector]
ScalarProduct_commutative [lemma, in Vector]
ScalarProduct_unit_same [lemma, in Vector]
ScalarProdVector [definition, in Vector]
ScalarProdVector_nth_range [lemma, in Vector]
selfincluded [lemma, in EnsembleFacts]
Singleton_compact [lemma, in Chaos]
single_notnil [lemma, in Array]
StronglyConnected [definition, in graphs]
SubPath [lemma, in graphs]
SubPathBack [lemma, in graphs]
summatoryS [lemma, in Vector]
summatory_add [lemma, in Vector]
summatory_swap [lemma, in Vector]
summatory_Kronecker_delta [lemma, in Vector]
summatory_Kronecker_delta_out [lemma, in Vector]
summatory_fR_Kronecker_delta [lemma, in Vector]
summatory_prod_l [lemma, in Vector]
summatory_prod_r [lemma, in Vector]
summatory_extensionality [lemma, in Vector]
summatory0 [lemma, in Vector]
sym_eqtype [lemma, in axiomtypes]
T
tail [definition, in Array]tailS [definition, in Array]
tailsequal [lemma, in Array]
tailS_tail [lemma, in Array]
tailS_ColumnHeadS [lemma, in Matrix_base]
tailS_ColumnTailS [lemma, in Matrix_base]
tailS_Transpose [lemma, in Matrix_base]
tailS0_nil [lemma, in Array]
tail1_nil [lemma, in Array]
transform [lemma, in axiomtypes]
TransposeProduct [lemma, in Matrix_arith]
TransposeTranspose [lemma, in Matrix_base]
TransposeZeroMatrix [lemma, in Matrix_arith]
Transpose_ijth_range [lemma, in Matrix_base]
Transpose_ijth [lemma, in Matrix_base]
Transpose_type [definition, in Matrix_base]
Transpose_nth_range [lemma, in Matrix_base]
Transpose_nth [lemma, in Matrix_base]
Transpose_Ctype [definition, in Matrix_base]
Transpose_nthC [lemma, in Matrix_base]
Transpose_nil [lemma, in Matrix_base]
Transpose_nthC_range [lemma, in Matrix_base]
trans_eqtype [lemma, in axiomtypes]
Turing [library]
tutorial [library]
typerewrite_simple [lemma, in axiomtypes]
typerewrite_Prop [lemma, in axiomtypes]
types [library]
typesdecission [library]
types_base [library]
U
Undirected [definition, in graphs]undirected_neighbor_sym [lemma, in graphs]
UndoInverse [lemma, in EnsembleFacts]
UndoInverseBijective [lemma, in EnsembleFacts]
UndoInverseSym [lemma, in EnsembleFacts]
uniqueidentity [lemma, in Groups]
UniquePartition [lemma, in EnsembleAsType]
unique_appending [lemma, in Array]
UnitVector [definition, in Vector]
UnitVector_as_app_construct [lemma, in Vector]
UnitVector_as_app [lemma, in Vector]
usingensembles [library]
V
Vector [section, in Vector]Vector [library]
VectorAdd_commutativity [lemma, in Vector]
VectorAdd_R [definition, in Vector]
VectorAdd_d_eq [lemma, in Vector]
VectorAdd_nth_range [lemma, in Vector]
VectorAdd_zerovector_l [lemma, in Vector]
VectorAdd_R_single [lemma, in Vector]
VectorAdd_R_nil [lemma, in Vector]
VectorAdd_R_eq [lemma, in Vector]
VectorAdd_associativity [lemma, in Vector]
VectorAdd_d_commutativity [lemma, in Vector]
VectorAdd_d_nil [lemma, in Vector]
VectorAdd_app [lemma, in Vector]
VectorAdd_single [lemma, in Vector]
VectorAdd_zerovector_r [lemma, in Vector]
VectorAdd_d_app [lemma, in Vector]
VectorAdd_d_associativity [lemma, in Vector]
VectorAdd_Rd_eq [lemma, in Vector]
VectorAdd_d [definition, in Vector]
VectorAdd_d_single [lemma, in Vector]
VectorAdd_nth [lemma, in Vector]
VectorAdd_nil [lemma, in Vector]
VectorProdScalar [definition, in Vector]
VectorProdScalar_nth_range [lemma, in Vector]
Vector.U [variable, in Vector]
vertexsymmetric [definition, in graphs]
vertexsymmetric_outregular [lemma, in graphs]
VerticalAppend [definition, in Matrix_base]
VerticalAppend_commute [lemma, in Matrix_base]
VerticalAppend_commute_ColumnHeadS_C [lemma, in Matrix_base]
VerticalAppend_Column [lemma, in Matrix_base]
VerticalAppend_commute_ColumnTailS [lemma, in Matrix_base]
VerticalAppend_commuteR [lemma, in Matrix_base]
VerticalAppend_commute_ColumnHeadS [lemma, in Matrix_base]
Z
ZeroMatrix [definition, in Matrix_base]ZeroMatrix_ijth [lemma, in Matrix_base]
ZeroMatrix_Transpose [lemma, in Matrix_base]
ZeroMatrix_Symmetric [lemma, in Matrix_base]
ZeroMatrix_ijth_range [lemma, in Matrix_base]
Zfacts [section, in Zfacts]
Zfacts [library]
Zmod [section, in Zmod]
Zmod [axiom, in Zmod]
Zmod [library]
Zmodeg_parity [lemma, in Zmod]
Zmodeg_equiv7_1_8 [lemma, in Zmod]
Zmodeg_add10_1_8 [lemma, in Zmod]
Zmodequiv [definition, in Zmod]
Zmodequivalence_right [axiom, in Zmod]
Zmodequivalence_left [axiom, in Zmod]
ZmodN [axiom, in Zmod]
Zmod_nat_repsetnat [lemma, in Zmod]
Zmod_elim [axiom, in Zmod]
Zmod_repset [definition, in Zmod]
Zmod_repsetnat [definition, in Zmod]
Zmod_opp [lemma, in Zmod]
Zmod_add [axiom, in Zmod]
Zmod_add_Z [axiom, in Zmod]
Zmod_canonical [lemma, in Zmod]
Zmod_haspos [lemma, in Zmod]
Zmod_addisbijection [lemma, in Zmod]
Zmod_addition [lemma, in Zmod]
Z_ge_mulpos [lemma, in Zfacts]
Z_absnat_posgt0 [lemma, in Zfacts]
Z_getpositive [lemma, in Zfacts]
Z_absnat_0 [lemma, in Zfacts]
Z_absnat_posge0 [lemma, in Zfacts]
Z_gt_mulpos [lemma, in Zfacts]
Z_ge_multwopos [lemma, in Zfacts]
Z_gt_divpos [lemma, in Zfacts]
Z_eucdiff [lemma, in Zfacts]
_
_Matrix_arith_summatory_swap [lemma, in Matrix_arith]other
_ ++ _ (array_scope) [notation, in Array]_ :: _ (array_scope) [notation, in Array]
_ +V+ _ (matrix_scope) [notation, in Matrix_base]
_ +H+ _ (matrix_scope) [notation, in Matrix_base]
_ o _ (type_scope) [notation, in types_base]
_ == _ :> _ _ [notation, in JMeqmaptype]
_ == _ [notation, in JMeqmaptype]
Projection Index
A
a [in Chaos]B
b [in Chaos]L
le [in Chaos]Record Index
I
Interval [in Chaos]Lemma Index
A
AlistIndec [in ListFacts]AppendCommuteDimensions [in Matrix_base]
AppendCommuteDimensions_RC [in Matrix_base]
AppendCommuteDimensions_R [in Matrix_base]
apply_func_intersection [in EnsembleFacts]
apply_func_singleton [in EnsembleFacts]
apply_func_add [in EnsembleFacts]
apply_func_finite [in EnsembleFacts]
apply_func_rec [in EnsembleFacts]
apply_func_empty [in EnsembleFacts]
apply_func_equation [in EnsembleFacts]
apply_func_couple [in EnsembleFacts]
app_headS [in Array]
app_from_appending [in Array]
app_ass [in Array]
app_nil_r [in Array]
app_single_l [in Array]
app_is_appending [in Array]
app_S [in Array]
app_tailS [in Array]
app_headS_tailS [in Array]
app_equality [in Array]
app_nil_l [in Array]
app_nth_right [in Array]
app_nth_left [in Array]
array_from_func_eq [in Array]
array_homogeneous_nth_range [in Array]
array_from_func_nth_aux [in Array]
array_from_funcrange_aux_H [in Array]
array_from_funcrange_nth_range [in Array]
array_from_funcrange_aux_head_eq [in Array]
array_from_func_nth_range [in Array]
array_0_nil [in Array]
array_from_funcrange_nth_error [in Array]
array_from_funcrange_nth_range_aux2 [in Array]
array_from_func_back [in Array]
array_destruct [in Array]
array_from_funcrange_nth_error_aux [in Array]
array_list_app [in Array]
array_homogeneous_nth_same [in Array]
array_single [in Array]
array_from_func_aux_eq [in Array]
array_from_func_nth_error_aux [in Array]
array_homogeneous_nth [in Array]
array_rewrite_dependent_Prop [in Array]
array_S_ht [in Array]
array_from_func_nth_error [in Array]
array_from_funcrange_back [in Array]
array_to_arrayfromfunc [in Array]
array_from_funcrange_aux_destructS [in Array]
array_from_funcrange_nth_range_aux [in Array]
array_rewrite_dependent [in Array]
array_single_type [in Array]
array_1_head [in Array]
array_typeequality_up [in Array]
array_from_funcrange_extensionality [in Array]
array_noninhabited [in Array]
array_from_func_extensionality [in Array]
array_destructS [in Array]
array_as_list_cero [in Array]
array_list_cons [in Array]
array_from_funcrange_extensionalityR [in Array]
array_nil_n0 [in Array]
array_typeequality [in Array]
array_homogeneous_app [in Array]
array_from_func_nth [in Array]
array_Function0 [in Array]
array_cut [in Array]
array_n0_nil [in Array]
array_to_arrayfromfuncrange [in Array]
array_from_funcrange_aux_destruct0 [in Array]
array_FunctionS [in Array]
array_assoc [in Array]
array2D_rewrite_dependent_H_Prop [in Matrix_base]
array2D_0_nilC [in Matrix_base]
array2D_1_Column [in Matrix_base]
array2D_rewrite_dependent_H [in Matrix_base]
array2D_typeequality_down_V [in Matrix_base]
B
BigIntersection_pair [in EnsembleAsType]BigUnion_pair [in EnsembleAsType]
BijectionComposition [in EnsembleFacts]
BijectionSimplify [in EnsembleFacts]
Bijective_rev [in EnsembleFacts]
bijective_eqcardinal [in EnsembleFacts]
bool_choice [in types_base]
C
CayAbel_wont4c_transcomm [in CayleyGraph]CayAbel_addrightisiso [in CayleyGraph]
CayAbel_wont4c_ft [in CayleyGraph]
CayAbel_inversioniso [in CayleyGraph]
CayAbel_wont4c_common [in CayleyGraph]
CayAbel_wont4c_edgecomm_iso [in CayleyGraph]
CayleyGraph_opp_rec [in CayleyGraph]
CayleyGraph_isoadjacencies [in CayleyGraph]
CayleyGraph_vertexsymmetric [in CayleyGraph]
CayleyGraph_isoIn [in CayleyGraph]
CayleyGraph_opp [in CayleyGraph]
CayleyGraph_addleftisiso [in CayleyGraph]
CayleyGraph_CommonNeighborhood [in CayleyGraph]
CayleyGraph_StronglyConnected [in CayleyGraph]
chaos [in Chaos]
chaos_prev_rev [in Chaos]
chaos_prev [in Chaos]
Choice [in types_base]
Choice2 [in types_base]
closed_set_half_down [in Chaos]
closed_set_half [in Chaos]
closed_set_intersection [in Chaos]
ColumnCons_HeadS_TailS [in Matrix_base]
ColumnDestructS [in Matrix_base]
ColumnHeadS_Column [in Matrix_base]
ColumnHeadS_Transpose [in Matrix_base]
ColumnHeadS_nil [in Matrix_base]
ColumnTailS_Transpose [in Matrix_base]
ColumnTailS_Column [in Matrix_base]
ColumnTailS_nil [in Matrix_base]
Column_ijth [in Matrix_base]
Column_headS [in Matrix_base]
Column_nth [in Matrix_base]
Column_eq_Transpose [in Matrix_base]
Column_tailS [in Matrix_base]
Column_cons [in Matrix_base]
Column_ijth_error [in Matrix_base]
complementary_intersection [in Chaos]
composition_injective [in types]
consapp_ass [in Array]
cons_to_app [in Chaos]
cons_untype [in Array]
cons_type [in Array]
cons_in [in ListFacts]
cons_maptype [in Array]
cons_JMeq_length [in Array]
cons_JMeq_type [in Array]
cons_hd_tail [in Array]
cons_headS_tailS [in Array]
cons_different [in ListFacts]
cons_maptype_apply [in Array]
contenido_self [in Chaos]
contenido_Intcontenido [in Chaos]
contenido_map_rangeInt [in Chaos]
contenido_map_rangeInt_rev [in Chaos]
continuity_identity [in Chaos]
count_occ_le [in ListFacts]
count_occ_app [in ListFacts]
CoupleComm [in EnsembleFacts]
D
decons [in Array]decons_tail [in Array]
decons_head [in Array]
DependentChoice [in types_base]
DependentChoice2 [in types_base]
DifferentAdd_Empty [in EnsembleFacts]
diff_comm [in Chaos]
diff_2_0 [in Chaos]
disc_destruct_up [in Chaos]
disc_destruct_down [in Chaos]
DisjointAddElim [in EnsembleFacts]
DisjointAddEquation [in EnsembleFacts]
DisjointAddEquationCommon [in EnsembleFacts]
DisjointAddEquationElim [in EnsembleFacts]
E
EAT_out_InA [in EnsembleAsType]EAT_out_in [in EnsembleAsType]
EAT_fout_simplify [in EnsembleAsType]
EAT_in_exists [in EnsembleAsType]
EAT_out_intro [in EnsembleAsType]
EAT_existence [in EnsembleAsType]
EAT_ex2 [in EnsembleAsType]
EAT_in_fout [in EnsembleAsType]
EAT_in_out [in EnsembleAsType]
EAT_fout_InA [in EnsembleAsType]
EAT_fout_in [in EnsembleAsType]
EAT_anyhypothesis [in EnsembleAsType]
ElementPartition [in EnsembleAsType]
ElementProduct_zero_l [in Vector]
ElementProduct_unit_diff [in Vector]
ElementProduct_zero_r [in Vector]
ElementProduct_unit_same [in Vector]
ElementProduct_unit_r [in Vector]
ElementProduct_unit_l [in Vector]
EnsembleAddComm [in EnsembleFacts]
EnsembleAddEmptyIsSingleton [in EnsembleFacts]
EnsembleAddIncludes [in EnsembleFacts]
EnsembleAddInto [in EnsembleFacts]
EnsembleAddToSub [in EnsembleFacts]
EnsembleApplyReductionExistence [in EnsembleFacts]
EnsembleAsTypeOut_isout [in EnsembleAsType]
EnsembleReductionExistence [in EnsembleFacts]
EnsembleReduction_unique [in EnsembleFacts]
EnsemblesSingletonEqAdd [in EnsembleFacts]
EnsemblesSingletonEqDisjAdd [in EnsembleFacts]
EnsembleSubCardinal [in EnsembleFacts]
EnsembleSubFinite [in EnsembleFacts]
eqtype_ind_self [in classicaltypes]
eqtype_to_eq [in classicaltypes]
eqtype_to_eq [in axiomtypes]
eqtype_rect_self [in classicaltypes]
EqualCouples [in EnsembleFacts]
EquivalenceFormsPartition [in EnsembleAsType]
EquivalenceFromPartition_equiv [in EnsembleAsType]
eq_closedset [in Chaos]
eq_JMeq [in JMeqmaptype]
eq_leibnitz [in types_base]
eq_injective [in types]
eq_rect_eq_nat [in Range]
eq_undo [in classicaltypes]
existsfunctions [in EnsembleFacts]
ExistsInverseOfBijective [in EnsembleFacts]
existsunique_to_function [in types_base]
exists_injective [in types]
Extensionality_Ensembles_rec [in EnsembleFacts]
F
fold_right_add_unit [in Vector]fold_right_ScalarProdVector [in Vector]
fold_right_VectorProdScalar [in Vector]
fold_right_array_from_func_back [in Vector]
fold_right_add_zero [in Vector]
fold_right_add_UnitVector [in Vector]
fold_right_app [in Vector]
fold_right_array_from_funcrange_back [in Vector]
fold_left_app [in Vector]
fold_right_shift [in Vector]
formulae_typeeq [in types]
function_typeeq [in types]
f_repeat_commS [in Chaos]
f_JMequal_dependent_Prop [in JMeqmaptype]
f_JMequal_dependent_gs [in JMeqmaptype]
f_JMequal_dependent_g [in JMeqmaptype]
f_JMequal_dependent [in JMeqmaptype]
f_repeat_plus [in Chaos]
f_JMequal [in JMeqmaptype]
f_repeat_comm [in Chaos]
f_repeat_continua [in Chaos]
f_JMequal_dependent_base [in JMeqmaptype]
f_JMequal_dependent_g_Prop [in JMeqmaptype]
f2_JMequal_s [in JMeqmaptype]
f2_JMequal [in JMeqmaptype]
f3_JMequal2 [in JMeqmaptype]
f3_JMequal3 [in JMeqmaptype]
f3_JMequal4 [in JMeqmaptype]
f3_JMequal [in JMeqmaptype]
G
glb_closed [in Chaos]Graph_isominverse [in graphs]
Graph_isocomposition [in graphs]
Group_AddMult_Shift [in Groups]
Group_additioninverse [in Groups]
Group_ShiftLeftTerm [in Groups]
Group_inversesref [in Groups]
Group_inversescommute [in Groups]
Group_is_Monoid [in Groups]
Group_indentityinverse [in Groups]
Group_identityfrominverses [in Groups]
Group_rightsimplifyinverses [in Groups]
Group_SimplifyInversion [in Groups]
Group_leftsimplifyinverses [in Groups]
Group_existsidentity [in Groups]
Group_ShiftInversion [in Groups]
Group_ElimInverseIdentity [in Groups]
Group_inversesareidentity [in Groups]
Group_ShiftRightTerm [in Groups]
Group_leftsimplify [in Groups]
Group_DoubleInversion [in Groups]
Group_InversionOfAdd [in Groups]
Group_leftadd [in Groups]
Group_AddMult_Extract [in Groups]
Group_InversionFromInverses [in Groups]
Group_inversesidentity [in Groups]
Group_InversionIsBijection [in Groups]
Group_InversionAsInverses [in Groups]
Group_refinverses [in Groups]
Group_rightadd [in Groups]
Group_ElimInversesRight [in Groups]
Group_existsInversion [in Groups]
Group_ElimInversesLeft [in Groups]
Group_uniqueinverse [in Groups]
Group_uniqueidentity [in Groups]
Group_existsinverse [in Groups]
Group_addrightisbijection [in Groups]
Group_addleftisbijection [in Groups]
Group_AddMult_Step [in Groups]
Group_rightsimplify [in Groups]
H
headS_ColumnTailS [in Matrix_base]headS_Transpose [in Matrix_base]
headS_hd [in Array]
headS_ColumnHeadS [in Matrix_base]
head_hd [in Array]
head_and_body [in Array]
HorizontalAppend_nil2D [in Matrix_base]
HorizontalAppend_commuteC [in Matrix_base]
HorizontalAppend_ColumnTailS_C [in Matrix_base]
HorizontalAppend_ColumnHeadS [in Matrix_base]
HorizontalAppend_ijth_right [in Matrix_base]
HorizontalAppend_commute_tailS [in Matrix_base]
HorizontalAppend_nil_l [in Matrix_base]
HorizontalAppend_nthC_left [in Matrix_base]
HorizontalAppend_associative [in Matrix_base]
HorizontalAppend_ColumnTailS [in Matrix_base]
HorizontalAppend_ColumnHeadS_C [in Matrix_base]
HorizontalAppend_commute [in Matrix_base]
HorizontalAppend_commute_headS [in Matrix_base]
HorizontalAppend_nil_r [in Matrix_base]
HorizontalAppend_type [in Matrix_base]
HorizontalAppend_nthC_right [in Matrix_base]
HorizontalAppend_ijth_left [in Matrix_base]
HorizontalAppend_associativeC [in Matrix_base]
I
IdentityMatrix_Transpose [in Matrix_base]IdentityMatrix_ijth_range [in Matrix_base]
IdentityMatrix_ijth [in Matrix_base]
IdentityMatrix_Symmetric [in Matrix_base]
id_injective [in types]
ijth_error_nth_error_D [in Matrix_base]
ijth_nth_d [in Matrix_base]
ijth_range_eq [in Matrix_base]
ijth_error_tailS [in Matrix_base]
ijth_error_headS [in Matrix_base]
ijth_range_error_eq [in Matrix_base]
ijth_out [in Matrix_base]
ijth_headS [in Matrix_base]
ijth_nth [in Matrix_base]
ijth_equality [in Matrix_base]
ijth_error_nth_error_d [in Matrix_base]
ijth_tailS [in Matrix_base]
ijth_range_equality [in Matrix_base]
ijth_error_eq [in Matrix_base]
Intcontenido_contenido [in Chaos]
Intcontenido_self [in Chaos]
InverseOfBijectiveIsBijective [in EnsembleFacts]
In_CayleyGraph_recgroup [in CayleyGraph]
In_CayleyGraph_rec [in CayleyGraph]
In_nth [in ListFacts]
Isomorphism_In_rec [in graphs]
Isomorphism_In [in graphs]
isom_commonneighbor [in graphs]
isom_outdegree [in graphs]
isom_neighbor [in graphs]
IVT_any [in Chaos]
IVT_any_rev [in Chaos]
J
JMeq_maptype_eq [in JMeqmaptype]JMeq_dependent_g [in JMeqmaptype]
JMeq_maptype [in JMeqmaptype]
JMeq_typeeq [in JMeqmaptype]
JMex [in JMeqmaptype]
JMfunctional_extensionality [in JMeqmaptype]
JMfunctional2_extensionality [in JMeqmaptype]
JMfunctional3_extensionality_dep [in JMeqmaptype]
JMfunctional3_extensionality [in JMeqmaptype]
K
Kronecker_delta_diff [in Vector]Kronecker_delta_refl [in Vector]
Kronecker_delta_sym [in Vector]
K_nat [in Range]
L
lcompleteness [in Chaos]lema0 [in Chaos]
lema1 [in Chaos]
lema2 [in Chaos]
lema2a [in Chaos]
lema2eq [in Chaos]
le_lowrange_in [in Range]
le_uniqueness_proof [in Range]
listpairscycle_last [in ListFacts]
listpairscycle_fst [in ListFacts]
listpairscycle_consecutive [in ListFacts]
listpairscycle_length [in ListFacts]
listpairscycle_Inexbef [in ListFacts]
listpairscycle_head [in ListFacts]
listpairscycle_nth [in ListFacts]
listpairscycle_doublesame [in ListFacts]
listpairscycle_break [in ListFacts]
listpairscycle_double [in ListFacts]
listpairs_length [in ListFacts]
listpairs_nth [in ListFacts]
listpairs_double [in ListFacts]
listpairs_Inexbef [in ListFacts]
listpairs_cons [in ListFacts]
listpairs_app [in ListFacts]
list_eq_nth_to_ntherror [in ListFacts]
list_ntherror_inR [in ListFacts]
list_last_cons2 [in ListFacts]
list_last_Incons [in ListFacts]
list_lastelim [in graphs]
list_last_In [in ListFacts]
list_ntherror_nth [in ListFacts]
list_lastpushback [in graphs]
list_inpushbackrev [in graphs]
list_ntherror_out [in ListFacts]
list_hderror_ntherror [in ListFacts]
list_zerolength [in graphs]
list_pushbacknotnil [in graphs]
list_last_cons [in ListFacts]
list_inpushbacknew [in graphs]
list_last_nth [in ListFacts]
list_nth_out [in ListFacts]
list_lengthpushback [in graphs]
list_hdpushbackrev [in graphs]
list_inpushback [in graphs]
list_nonzerolengthback [in graphs]
list_nonzerolength [in graphs]
list_eq_ntherror_to_nth [in ListFacts]
list_ntherror_outR [in ListFacts]
list_foldleft_pushback [in graphs]
list_hdpushback [in graphs]
list_hdchangebase [in graphs]
list_last_other [in ListFacts]
list_last_app [in ListFacts]
list_ntherror_inL [in ListFacts]
list_hd_nth [in ListFacts]
lowrange_prevfunc_injective [in Range]
lowrange_injective_P_func_aux2 [in Range]
lowrange_injective_S [in Range]
lowrange_eq [in Range]
lowrange_injective_S_func_aux [in Range]
lowrange_injective_n0 [in Range]
lowrange_0_unique [in Range]
lowrange_exist_eq [in Range]
lowrange_injective_le [in Range]
lowrange_injective_n [in Range]
lowrange_S_pair [in Range]
lowrange_identity_injective [in Range]
lowrange_lowrangtS_identity_injective [in Range]
lowrange_injective_P_func_aux [in Range]
lowrange_discr [in Range]
lowrange_identity_le [in Range]
lowrangtS_lowrange_identity_injective [in Range]
lowrangt_0_nonihabited [in Range]
lowrangt_exist_eq [in Range]
lowrangt_S_ihabited [in Range]
lowrangt_lowrange_identity_injective [in Range]
lowrangt_injective_0 [in Range]
lowrangt_injective_n [in Range]
lowrangt_injective_Sn [in Range]
lowrangt_discr [in Range]
lt_uniqueness_proof [in Range]
lub_closed [in Chaos]
M
maprepeat_idInterval [in Chaos]maptype_compose [in JMeqmaptype]
maptype_application_t [in JMeqmaptype]
maptype_selfany [in axiomtypes]
maptype_rect [in axiomtypes]
maptype_combine_l [in JMeqmaptype]
maptype_ind_t [in axiomtypes]
maptype_square [in JMeqmaptype]
maptype_dependent [in JMeqmaptype]
maptype_square2 [in JMeqmaptype]
maptype_fun [in JMeqmaptype]
maptype_selfany [in classicaltypes]
maptype_mapproduct [in axiomtypes]
maptype_dependent_g [in axiomtypes]
maptype_sym [in axiomtypes]
maptype_trans [in JMeqmaptype]
maptype_mapproduct [in JMeqmaptype]
maptype_rect_r [in axiomtypes]
maptype_rectX [in axiomtypes]
maptype_returnpi [in JMeqmaptype]
maptype_constant [in axiomtypes]
maptype_combine_r [in JMeqmaptype]
maptype_pi [in classicaltypes]
maptype_dependent_g [in JMeqmaptype]
maptype_identity [in axiomtypes]
maptype_binary [in JMeqmaptype]
maptype_rect_tr [in axiomtypes]
maptype_square [in axiomtypes]
maptype_undo [in JMeqmaptype]
maptype_fun_t [in JMeqmaptype]
maptype_returnpi [in axiomtypes]
maptype_ind [in axiomtypes]
maptype_JMeq_g [in JMeqmaptype]
maptype_JMeq [in JMeqmaptype]
maptype_undo [in axiomtypes]
maptype_selfany [in JMeqmaptype]
maptype_rect_t [in axiomtypes]
maptype_proof_irrelevance [in JMeqmaptype]
maptype_preserveidentity [in JMeqmaptype]
maptype_identity [in JMeqmaptype]
maptype_proof_irrelevance [in axiomtypes]
maptype_fun [in axiomtypes]
maptype_sym [in JMeqmaptype]
maptype_application [in JMeqmaptype]
maptype_fun_t [in axiomtypes]
maptype_dependent [in axiomtypes]
map_repeat_to_f_repeat [in Chaos]
map_idInterval [in Chaos]
map_repeat_comm [in Chaos]
map_repeat_cons [in Chaos]
match_boolunique [in types]
MatrixAdd_ijth [in Matrix_arith]
MatrixAdd_nil [in Matrix_arith]
MatrixAdd_associativity [in Matrix_arith]
MatrixAdd_single [in Matrix_arith]
MatrixAdd_d_nil [in Matrix_arith]
MatrixAdd_d_single [in Matrix_arith]
MatrixAdd_commutativity [in Matrix_arith]
MatrixProduct_Zero_l [in Matrix_arith]
MatrixProduct_summatory [in Matrix_arith]
MatrixProduct_Zero_r [in Matrix_arith]
MatrixProduct_associativity [in Matrix_arith]
MatrixSymmetric_ijth [in Matrix_base]
MatrixSymmetric_ijth_range [in Matrix_base]
matrix_from_funcrange_extensionalityR [in Matrix_base]
matrix_from_func_ijth [in Matrix_base]
matrix_from_funcrange_ijth_range [in Matrix_base]
Matrix_col_summatory [in Matrix_arith]
matrix_from_func_ijth_error [in Matrix_base]
Matrix_row_summatory [in Matrix_arith]
matrix_from_func_extensionality [in Matrix_base]
minperiod_f [in Chaos]
minperiod0 [in Chaos]
Monoid_uniqueinverse [in Groups]
N
nat_destruct [in types]NonEmptyAsAdd [in EnsembleFacts]
nthC_out [in Matrix_base]
nthC_error_out [in Matrix_base]
nthC_range_ColumnHeadS [in Matrix_base]
nthC_range_matrix_from_funcrange [in Matrix_base]
nthC_error_ColumnHeadS [in Matrix_base]
nthC_range_eq [in Matrix_base]
nthC_nth [in Matrix_base]
nthC_headS [in Matrix_base]
nthC_error_eq [in Matrix_base]
nthC_error_ColumnTailS [in Matrix_base]
nthC_anydefault [in Matrix_base]
nthC_range_ColumnTailS [in Matrix_base]
nthC_range_nth_range [in Matrix_base]
nthC_ColumnTailS [in Matrix_base]
nthC_nth_R [in Matrix_base]
nthC_matrix_from_func [in Matrix_base]
nthC_ColumnHeadS [in Matrix_base]
nthC_tailS [in Matrix_base]
nth_range_summatoryv [in Matrix_arith]
nth_out [in Array]
nth_error_tailS [in Array]
nth_error_headS [in Array]
nth_range_matrix_from_funcrange [in Matrix_base]
nth_range_tailS [in Array]
nth_ColumnTailS [in Matrix_base]
nth_range_equality [in Array]
nth_range_headS [in Array]
nth_tailS [in Array]
nth_error_eq [in Array]
nth_range_eq [in Array]
nth_ColumnHeadS [in Matrix_base]
nth_error_out [in Array]
nth_range_JMequality [in Array]
nth_equality [in Array]
nth_error_equality [in Array]
nth_headS [in Array]
nth_anydefault [in Array]
P
PartitionExlusive [in EnsembleAsType]PartitionFromEquivalence_out [in EnsembleAsType]
PartitionFromEquivalence_intro [in EnsembleAsType]
PathExtractBack [in graphs]
Path_nonemptyback [in graphs]
period_f_rev [in Chaos]
period_f [in Chaos]
posreal_destruct [in Chaos]
preimage_closed [in Chaos]
preimage_complementary [in Chaos]
Product_unit_l [in Matrix_arith]
Product_nil_l [in Matrix_arith]
Product_unit_r [in Matrix_arith]
Product_nil_r [in Matrix_arith]
Product_nil_c [in Matrix_arith]
R
rangeInt_b [in Chaos]rangeInt_a [in Chaos]
real_le_signchange_r [in Chaos]
real_le_signchange_l [in Chaos]
real_glb_eq2 [in Chaos]
real_glb_eq [in Chaos]
real_lub_eq2 [in Chaos]
real_lub_eq [in Chaos]
real_middlepoint [in Chaos]
RelatedByEquivalence [in EnsembleAsType]
removelast_different [in ListFacts]
removelast_length [in ListFacts]
removelast_lengthle [in ListFacts]
rotatelistn_ntherror [in ListFacts]
rotatelistn_InL [in ListFacts]
rotatelistn_cons [in ListFacts]
rotatelistn_plus [in ListFacts]
rotatelistn_nil [in ListFacts]
rotatelistn_InR [in ListFacts]
rotatelistn_periodic [in ListFacts]
rotatelistn_length [in ListFacts]
rotatelistn_count [in ListFacts]
rotatelistn_listpairscycle [in ListFacts]
rotatelistn_app [in ListFacts]
rotatelistn_rotatelist [in ListFacts]
rotatelistn_nilinv [in ListFacts]
rotatelistn_hderror [in ListFacts]
rotatelistn_single [in ListFacts]
rotatelistn_comm [in ListFacts]
rotatelist_InL [in ListFacts]
rotatelist_listpairscycle [in ListFacts]
rotatelist_nilinv [in ListFacts]
rotatelist_hderror [in ListFacts]
rotatelist_ntherrorS [in ListFacts]
rotatelist_cons [in ListFacts]
rotatelist_InR [in ListFacts]
rotatelist_topair [in ListFacts]
rotatelist_ntherror [in ListFacts]
rotatelist_to [in ListFacts]
rotatelist_count [in ListFacts]
rotatelist_length [in ListFacts]
S
SameCouple [in EnsembleFacts]ScalarProduct_unit_diff [in Vector]
ScalarProduct_cons [in Vector]
ScalarProduct_unit_l [in Vector]
ScalarProduct_app [in Vector]
ScalarProduct_zero_l [in Vector]
ScalarProduct_unit_r [in Vector]
ScalarProduct_ScalarProdVector_l [in Vector]
ScalarProduct_zero_r [in Vector]
ScalarProduct_summatory_r [in Matrix_arith]
ScalarProduct_single [in Vector]
ScalarProduct_as_fold [in Vector]
ScalarProduct_comm [in Matrix_arith]
ScalarProduct_VectorProdScalar_r [in Vector]
ScalarProduct_as_summatory [in Vector]
ScalarProduct_summatory_l [in Matrix_arith]
ScalarProduct_nil [in Vector]
ScalarProduct_commutative [in Vector]
ScalarProduct_unit_same [in Vector]
ScalarProdVector_nth_range [in Vector]
selfincluded [in EnsembleFacts]
Singleton_compact [in Chaos]
single_notnil [in Array]
SubPath [in graphs]
SubPathBack [in graphs]
summatoryS [in Vector]
summatory_add [in Vector]
summatory_swap [in Vector]
summatory_Kronecker_delta [in Vector]
summatory_Kronecker_delta_out [in Vector]
summatory_fR_Kronecker_delta [in Vector]
summatory_prod_l [in Vector]
summatory_prod_r [in Vector]
summatory_extensionality [in Vector]
summatory0 [in Vector]
sym_eqtype [in axiomtypes]
T
tailsequal [in Array]tailS_tail [in Array]
tailS_ColumnHeadS [in Matrix_base]
tailS_ColumnTailS [in Matrix_base]
tailS_Transpose [in Matrix_base]
tailS0_nil [in Array]
tail1_nil [in Array]
transform [in axiomtypes]
TransposeProduct [in Matrix_arith]
TransposeTranspose [in Matrix_base]
TransposeZeroMatrix [in Matrix_arith]
Transpose_ijth_range [in Matrix_base]
Transpose_ijth [in Matrix_base]
Transpose_nth_range [in Matrix_base]
Transpose_nth [in Matrix_base]
Transpose_nthC [in Matrix_base]
Transpose_nil [in Matrix_base]
Transpose_nthC_range [in Matrix_base]
trans_eqtype [in axiomtypes]
typerewrite_simple [in axiomtypes]
typerewrite_Prop [in axiomtypes]
U
undirected_neighbor_sym [in graphs]UndoInverse [in EnsembleFacts]
UndoInverseBijective [in EnsembleFacts]
UndoInverseSym [in EnsembleFacts]
uniqueidentity [in Groups]
UniquePartition [in EnsembleAsType]
unique_appending [in Array]
UnitVector_as_app_construct [in Vector]
UnitVector_as_app [in Vector]
V
VectorAdd_commutativity [in Vector]VectorAdd_d_eq [in Vector]
VectorAdd_nth_range [in Vector]
VectorAdd_zerovector_l [in Vector]
VectorAdd_R_single [in Vector]
VectorAdd_R_nil [in Vector]
VectorAdd_R_eq [in Vector]
VectorAdd_associativity [in Vector]
VectorAdd_d_commutativity [in Vector]
VectorAdd_d_nil [in Vector]
VectorAdd_app [in Vector]
VectorAdd_single [in Vector]
VectorAdd_zerovector_r [in Vector]
VectorAdd_d_app [in Vector]
VectorAdd_d_associativity [in Vector]
VectorAdd_Rd_eq [in Vector]
VectorAdd_d_single [in Vector]
VectorAdd_nth [in Vector]
VectorAdd_nil [in Vector]
VectorProdScalar_nth_range [in Vector]
vertexsymmetric_outregular [in graphs]
VerticalAppend_commute [in Matrix_base]
VerticalAppend_commute_ColumnHeadS_C [in Matrix_base]
VerticalAppend_Column [in Matrix_base]
VerticalAppend_commute_ColumnTailS [in Matrix_base]
VerticalAppend_commuteR [in Matrix_base]
VerticalAppend_commute_ColumnHeadS [in Matrix_base]
Z
ZeroMatrix_ijth [in Matrix_base]ZeroMatrix_Transpose [in Matrix_base]
ZeroMatrix_Symmetric [in Matrix_base]
ZeroMatrix_ijth_range [in Matrix_base]
Zmodeg_parity [in Zmod]
Zmodeg_equiv7_1_8 [in Zmod]
Zmodeg_add10_1_8 [in Zmod]
Zmod_nat_repsetnat [in Zmod]
Zmod_opp [in Zmod]
Zmod_canonical [in Zmod]
Zmod_haspos [in Zmod]
Zmod_addisbijection [in Zmod]
Zmod_addition [in Zmod]
Z_ge_mulpos [in Zfacts]
Z_absnat_posgt0 [in Zfacts]
Z_getpositive [in Zfacts]
Z_absnat_0 [in Zfacts]
Z_absnat_posge0 [in Zfacts]
Z_gt_mulpos [in Zfacts]
Z_ge_multwopos [in Zfacts]
Z_gt_divpos [in Zfacts]
Z_eucdiff [in Zfacts]
_
_Matrix_arith_summatory_swap [in Matrix_arith]Section Index
A
Arith [in Matrix_arith]Arith [in Vector]
Arrays [in Array]
arrays_lists [in Array]
C
CayleyGraphs [in CayleyGraph]Chaos [in Chaos]
Chaos_begin [in Chaos]
ChoiceT_lemmas [in types_base]
Cutting [in Array]
D
DependentChoice_lemmas [in types_base]E
EnsembleAsType [in EnsembleAsType]EnsembleFacts [in EnsembleFacts]
Examples [in JMeqmaptype]
F
Fold_Right_Recursor [in Vector]Fold_Left_Recursor [in Vector]
G
graphs [in graphs]Groups [in Groups]
L
Lema2 [in Chaos]R
RealLemmas [in Chaos]RealLemmas' [in Chaos]
V
Vector [in Vector]Z
Zfacts [in Zfacts]Zmod [in Zmod]
Notation Index
A
_ + _ [in Vector]_ * _ [in Matrix_arith]
_ :* _ [in Matrix_arith]
_ :+ _ [in Matrix_arith]
_ + _ [in Matrix_arith]
_ \u00b7 _ [in Vector]
_ ^T [in Matrix_arith]
_ * _ [in Matrix_arith]
_ * _ [in Vector]
_ + _ [in Matrix_arith]
E
_ ++ _ [in JMeqmaptype]other
_ ++ _ (array_scope) [in Array]_ :: _ (array_scope) [in Array]
_ +V+ _ (matrix_scope) [in Matrix_base]
_ +H+ _ (matrix_scope) [in Matrix_base]
_ o _ (type_scope) [in types_base]
_ == _ :> _ _ [in JMeqmaptype]
_ == _ [in JMeqmaptype]
Constructor Index
A
appending_intro [in Array]appending_nil [in Array]
B
BigIntersection_intro [in EnsembleAsType]BigUnion_intro [in EnsembleAsType]
C
cons [in Array]E
EnsembleApplyReduction_empty [in EnsembleFacts]EnsembleApplyReduction_add [in EnsembleFacts]
EnsembleAsTypeIntro [in EnsembleAsType]
EnsembleReduction_add [in EnsembleFacts]
EnsembleReduction_empty [in EnsembleFacts]
EquivalenceFromPartition_intro [in EnsembleAsType]
I
In_CayleyGraph [in CayleyGraph]In_apply_func [in EnsembleFacts]
In_Neighborhood [in graphs]
M
mkInt [in Chaos]N
nat_firsts_def [in Zfacts]neighbor_cardinal [in graphs]
nil [in Array]
P
Path_nonempty [in graphs]Path_empty [in graphs]
Path_single [in graphs]
R
RelatedElements_intro [in EnsembleAsType]Inductive Index
A
appending [in Array]apply_func [in EnsembleFacts]
array [in Array]
B
BigIntersection [in EnsembleAsType]BigUnion [in EnsembleAsType]
C
CayleyGraph [in CayleyGraph]E
EnsembleApplyReduction [in EnsembleFacts]EnsembleAsType [in EnsembleAsType]
EnsembleReduction [in EnsembleFacts]
EquivalenceFromPartition [in EnsembleAsType]
N
nat_firsts [in Zfacts]Neighborhood [in graphs]
O
outdegree [in graphs]P
Path [in graphs]R
RelatedElements [in EnsembleAsType]Definition Index
A
AbelianGroup [in Groups]app [in Array]
appaux [in Array]
arrayapp [in Array]
arraycons [in Array]
arraynil [in Array]
array_from_func_aux [in Array]
array_homogeneous [in Array]
array_from_func [in Array]
array_as_list [in Array]
array_from_funcrange_aux_head2 [in Array]
array_from_funcrange_aux_head [in Array]
array_from_funcrange [in Array]
array_app_nil_l [in Array]
array2D [in Matrix_base]
Associativity [in EnsembleFacts]
B
Bijective [in EnsembleFacts]C
CayAbel_without_nontrivial4cycles [in CayleyGraph]CommonNeighborhood [in graphs]
Commutativity [in EnsembleFacts]
compose [in types_base]
Compose [in EnsembleFacts]
cons2D [in Matrix_base]
contenido [in Chaos]
D
dtype [in graphs]E
EAT [in EnsembleAsType]EAT_ex1set [in EnsembleAsType]
EAT_ex1 [in EnsembleAsType]
EAT_in [in EnsembleAsType]
EAT_out [in EnsembleAsType]
EAT_fout [in EnsembleAsType]
ej1 [in Vector]
ej2 [in Vector]
ej3 [in Vector]
EnsembleAsTypeOut [in EnsembleAsType]
F
fold_left [in Vector]fold_right [in Vector]
f_repeat [in Chaos]
G
Graph [in graphs]Group [in Groups]
Group_Inversion [in Groups]
Group_AddMult [in Groups]
H
HasIdentity [in Groups]HasInverses [in Groups]
hd [in Array]
head [in Array]
headS [in Array]
I
Identity [in Groups]IdentityMatrix [in Matrix_base]
idInterval [in Chaos]
ijth [in Matrix_base]
ijth_error [in Matrix_base]
ijth_range [in Matrix_base]
injective [in types]
inrange [in Chaos]
Intcontenido [in Chaos]
Inverse [in Groups]
InverseFunction [in EnsembleFacts]
Isomorph [in graphs]
Isomorphism [in graphs]
is_lower_bound [in Chaos]
is_glb [in Chaos]
K
Kronecker_delta [in Vector]L
lbound [in Chaos]LeftIdentity [in Groups]
LeftInverse [in Groups]
length [in Array]
le_lowrange [in Range]
listcons [in Array]
listnil [in Array]
listpairs [in ListFacts]
listpairscycle [in ListFacts]
list_pushback [in graphs]
lowrange [in Range]
lowrange_prevfunc [in Range]
lowrange_identity [in Range]
lowrange_injective_P_func [in Range]
lowrange_lowrangtS_identity [in Range]
lowrange_injective_le_fun [in Range]
lowrange_injective_S_func [in Range]
lowrange_injective_P [in Range]
lowrangt [in Range]
lowrangtS_lowrange_identity [in Range]
lowrangt_lowrange_identity [in Range]
lowrangt_prevfunc [in Range]
lowrangt_identity [in Range]
M
makevar_tactic [in types_base]map [in Chaos]
maptype [in JMeqmaptype]
maptype_pi [in JMeqmaptype]
map_repeat [in Chaos]
MatrixAdd [in Matrix_arith]
MatrixAdd_d [in Matrix_arith]
MatrixProduct [in Matrix_arith]
MatrixSymmetric [in Matrix_base]
matrix_from_funcrange [in Matrix_base]
matrix_from_func [in Matrix_base]
minperiod [in Chaos]
Monoid [in Groups]
N
natfunc_lowrange_Prop [in Range]natfunc_lowrange [in Range]
natfunc_lowrangt [in Range]
nilC [in Matrix_base]
nil2D [in Matrix_base]
nth [in Array]
nthC [in Matrix_base]
nthC_range [in Matrix_base]
nthC_type [in Matrix_base]
nthC_error [in Matrix_base]
nth_error [in Array]
nth_range [in Array]
O
Operation [in EnsembleFacts]outregular [in graphs]
P
Partition [in EnsembleAsType]PartitionFromEquivalence [in EnsembleAsType]
period [in Chaos]
Preimage [in Chaos]
R
range [in Range]rangeInt [in Chaos]
rangt [in Range]
RightIdentity [in Groups]
RightInverse [in Groups]
rotatelist [in ListFacts]
rotatelistn [in ListFacts]
S
ScalarProdVector [in Vector]StronglyConnected [in graphs]
T
tail [in Array]tailS [in Array]
Transpose_type [in Matrix_base]
Transpose_Ctype [in Matrix_base]
U
Undirected [in graphs]UnitVector [in Vector]
V
VectorAdd_R [in Vector]VectorAdd_d [in Vector]
VectorProdScalar [in Vector]
vertexsymmetric [in graphs]
VerticalAppend [in Matrix_base]
Z
ZeroMatrix [in Matrix_base]Zmodequiv [in Zmod]
Zmod_repset [in Zmod]
Zmod_repsetnat [in Zmod]
Axiom Index
A
array_typeequality_down [in Array]array2D_typeequality_down_H [in Matrix_base]
M
maptype_application [in axiomtypes]maptype_trans [in axiomtypes]
maptype_application_t [in axiomtypes]
Z
Zmod [in Zmod]Zmodequivalence_right [in Zmod]
Zmodequivalence_left [in Zmod]
ZmodN [in Zmod]
Zmod_elim [in Zmod]
Zmod_add [in Zmod]
Zmod_add_Z [in Zmod]
Variable Index
A
Arith.add [in Vector]Arith.add [in Matrix_arith]
Arith.add_ass [in Vector]
Arith.add_comm [in Matrix_arith]
Arith.add_ass [in Matrix_arith]
Arith.add_comm [in Vector]
Arith.distributive_left [in Vector]
Arith.distributive_left [in Matrix_arith]
Arith.distributive_right [in Matrix_arith]
Arith.distributive_right [in Vector]
Arith.dotproduct [in Vector]
Arith.one [in Vector]
Arith.one [in Matrix_arith]
Arith.oneL [in Vector]
Arith.oneL [in Matrix_arith]
Arith.oneR [in Matrix_arith]
Arith.oneR [in Vector]
Arith.prod [in Vector]
Arith.prod [in Matrix_arith]
Arith.prod_ass [in Matrix_arith]
Arith.prod_comm [in Matrix_arith]
Arith.prod_zero_r [in Vector]
Arith.prod_zero_l [in Matrix_arith]
Arith.prod_zero_r [in Matrix_arith]
Arith.prod_comm [in Vector]
Arith.prod_ass [in Vector]
Arith.prod_zero_l [in Vector]
Arith.summatory [in Matrix_arith]
Arith.summatory [in Vector]
Arith.summatoryv [in Matrix_arith]
Arith.U [in Matrix_arith]
Arith.U [in Vector]
Arith.unitcol [in Matrix_arith]
Arith.unitrow [in Matrix_arith]
Arith.unitvector [in Vector]
Arith.unitvector [in Matrix_arith]
Arith.zero [in Matrix_arith]
Arith.zero [in Vector]
Arith.zeroL [in Matrix_arith]
Arith.zeroL [in Vector]
Arith.zeroR [in Vector]
Arith.zeroR [in Matrix_arith]
Arith.zerovector [in Matrix_arith]
Arith.zerovector [in Vector]
C
Chaos_begin.suprayectiva [in Chaos]Chaos_begin.f [in Chaos]
Chaos_begin.continua [in Chaos]
Chaos_begin.f_01_01 [in Chaos]
Chaos.continua [in Chaos]
Chaos.f [in Chaos]
Chaos.f_01_01 [in Chaos]
Chaos.suprayectiva [in Chaos]
ChoiceT_lemmas.bool_choice_aux2 [in types_base]
ChoiceT_lemmas.R1 [in types_base]
ChoiceT_lemmas.Choice2_aux [in types_base]
ChoiceT_lemmas.R [in types_base]
ChoiceT_lemmas.bool_choice_aux [in types_base]
ChoiceT_lemmas.Choice_aux [in types_base]
ChoiceT_lemmas.T [in types_base]
ChoiceT_lemmas.Choice_aux2 [in types_base]
ChoiceT_lemmas.T' [in types_base]
ChoiceT_lemmas.Choice2_aux2 [in types_base]
ChoiceT_lemmas.R' [in types_base]
ChoiceT_lemmas.R2 [in types_base]
Cutting.A [in Array]
D
DependentChoice_lemmas.DependentChoice_aux2 [in types_base]DependentChoice_lemmas.DependentChoice2_aux [in types_base]
DependentChoice_lemmas.T [in types_base]
DependentChoice_lemmas.R [in types_base]
DependentChoice_lemmas.g [in types_base]
DependentChoice_lemmas.DependentChoice2_aux2 [in types_base]
DependentChoice_lemmas.R' [in types_base]
DependentChoice_lemmas.DependentChoice_aux [in types_base]
E
Examples.app [in JMeqmaptype]Examples.ej1 [in JMeqmaptype]
Examples.Emn [in JMeqmaptype]
Examples.Exy [in JMeqmaptype]
Examples.m [in JMeqmaptype]
Examples.n [in JMeqmaptype]
Examples.p [in JMeqmaptype]
Examples.q [in JMeqmaptype]
Examples.t [in JMeqmaptype]
Examples.u [in JMeqmaptype]
Examples.v [in JMeqmaptype]
Examples.x [in JMeqmaptype]
Examples.y [in JMeqmaptype]
F
Fold_Left_Recursor.B [in Vector]Fold_Right_Recursor.B [in Vector]
Fold_Left_Recursor.f [in Vector]
Fold_Right_Recursor.f [in Vector]
Fold_Left_Recursor.A [in Vector]
Fold_Right_Recursor.A [in Vector]
G
Groups.f [in Groups]Groups.U [in Groups]
L
Lema2.continua [in Chaos]Lema2.f [in Chaos]
R
RealLemmas'.continua [in Chaos]RealLemmas'.f [in Chaos]
RealLemmas'.f_01_01 [in Chaos]
RealLemmas'.suprayectiva [in Chaos]
RealLemmas.continua [in Chaos]
RealLemmas.f [in Chaos]
RealLemmas.f_01_01 [in Chaos]
RealLemmas.suprayectiva [in Chaos]
V
Vector.U [in Vector]Library Index
A
anomalybugArray
Array_old_eqtype
axiomtypes
C
CayleyGraphChaos
circulant
classicaltypes
E
EnsembleAsTypeEnsembleFacts
F
Function_bugG
Geometrygodel
graphs
Groups
H
hurryI
illtypebugJ
JMeqmaptypeL
ListFactsM
maptypeconstructmaptype_standard
Matrix
Matrix_arith
Matrix_base
N
NetworkP
positivereducedQ
QuotientGroupR
RangeRings
T
Turingtutorial
types
typesdecission
types_base
U
usingensemblesV
VectorZ
ZfactsZmod
| 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 | (1091 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 | (3 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 | (1 entry) |
| 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 | (713 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 | (23 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 | (18 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 | (22 entries) |
| Inductive 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 | (15 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 | (141 entries) |
| Axiom 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) |
| 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 | (105 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 | (38 entries) |
This page has been generated by coqdoc