C
C [definition, in C]
cancel_app [lemma, in cancel_app]
canon [projection, in canon]
canonical_Rsqr [lemma, in canonical_Rsqr]
cardinal [inductive, in cardinal]
cardinalO_empty [lemma, in cardinalO_empty]
cardinal_finite [lemma, in cardinal_finite]
cardinal_unicity [lemma, in cardinal_unicity]
cardinal_is_functional [lemma, in cardinal_is_functional]
cardinal_elim [lemma, in cardinal_elim]
cardinal_decreases [lemma, in cardinal_decreases]
cardinal_Im_intro [lemma, in cardinal_Im_intro]
cardinal_invert [lemma, in cardinal_invert]
cardinal_Empty [lemma, in cardinal_Empty]
card_soustr_1 [lemma, in card_soustr_1]
card_empty [constructor, in card_empty]
card_Add_gen [lemma, in card_Add_gen]
card_add [constructor, in card_add]
Carrier [definition, in Carrier]
Carrier_of [projection, in Carrier_of]
carry [inductive, in carry]
Carry [section, in Carry]
Carry.A [variable, in A]
caseS [definition, in caseS]
caseS [definition, in caseS]
case0 [definition, in case0]
case0 [definition, in case0]
castm [definition, in castm]
Cauchy_crit [definition, in Cauchy_crit]
Cauchy_crit_series [definition, in Cauchy_crit_series]
cauchy_abs [lemma, in cauchy_abs]
cauchy_opp [lemma, in cauchy_opp]
cauchy_maj [lemma, in cauchy_maj]
cauchy_crit_geometric_dec_fun [lemma, in cauchy_crit_geometric_dec_fun]
cauchy_bound [lemma, in cauchy_bound]
cauchy_min [lemma, in cauchy_min]
cauchy_finite [lemma, in cauchy_finite]
Cauchy_prod [library]
Cesaro [lemma, in Cesaro]
Cesaro_1 [lemma, in Cesaro_1]
Chain [record, in Chain]
Chain_cond [projection, in Chain_cond]
Charac [constructor, in Charac]
charac [definition, in charac]
Characterisation_wf_relations.leA [variable, in leA]
Characterisation_wf_relations.A [variable, in A]
Characterisation_wf_relations [section, in Characterisation_wf_relations]
Choice [lemma, in Choice]
choice [lemma, in choice]
choice [lemma, in choice]
ChoiceFacts [library]
ChoiceSchemes [section, in ChoiceSchemes]
ChoiceSchemes.A [variable, in A]
ChoiceSchemes.B [variable, in B]
ChoiceSchemes.P [variable, in P]
ChoiceSchemes.R [variable, in R]
Choice_lemmas.S [variable, in S]
Choice_lemmas.S' [variable, in S']
Choice_lemmas [section, in Choice_lemmas]
Choice_lemmas.R [variable, in R]
Choice_lemmas.R1 [variable, in R1]
Choice_lemmas.R' [variable, in R']
Choice_lemmas.R2 [variable, in R2]
Choice2 [lemma, in Choice2]
classic [axiom, in classic]
Classical [library]
ClassicalChoice [library]
ClassicalDescription [library]
ClassicalEpsilon [library]
ClassicalFacts [library]
ClassicalUniqueChoice [library]
classical_denumerable_description_imp_fun_choice [lemma, in classical_denumerable_description_imp_fun_choice]
classical_proof_irrelevence [lemma, in classical_proof_irrelevence]
classical_definite_description [lemma, in classical_definite_description]
classical_indefinite_description [lemma, in classical_indefinite_description]
Classical_Pred_Set [library]
Classical_Prop [library]
Classical_Type [library]
Classical_Pred_Type [library]
Classical_sets [library]
classic_set [abbreviation, in classic_set]
classic_set_in_prop_context [lemma, in classic_set_in_prop_context]
closed_set [definition, in closed_set]
closed_set_P1 [lemma, in closed_set_P1]
clos_trans_t1n [lemma, in clos_trans_t1n]
clos_refl_trans_n1 [inductive, in clos_refl_trans_n1]
clos_rt1n_rt [lemma, in clos_rt1n_rt]
clos_refl_trans_1n [inductive, in clos_refl_trans_1n]
clos_rt_is_preorder [lemma, in clos_rt_is_preorder]
clos_refl_sym_trans_n1 [inductive, in clos_refl_sym_trans_n1]
clos_refl_sym_trans_1n [inductive, in clos_refl_sym_trans_1n]
clos_rt_idempotent [lemma, in clos_rt_idempotent]
clos_trans_t1n_iff [lemma, in clos_trans_t1n_iff]
clos_trans_tn1 [lemma, in clos_trans_tn1]
clos_trans_1n [inductive, in clos_trans_1n]
clos_refl_trans_ind_right [lemma, in clos_refl_trans_ind_right]
clos_rstn1_sym [lemma, in clos_rstn1_sym]
clos_refl_trans_ind_left [lemma, in clos_refl_trans_ind_left]
clos_refl_sym_trans [inductive, in clos_refl_sym_trans]
clos_t1n_trans [lemma, in clos_t1n_trans]
clos_rst1n_sym [lemma, in clos_rst1n_sym]
clos_tn1_trans [lemma, in clos_tn1_trans]
clos_rst1n_trans [lemma, in clos_rst1n_trans]
clos_rt1n_step [lemma, in clos_rt1n_step]
clos_rst_rst1n [lemma, in clos_rst_rst1n]
clos_rt_rt1n_iff [lemma, in clos_rt_rt1n_iff]
clos_rstn1_rst [lemma, in clos_rstn1_rst]
clos_rtn1_rt [lemma, in clos_rtn1_rt]
clos_trans_n1 [inductive, in clos_trans_n1]
clos_rt_rt1n [lemma, in clos_rt_rt1n]
clos_rtn1_step [lemma, in clos_rtn1_step]
clos_rst_rstn1_iff [lemma, in clos_rst_rstn1_iff]
clos_trans_tn1_iff [lemma, in clos_trans_tn1_iff]
clos_rt_rtn1 [lemma, in clos_rt_rtn1]
clos_rst_is_equiv [lemma, in clos_rst_is_equiv]
clos_rt_clos_rst [lemma, in clos_rt_clos_rst]
clos_rstn1_trans [lemma, in clos_rstn1_trans]
clos_rst_rst1n_iff [lemma, in clos_rst_rst1n_iff]
clos_trans [inductive, in clos_trans]
clos_rst_rstn1 [lemma, in clos_rst_rstn1]
clos_rt_rtn1_iff [lemma, in clos_rt_rtn1_iff]
clos_rst1n_rst [lemma, in clos_rst1n_rst]
clos_refl_trans [inductive, in clos_refl_trans]
clos_rst_idempotent [lemma, in clos_rst_idempotent]
Cmp [definition, in Cmp]
CmpNotation [module, in CmpNotation]
_ ?= _ [notation, in ::x_'?='_x]
CmpSpec [module, in CmpSpec]
CmpSpec.compare_spec [axiom, in compare_spec]
coherent [definition, in coherent]
COHERENT_VALUE [section, in COHERENT_VALUE]
coherent_symmetric [lemma, in coherent_symmetric]
color [inductive, in color]
Color [module, in Color]
Color.t [definition, in t]
Combinators [library]
combine [definition, in combine]
combine_split [lemma, in combine_split]
combine_nth [lemma, in combine_nth]
combine_length [lemma, in combine_length]
commut [definition, in commut]
comm_left [lemma, in comm_left]
comm_right [lemma, in comm_right]
comp [definition, in comp]
compact [definition, in compact]
compact_P4 [lemma, in compact_P4]
compact_P3 [lemma, in compact_P3]
compact_P6 [lemma, in compact_P6]
compact_P1 [lemma, in compact_P1]
compact_EMP [lemma, in compact_EMP]
compact_carac [lemma, in compact_carac]
compact_P2 [lemma, in compact_P2]
compact_P5 [lemma, in compact_P5]
compact_eqDom [lemma, in compact_eqDom]
compare [definition, in compare]
Compare [inductive, in Compare]
Compare [library]
CompareBasedOrder [module, in CompareBasedOrder]
CompareBasedOrderFacts [module, in CompareBasedOrderFacts]
CompareBasedOrderFacts.compare_ngt_iff [lemma, in compare_ngt_iff]
CompareBasedOrderFacts.compare_eq [lemma, in compare_eq]
CompareBasedOrderFacts.compare_spec [lemma, in compare_spec]
CompareBasedOrderFacts.compare_gt_iff [lemma, in compare_gt_iff]
CompareBasedOrderFacts.compare_nle_iff [lemma, in compare_nle_iff]
CompareBasedOrderFacts.compare_nlt_iff [lemma, in compare_nlt_iff]
CompareBasedOrderFacts.compare_refl [lemma, in compare_refl]
CompareBasedOrderFacts.compare_ge_iff [lemma, in compare_ge_iff]
CompareBasedOrderFacts.compare_nge_iff [lemma, in compare_nge_iff]
CompareBasedOrderFacts.lt_irrefl [lemma, in lt_irrefl]
CompareBasedOrderFacts.lt_eq_cases [lemma, in lt_eq_cases]
CompareBasedOrder.compare_lt_iff [axiom, in compare_lt_iff]
CompareBasedOrder.compare_antisym [axiom, in compare_antisym]
CompareBasedOrder.compare_le_iff [axiom, in compare_le_iff]
CompareBasedOrder.compare_eq_iff [axiom, in compare_eq_iff]
CompareFacts [module, in CompareFacts]
CompareFacts.compare_lt_iff [lemma, in compare_lt_iff]
CompareFacts.compare_ngt_iff [lemma, in compare_ngt_iff]
CompareFacts.compare_eq [lemma, in compare_eq]
CompareFacts.compare_antisym [lemma, in compare_antisym]
CompareFacts.compare_gt_iff [lemma, in compare_gt_iff]
CompareFacts.compare_compat [instance, in compare_compat]
CompareFacts.compare_nlt_iff [lemma, in compare_nlt_iff]
CompareFacts.compare_refl [lemma, in compare_refl]
CompareFacts.compare_eq_iff [lemma, in compare_eq_iff]
_ ?= _ [notation, in ::x_'?='_x]
CompareRec [section, in CompareRec]
CompareRec.compare [variable, in compare]
CompareRec.compare_m [variable, in compare_m]
CompareRec.compare0_m [variable, in compare0_m]
CompareRec.double_to_Z [variable, in double_to_Z]
CompareRec.double_wB [variable, in double_wB]
CompareRec.double_to_Z_pos [variable, in double_to_Z_pos]
CompareRec.double_wB_lt [variable, in double_wB_lt]
CompareRec.spec_compare_m [variable, in spec_compare_m]
CompareRec.spec_compare0_m [variable, in spec_compare0_m]
CompareRec.spec_compare [variable, in spec_compare]
CompareRec.w [variable, in w]
CompareRec.wm [variable, in wm]
CompareRec.wm_base [variable, in wm_base]
CompareRec.wm_base_lt [variable, in wm_base_lt]
CompareRec.wm_to_Z_pos [variable, in wm_to_Z_pos]
CompareRec.wm_to_Z [variable, in wm_to_Z]
CompareRec.w_to_Z [variable, in w_to_Z]
CompareRec.w_to_Z_0 [variable, in w_to_Z_0]
CompareRec.w_0 [variable, in w_0]
CompareSpec [inductive, in CompareSpec]
CompareSpecT [inductive, in CompareSpecT]
CompareSpec2Type [lemma, in CompareSpec2Type]
compare_mn_1 [definition, in compare_mn_1]
Compare_dec [library]
compare0_mn [definition, in compare0_mn]
Compare2EqBool [module, in Compare2EqBool]
Compare2EqBool.eqb [definition, in eqb]
Compare2EqBool.eqb_eq [lemma, in eqb_eq]
compare31 [definition, in compare31]
comparison [inductive, in comparison]
Compatible [definition, in Compatible]
compat_nat [definition, in compat_nat]
compat_P [definition, in compat_P]
compat_op [definition, in compat_op]
compat_bool [definition, in compat_bool]
CompEq [constructor, in CompEq]
CompEqT [constructor, in CompEqT]
CompGt [constructor, in CompGt]
CompGtT [constructor, in CompGtT]
complement [definition, in complement]
Complement [definition, in Complement]
Complement [definition, in Complement]
complementary [definition, in complementary]
complementary_P1 [lemma, in complementary_P1]
complement_inverse [lemma, in complement_inverse]
Complement_Complement [lemma, in Complement_Complement]
complement_proper [definition, in complement_proper]
complement_Symmetric [definition, in complement_Symmetric]
complement_negative [definition, in complement_negative]
Complete [inductive, in Complete]
completeness [axiom, in completeness]
completeness_weak [lemma, in completeness_weak]
CompLt [constructor, in CompLt]
CompLtT [constructor, in CompLtT]
CompOpp [definition, in CompOpp]
CompOpp_inj [lemma, in CompOpp_inj]
CompOpp_involutive [lemma, in CompOpp_involutive]
CompOpp_iff [lemma, in CompOpp_iff]
compose [definition, in compose]
compose_proper [instance, in compose_proper]
compose_assoc [lemma, in compose_assoc]
compose_id_right [lemma, in compose_id_right]
compose_id_left [lemma, in compose_id_left]
CompSpec [definition, in CompSpec]
CompSpecT [definition, in CompSpecT]
CompSpec2Type [lemma, in CompSpec2Type]
Conditionally_complete [inductive, in Conditionally_complete]
conditional_eq [definition, in conditional_eq]
cond_nonpos [projection, in cond_nonpos]
cond_nonneg [projection, in cond_nonneg]
cond_pos_sum [lemma, in cond_pos_sum]
cond_D1 [projection, in cond_D1]
cond_diff [projection, in cond_diff]
cond_neg [projection, in cond_neg]
cond_D2 [projection, in cond_D2]
cond_fam [projection, in cond_fam]
cond_eq [lemma, in cond_eq]
cond_nonzero [projection, in cond_nonzero]
cond_positivity [definition, in cond_positivity]
cond_pos [projection, in cond_pos]
confluent [definition, in confluent]
Confluent [definition, in Confluent]
cong_transitive_same_relation [lemma, in cong_transitive_same_relation]
cong_antisymmetric_same_relation [lemma, in cong_antisymmetric_same_relation]
cong_congr [lemma, in cong_congr]
cong_reflexive_same_relation [lemma, in cong_reflexive_same_relation]
cong_symmetric_same_relation [lemma, in cong_symmetric_same_relation]
conj [constructor, in conj]
Conjunction [section, in Conjunction]
Conjunction.A [variable, in A]
Conjunction.B [variable, in B]
connectives [section, in connectives]
connectives.A [variable, in A]
connectives.B [variable, in B]
connectives.C [variable, in C]
connectives.D [variable, in D]
connectives.H1 [variable, in H1]
connectives.H2 [variable, in H2]
Cons [abbreviation, in Cons]
Cons [constructor, in Cons]
cons [constructor, in cons]
cons [constructor, in cons]
cons [abbreviation, in cons]
cons [constructor, in cons]
const [definition, in const]
const [definition, in const]
const [definition, in const]
constant [definition, in constant]
Constant_Stream.a [variable, in a]
constant_D_eq [definition, in constant_D_eq]
Constant_Stream [section, in Constant_Stream]
Constant_Stream.A [variable, in A]
ConstructiveDefiniteDescription [abbreviation, in ConstructiveDefiniteDescription]
ConstructiveDefiniteDescription_on [definition, in ConstructiveDefiniteDescription_on]
ConstructiveEpsilon [library]
ConstructiveGroundEpsilon [section, in ConstructiveGroundEpsilon]
ConstructiveGroundEpsilon_nat.P [variable, in P]
ConstructiveGroundEpsilon_nat.P_decidable [variable, in P_decidable]
ConstructiveGroundEpsilon_nat [section, in ConstructiveGroundEpsilon_nat]
ConstructiveGroundEpsilon.A [variable, in A]
ConstructiveGroundEpsilon.f [variable, in f]
ConstructiveGroundEpsilon.g [variable, in g]
ConstructiveGroundEpsilon.gof_eq_id [variable, in gof_eq_id]
ConstructiveGroundEpsilon.P [variable, in P]
ConstructiveGroundEpsilon.P_decidable [variable, in P_decidable]
ConstructiveIndefiniteDescription [abbreviation, in ConstructiveIndefiniteDescription]
ConstructiveIndefiniteDescription_on [definition, in ConstructiveIndefiniteDescription_on]
ConstructiveIndefiniteGroundDescription_Acc.P [variable, in P]
ConstructiveIndefiniteGroundDescription_Direct.P [variable, in P]
ConstructiveIndefiniteGroundDescription_Direct.P_dec [variable, in P_dec]
ConstructiveIndefiniteGroundDescription_Acc.R [variable, in R]
ConstructiveIndefiniteGroundDescription_Direct [section, in ConstructiveIndefiniteGroundDescription_Direct]
ConstructiveIndefiniteGroundDescription_Acc.P_decidable [variable, in P_decidable]
ConstructiveIndefiniteGroundDescription_Acc [section, in ConstructiveIndefiniteGroundDescription_Acc]
constructive_indefinite_ground_description [lemma, in constructive_indefinite_ground_description]
constructive_indefinite_ground_description_nat [definition, in constructive_indefinite_ground_description_nat]
constructive_indefinite_description_and_small_drinker_iff_epsilon [lemma, in constructive_indefinite_description_and_small_drinker_iff_epsilon]
constructive_ground_epsilon_spec_nat [definition, in constructive_ground_epsilon_spec_nat]
constructive_epsilon_spec_nat [abbreviation, in constructive_epsilon_spec_nat]
constructive_indefinite_description [axiom, in constructive_indefinite_description]
constructive_indefinite_description [lemma, in constructive_indefinite_description]
constructive_indefinite_description [abbreviation, in constructive_indefinite_description]
constructive_indefinite_description [axiom, in constructive_indefinite_description]
constructive_definite_description [lemma, in constructive_definite_description]
constructive_definite_description [lemma, in constructive_definite_description]
constructive_definite_description [axiom, in constructive_definite_description]
constructive_definite_description [abbreviation, in constructive_definite_description]
constructive_definite_description [lemma, in constructive_definite_description]
constructive_epsilon_nat [abbreviation, in constructive_epsilon_nat]
constructive_epsilon_spec [abbreviation, in constructive_epsilon_spec]
constructive_indefinite_description_and_small_drinker_imp_epsilon [lemma, in constructive_indefinite_description_and_small_drinker_imp_epsilon]
constructive_ground_epsilon [definition, in constructive_ground_epsilon]
constructive_definite_ground_description [lemma, in constructive_definite_ground_description]
constructive_ground_epsilon_nat [definition, in constructive_ground_epsilon_nat]
constructive_epsilon [abbreviation, in constructive_epsilon]
constructive_indefinite_ground_description_nat_Acc [lemma, in constructive_indefinite_ground_description_nat_Acc]
constructive_indefinite_descr_fun_choice [lemma, in constructive_indefinite_descr_fun_choice]
constructive_ground_epsilon_spec [definition, in constructive_ground_epsilon_spec]
constructive_definite_descr_fun_reification [lemma, in constructive_definite_descr_fun_reification]
constructive_definite_descr_excluded_middle [lemma, in constructive_definite_descr_excluded_middle]
constructive_indefinite_description_nat [abbreviation, in constructive_indefinite_description_nat]
Constructive_sets [library]
const_nth [lemma, in const_nth]
cons_Rlist [definition, in cons_Rlist]
cons_leA [abbreviation, in cons_leA]
cons_inj [definition, in cons_inj]
cons_ORlist [definition, in cons_ORlist]
cons_sort [abbreviation, in cons_sort]
contains [definition, in contains]
contains_is_preorder [lemma, in contains_is_preorder]
contents [definition, in contents]
continue_in [definition, in continue_in]
continuity [definition, in continuity]
continuity_pt_div [lemma, in continuity_pt_div]
continuity_pt_scal [lemma, in continuity_pt_scal]
continuity_sin [lemma, in continuity_sin]
continuity_pt_plus [lemma, in continuity_pt_plus]
continuity_pt_const [lemma, in continuity_pt_const]
continuity_ab_min [lemma, in continuity_ab_min]
continuity_comp [lemma, in continuity_comp]
continuity_pt_finite_SF [lemma, in continuity_pt_finite_SF]
continuity_cos [lemma, in continuity_cos]
continuity_pt_comp [lemma, in continuity_pt_comp]
continuity_compact [lemma, in continuity_compact]
continuity_pt_recip_prelim [lemma, in continuity_pt_recip_prelim]
continuity_pt_inv [lemma, in continuity_pt_inv]
continuity_const [lemma, in continuity_const]
continuity_opp [lemma, in continuity_opp]
continuity_scal [lemma, in continuity_scal]
continuity_mult [lemma, in continuity_mult]
continuity_pt_minus [lemma, in continuity_pt_minus]
continuity_P2 [lemma, in continuity_P2]
continuity_seq [lemma, in continuity_seq]
continuity_pt_opp [lemma, in continuity_pt_opp]
continuity_P1 [lemma, in continuity_P1]
continuity_implies_RiemannInt [lemma, in continuity_implies_RiemannInt]
continuity_div [lemma, in continuity_div]
continuity_ab_maj [lemma, in continuity_ab_maj]
continuity_inv [lemma, in continuity_inv]
continuity_pt_sqrt [lemma, in continuity_pt_sqrt]
continuity_finite_sum [lemma, in continuity_finite_sum]
continuity_P3 [lemma, in continuity_P3]
continuity_pt_mult [lemma, in continuity_pt_mult]
continuity_pt_recip_interv [lemma, in continuity_pt_recip_interv]
continuity_pt [definition, in continuity_pt]
continuity_minus [lemma, in continuity_minus]
continuity_plus [lemma, in continuity_plus]
continuous_neq_0 [lemma, in continuous_neq_0]
contrapositive [lemma, in contrapositive]
cont_deriv [lemma, in cont_deriv]
cont1 [projection, in cont1]
Converse [section, in Converse]
Converse.A [variable, in A]
Converse.R [variable, in R]
Corollaries [section, in Corollaries]
Corollaries.U [variable, in U]
cos [definition, in cos]
COS [lemma, in COS]
cosd [definition, in cosd]
cosh [definition, in cosh]
cosh_0 [lemma, in cosh_0]
cosn_no_R0 [lemma, in cosn_no_R0]
cos_3PI2 [lemma, in cos_3PI2]
cos_2a [lemma, in cos_2a]
cos_approx [definition, in cos_approx]
cos_n [definition, in cos_n]
cos_incr_1 [lemma, in cos_incr_1]
cos_sym [lemma, in cos_sym]
cos_eq_0_0 [lemma, in cos_eq_0_0]
cos_pi2 [lemma, in cos_pi2]
cos_eq_0_1 [lemma, in cos_eq_0_1]
cos_PI3 [lemma, in cos_PI3]
cos_2a_sin [lemma, in cos_2a_sin]
cos_ub [definition, in cos_ub]
cos_le_0 [lemma, in cos_le_0]
cos_term [definition, in cos_term]
cos_PI2 [lemma, in cos_PI2]
cos_increasing_1 [lemma, in cos_increasing_1]
cos_5PI4 [lemma, in cos_5PI4]
cos_eq_0_2PI_1 [lemma, in cos_eq_0_2PI_1]
cos_period [lemma, in cos_period]
cos_increasing_0 [lemma, in cos_increasing_0]
cos_bound [lemma, in cos_bound]
cos_in [definition, in cos_in]
cos_decr_1 [lemma, in cos_decr_1]
cos_PI4 [lemma, in cos_PI4]
cos_incr_0 [lemma, in cos_incr_0]
cos_sin_0 [lemma, in cos_sin_0]
cos_gt_0 [lemma, in cos_gt_0]
cos_PI [lemma, in cos_PI]
cos_0 [lemma, in cos_0]
cos_PI6 [lemma, in cos_PI6]
cos_2a_cos [lemma, in cos_2a_cos]
cos_lb [definition, in cos_lb]
cos_decr_0 [lemma, in cos_decr_0]
cos_minus [lemma, in cos_minus]
cos_eq_0_2PI_0 [lemma, in cos_eq_0_2PI_0]
cos_neg [lemma, in cos_neg]
cos_plus_form [lemma, in cos_plus_form]
cos_lt_0 [lemma, in cos_lt_0]
cos_sin [lemma, in cos_sin]
cos_sin_0_var [lemma, in cos_sin_0_var]
cos_ge_0_3PI2 [lemma, in cos_ge_0_3PI2]
cos_plus [lemma, in cos_plus]
cos_2PI [lemma, in cos_2PI]
cos_decreasing_1 [lemma, in cos_decreasing_1]
COS_bound [lemma, in COS_bound]
cos_ge_0 [lemma, in cos_ge_0]
cos_shift [lemma, in cos_shift]
cos_2PI3 [lemma, in cos_2PI3]
cos_decreasing_0 [lemma, in cos_decreasing_0]
Cos_plus [library]
Cos_rel [library]
cos2 [lemma, in cos2]
cos3PI4 [lemma, in cos3PI4]
count_occ_cons_eq [lemma, in count_occ_cons_eq]
count_occ_inv_nil [lemma, in count_occ_inv_nil]
count_occ [definition, in count_occ]
count_occ_nil [lemma, in count_occ_nil]
count_occ_In [lemma, in count_occ_In]
count_occ_cons_neq [lemma, in count_occ_cons_neq]
Couple [inductive, in Couple]
Couple_r [constructor, in Couple_r]
Couple_l [constructor, in Couple_l]
Couple_as_union [lemma, in Couple_as_union]
Couple_inv [lemma, in Couple_inv]
covering [definition, in covering]
covering_open_set [definition, in covering_open_set]
covering_finite [definition, in covering_finite]
covers [inductive, in covers]
covers_is_Add [lemma, in covers_is_Add]
covers_Add [lemma, in covers_Add]
co_interval [definition, in co_interval]
Cpo [record, in Cpo]
Cpo [library]
Cpo_cond [projection, in Cpo_cond]
cstlist [definition, in cstlist]
Cutting [section, in Cutting]
Cutting.A [variable, in A]
CVN_R_cos [lemma, in CVN_R_cos]
CVN_R_CVS [lemma, in CVN_R_CVS]
CVN_CVU [lemma, in CVN_CVU]
CVN_r [definition, in CVN_r]
CVN_R [definition, in CVN_R]
CVN_R_sin [lemma, in CVN_R_sin]
CVU [definition, in CVU]
CVU_continuity [lemma, in CVU_continuity]
cv_speed_pow_fact [lemma, in cv_speed_pow_fact]
cv_cvabs [lemma, in cv_cvabs]
CV_Cauchy [lemma, in CV_Cauchy]
CV_ALT_step2 [lemma, in CV_ALT_step2]
CV_ALT_step4 [lemma, in CV_ALT_step4]
CV_ALT_step1 [lemma, in CV_ALT_step1]
cv_infty_cv_R0 [lemma, in cv_infty_cv_R0]
CV_ALT_step3 [lemma, in CV_ALT_step3]
CV_mult [lemma, in CV_mult]
CV_minus [lemma, in CV_minus]
cv_infty [definition, in cv_infty]
cv_dicho [lemma, in cv_dicho]
cv_cauchy_2 [lemma, in cv_cauchy_2]
cv_cauchy_1 [lemma, in cv_cauchy_1]
CV_ALT [lemma, in CV_ALT]
CV_opp [lemma, in CV_opp]
CV_plus [lemma, in CV_plus]
CV_ALT_step0 [lemma, in CV_ALT_step0]
CyclicAxioms [library]
CyclicRing [module, in CyclicRing]
CyclicRing.add_opp_diag_r [lemma, in add_opp_diag_r]
CyclicRing.add_assoc [lemma, in add_assoc]
CyclicRing.add_comm [lemma, in add_comm]
CyclicRing.add_0_l [lemma, in add_0_l]
CyclicRing.add_opp_r [lemma, in add_opp_r]
CyclicRing.CyclicRing [lemma, in CyclicRing]
CyclicRing.eq [definition, in eq]
CyclicRing.eqb [definition, in eqb]
CyclicRing.eqb_eq [lemma, in eqb_eq]
CyclicRing.eqb_correct [lemma, in eqb_correct]
CyclicRing.mul_1_l [lemma, in mul_1_l]
CyclicRing.mul_add_distr_r [lemma, in mul_add_distr_r]
CyclicRing.mul_comm [lemma, in mul_comm]
CyclicRing.mul_assoc [lemma, in mul_assoc]
CyclicRing.wB [abbreviation, in wB]
_ == _ [notation, in ::x_'=='_x]
_ - _ [notation, in ::x_'-'_x]
_ * _ [notation, in ::x_'*'_x]
_ + _ [notation, in ::x_'+'_x]
- _ [notation, in ::'-'_x]
0 [notation, in ::'0']
1 [notation, in ::'1']
[| _ |] [notation, in ::'[|'_x_'|]']
CyclicType [module, in CyclicType]
CyclicType.ops [instance, in ops]
CyclicType.specs [instance, in specs]
CyclicType.t [axiom, in t]
Cyclic31 [library]
C_maj [lemma, in C_maj]
c_sqrt [constructor, in c_sqrt]
C0 [constructor, in C0]
C0_id [lemma, in C0_id]
c1 [projection, in c1]
C1 [constructor, in C1]
C1 [definition, in C1]
C1_plus_wB [lemma, in C1_plus_wB]
C1_fun [record, in C1_fun]
C1_cvg [lemma, in C1_cvg]