| 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 | _ | (7984 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 | _ | (401 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (5228 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 | _ | (292 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 | _ | (184 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 | _ | (1519 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (85 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 | _ | (275 entries) |
C
C [definition, in Coq.Reals.Binomial]canonical_Rsqr [lemma, in Coq.Reals.R_sqr]
cardinal [axiom, in Coq.FSets.FSetWeakInterface]
cardinal [inductive, in Coq.Sets.Finite_sets]
cardinal [axiom, in Coq.FSets.FSetInterface]
cardinal [axiom, in Coq.FSets.FSetInterface]
cardinalO_empty [lemma, in Coq.Sets.Finite_sets_facts]
cardinal_decreases [lemma, in Coq.Sets.Image]
cardinal_elim [lemma, in Coq.Sets.Finite_sets]
cardinal_Empty [lemma, in Coq.Sets.Finite_sets_facts]
cardinal_finite [lemma, in Coq.Sets.Finite_sets_facts]
cardinal_Im_intro [lemma, in Coq.Sets.Image]
cardinal_invert [lemma, in Coq.Sets.Finite_sets]
cardinal_is_functional [lemma, in Coq.Sets.Finite_sets_facts]
cardinal_unicity [lemma, in Coq.Sets.Finite_sets_facts]
cardinal_1 [axiom, in Coq.FSets.FSetInterface]
cardinal_1 [axiom, in Coq.FSets.FSetWeakInterface]
card_add [constructor, in Coq.Sets.Finite_sets]
card_Add_gen [lemma, in Coq.Sets.Finite_sets_facts]
card_empty [constructor, in Coq.Sets.Finite_sets]
card_soustr_1 [lemma, in Coq.Sets.Finite_sets_facts]
Carrier [definition, in Coq.Sets.Partial_Order]
carrier_of_areflexive_relation_class [definition, in Coq.Setoids.Setoid]
carrier_of_reflexive_relation_class [definition, in Coq.Setoids.Setoid]
carrier_of_relation_class [definition, in Coq.Setoids.Setoid]
caseRxy [lemma, in Coq.Relations.Newman]
cauchy_abs [lemma, in Coq.Reals.PartSum]
cauchy_bound [lemma, in Coq.Reals.Rseries]
Cauchy_crit [definition, in Coq.Reals.Rseries]
Cauchy_crit_series [definition, in Coq.Reals.PartSum]
cauchy_finite [lemma, in Coq.Reals.Cauchy_prod]
cauchy_maj [lemma, in Coq.Reals.SeqProp]
cauchy_min [lemma, in Coq.Reals.SeqProp]
cauchy_opp [lemma, in Coq.Reals.SeqProp]
Cauchy_prod [library]
Cesaro [lemma, in Coq.Reals.SeqSeries]
Cesaro_1 [lemma, in Coq.Reals.SeqSeries]
Chain [inductive, in Coq.Sets.Cpo]
Charac [constructor, in Coq.Sets.Uniset]
charac [definition, in Coq.Sets.Uniset]
check_if_variance_is_respected [inductive, in Coq.Setoids.Setoid]
choice [lemma, in Coq.Logic.ClassicalChoice]
choice [lemma, in Coq.Logic.ConstructiveEpsilon]
choice [lemma, in Coq.Logic.ClassicalEpsilon]
Choice [lemma, in Coq.Init.Specif]
ChoiceFacts [library]
Choice2 [lemma, in Coq.Init.Specif]
choose [axiom, in Coq.FSets.FSetInterface]
choose [axiom, in Coq.FSets.FSetInterface]
choose [axiom, in Coq.FSets.FSetWeakInterface]
choose_1 [axiom, in Coq.FSets.FSetInterface]
choose_1 [axiom, in Coq.FSets.FSetWeakInterface]
choose_2 [axiom, in Coq.FSets.FSetWeakInterface]
choose_2 [axiom, in Coq.FSets.FSetInterface]
classic [axiom, in Coq.Logic.Classical_Prop]
Classical [library]
ClassicalChoice [library]
ClassicalDefiniteDescription [definition, in Coq.Logic.ChoiceFacts]
ClassicalDescription [library]
ClassicalEpsilon [library]
ClassicalFacts [library]
ClassicalIndefiniteDescription [definition, in Coq.Logic.ChoiceFacts]
ClassicalUniqueChoice [library]
classical_definite_description [lemma, in Coq.Logic.ClassicalDescription]
classical_denumerable_description_imp_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
classical_indefinite_description [lemma, in Coq.Logic.ClassicalEpsilon]
Classical_Pred_Set [library]
Classical_Pred_Type [library]
classical_proof_irrelevence [lemma, in Coq.Logic.Berardi]
Classical_Prop [library]
Classical_sets [library]
Classical_Type [library]
classic_set [lemma, in Coq.Logic.ClassicalUniqueChoice]
closed_set [definition, in Coq.Reals.Rtopology]
closed_set_P1 [lemma, in Coq.Reals.Rtopology]
clos_refl_sym_trans [inductive, in Coq.Relations.Relation_Operators]
clos_refl_trans [inductive, in Coq.Relations.Relation_Operators]
clos_refl_trans_ind_left [lemma, in Coq.Relations.Operators_Properties]
clos_rst_idempotent [lemma, in Coq.Relations.Operators_Properties]
clos_rst_is_equiv [lemma, in Coq.Relations.Operators_Properties]
clos_rt_clos_rst [lemma, in Coq.Relations.Operators_Properties]
clos_rt_idempotent [lemma, in Coq.Relations.Operators_Properties]
clos_rt_is_preorder [lemma, in Coq.Relations.Operators_Properties]
clos_trans [inductive, in Coq.Relations.Relation_Operators]
coherence [definition, in Coq.Relations.Newman]
coherence_intro [lemma, in Coq.Relations.Newman]
coherence_sym [lemma, in Coq.Relations.Newman]
coherent [definition, in Coq.Sets.Relations_3]
coherent_symmetric [lemma, in Coq.Sets.Relations_3_facts]
combine [definition, in Coq.Lists.List]
combine_length [lemma, in Coq.Lists.List]
combine_nth [lemma, in Coq.Lists.List]
combine_split [lemma, in Coq.Lists.List]
commut [definition, in Coq.Relations.Relation_Definitions]
commut [definition, in Coq.Relations.Rstar]
comm_left [lemma, in Coq.Sets.Permut]
comm_right [lemma, in Coq.Sets.Permut]
comp [definition, in Coq.Reals.Ranalysis1]
compact [definition, in Coq.Reals.Rtopology]
compact_carac [lemma, in Coq.Reals.Rtopology]
compact_EMP [lemma, in Coq.Reals.Rtopology]
compact_eqDom [lemma, in Coq.Reals.Rtopology]
compact_P1 [lemma, in Coq.Reals.Rtopology]
compact_P2 [lemma, in Coq.Reals.Rtopology]
compact_P3 [lemma, in Coq.Reals.Rtopology]
compact_P4 [lemma, in Coq.Reals.Rtopology]
compact_P5 [lemma, in Coq.Reals.Rtopology]
compact_P6 [lemma, in Coq.Reals.Rtopology]
compare [axiom, in Coq.FSets.FSetInterface]
compare [axiom, in Coq.FSets.OrderedType]
compare [axiom, in Coq.FSets.FSetInterface]
compare [axiom, in Coq.FSets.FMapInterface]
compare [axiom, in Coq.FSets.OrderedTypeAlt]
Compare [inductive, in Coq.FSets.OrderedType]
compare [axiom, in Coq.FSets.OrderedTypeEx]
Compare [library]
Compare_dec [library]
compare_sym [axiom, in Coq.FSets.OrderedTypeAlt]
compare_trans [axiom, in Coq.FSets.OrderedTypeAlt]
comparison [inductive, in Coq.Init.Datatypes]
Compatible [definition, in Coq.Sets.Cpo]
compat_bool [definition, in Coq.FSets.FSetWeakInterface]
compat_bool [definition, in Coq.FSets.FSetInterface]
compat_nat [definition, in Coq.Lists.SetoidList]
compat_op [definition, in Coq.Lists.SetoidList]
compat_P [definition, in Coq.FSets.FSetInterface]
compat_P [definition, in Coq.FSets.FSetWeakInterface]
Complement [definition, in Coq.Sets.Ensembles]
Complement [definition, in Coq.Sets.Relations_1_facts]
complementary [definition, in Coq.Reals.Rtopology]
complementary_P1 [lemma, in Coq.Reals.Rtopology]
Complement_Complement [lemma, in Coq.Sets.Classical_sets]
Complete [inductive, in Coq.Sets.Cpo]
completeness [axiom, in Coq.Reals.Raxioms]
completeness_weak [lemma, in Coq.Reals.RIneq]
CompOpp [definition, in Coq.Init.Datatypes]
Conditionally_complete [inductive, in Coq.Sets.Cpo]
cond_eq [lemma, in Coq.Reals.SeqProp]
cond_positivity [definition, in Coq.Reals.Rsqrt_def]
cond_pos_sum [lemma, in Coq.Reals.PartSum]
confluence [definition, in Coq.Relations.Newman]
Confluent [definition, in Coq.Sets.Relations_3]
confluent [definition, in Coq.Sets.Relations_3]
congr_id [lemma, in Coq.Init.Logic_Type]
cong_antisymmetric_same_relation [lemma, in Coq.Sets.Relations_1_facts]
cong_congr [lemma, in Coq.Sets.Permut]
cong_reflexive_same_relation [lemma, in Coq.Sets.Relations_1_facts]
cong_symmetric_same_relation [lemma, in Coq.Sets.Relations_1_facts]
cong_transitive_same_relation [lemma, in Coq.Sets.Relations_1_facts]
conj [constructor, in Coq.Init.Logic]
cons [constructor, in Coq.Lists.List]
cons [constructor, in Coq.Lists.MonoList]
Cons [constructor, in Coq.Lists.Streams]
cons [constructor, in Coq.Reals.RList]
const [definition, in Coq.Lists.Streams]
constant [definition, in Coq.Reals.Ranalysis1]
constant_D_eq [definition, in Coq.Reals.Ranalysis1]
ConstructiveDefiniteDescription_on [definition, in Coq.Logic.ChoiceFacts]
ConstructiveEpsilon [library]
ConstructiveIndefiniteDescription_on [definition, in Coq.Logic.ChoiceFacts]
constructive_definite_description [axiom, in Coq.Logic.ClassicalDescription]
constructive_definite_description [lemma, in Coq.Logic.ClassicalEpsilon]
constructive_definite_description [lemma, in Coq.Logic.ConstructiveEpsilon]
constructive_definite_descr_excluded_middle [lemma, in Coq.Logic.ChoiceFacts]
constructive_definite_descr_fun_reification [lemma, in Coq.Logic.ChoiceFacts]
constructive_indefinite_description [axiom, in Coq.Logic.ClassicalEpsilon]
constructive_indefinite_description [lemma, in Coq.Logic.ConstructiveEpsilon]
constructive_indefinite_description_nat [lemma, in Coq.Logic.ConstructiveEpsilon]
constructive_indefinite_descr_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
Constructive_sets [library]
cons_leA [constructor, in Coq.Sorting.Sorting]
cons_ORlist [definition, in Coq.Reals.RList]
cons_Rlist [definition, in Coq.Reals.RList]
cons_sort [constructor, in Coq.Sorting.Sorting]
contains [definition, in Coq.Sets.Relations_1]
contains_is_preorder [lemma, in Coq.Sets.Relations_1_facts]
contents [definition, in Coq.Sorting.Heap]
continue_in [definition, in Coq.Reals.Rderiv]
continuity [definition, in Coq.Reals.Ranalysis1]
continuity_ab_maj [lemma, in Coq.Reals.Rtopology]
continuity_ab_min [lemma, in Coq.Reals.Rtopology]
continuity_comp [lemma, in Coq.Reals.Ranalysis1]
continuity_compact [lemma, in Coq.Reals.Rtopology]
continuity_const [lemma, in Coq.Reals.Ranalysis1]
continuity_cos [lemma, in Coq.Reals.Rtrigo_reg]
continuity_div [lemma, in Coq.Reals.Ranalysis1]
continuity_finite_sum [lemma, in Coq.Reals.Ranalysis4]
continuity_implies_RiemannInt [lemma, in Coq.Reals.RiemannInt]
continuity_inv [lemma, in Coq.Reals.Ranalysis1]
continuity_minus [lemma, in Coq.Reals.Ranalysis1]
continuity_mult [lemma, in Coq.Reals.Ranalysis1]
continuity_opp [lemma, in Coq.Reals.Ranalysis1]
continuity_plus [lemma, in Coq.Reals.Ranalysis1]
continuity_pt [definition, in Coq.Reals.Ranalysis1]
continuity_pt_comp [lemma, in Coq.Reals.Ranalysis1]
continuity_pt_const [lemma, in Coq.Reals.Ranalysis1]
continuity_pt_div [lemma, in Coq.Reals.Ranalysis1]
continuity_pt_finite_SF [lemma, in Coq.Reals.PSeries_reg]
continuity_pt_inv [lemma, in Coq.Reals.Ranalysis1]
continuity_pt_minus [lemma, in Coq.Reals.Ranalysis1]
continuity_pt_mult [lemma, in Coq.Reals.Ranalysis1]
continuity_pt_opp [lemma, in Coq.Reals.Ranalysis1]
continuity_pt_plus [lemma, in Coq.Reals.Ranalysis1]
continuity_pt_scal [lemma, in Coq.Reals.Ranalysis1]
continuity_pt_sqrt [lemma, in Coq.Reals.Sqrt_reg]
continuity_P1 [lemma, in Coq.Reals.Rtopology]
continuity_P2 [lemma, in Coq.Reals.Rtopology]
continuity_P3 [lemma, in Coq.Reals.Rtopology]
continuity_scal [lemma, in Coq.Reals.Ranalysis1]
continuity_seq [lemma, in Coq.Reals.Rsqrt_def]
continuity_sin [lemma, in Coq.Reals.Rtrigo_reg]
continuous_neq_0 [lemma, in Coq.Reals.Ranalysis2]
Contravariant [constructor, in Coq.Setoids.Setoid]
cont_deriv [lemma, in Coq.Reals.Rderiv]
cos [definition, in Coq.Reals.Rtrigo_def]
COS [lemma, in Coq.Reals.Rtrigo]
cosd [definition, in Coq.Reals.Rtrigo_calc]
cosh [definition, in Coq.Reals.Rtrigo_def]
cosh_0 [lemma, in Coq.Reals.Rtrigo_def]
cosn_no_R0 [lemma, in Coq.Reals.Rtrigo_def]
cos2 [lemma, in Coq.Reals.Rtrigo]
cos3PI4 [lemma, in Coq.Reals.Rtrigo_calc]
cos_approx [definition, in Coq.Reals.Rtrigo_alt]
COS_bound [lemma, in Coq.Reals.Rtrigo]
cos_bound [lemma, in Coq.Reals.Rtrigo_alt]
cos_decreasing_0 [lemma, in Coq.Reals.Rtrigo]
cos_decreasing_1 [lemma, in Coq.Reals.Rtrigo]
cos_decr_0 [lemma, in Coq.Reals.Rtrigo]
cos_decr_1 [lemma, in Coq.Reals.Rtrigo]
cos_eq_0_0 [lemma, in Coq.Reals.Rtrigo]
cos_eq_0_1 [lemma, in Coq.Reals.Rtrigo]
cos_eq_0_2PI_0 [lemma, in Coq.Reals.Rtrigo]
cos_eq_0_2PI_1 [lemma, in Coq.Reals.Rtrigo]
cos_ge_0 [lemma, in Coq.Reals.Rtrigo]
cos_ge_0_3PI2 [lemma, in Coq.Reals.Rtrigo]
cos_gt_0 [lemma, in Coq.Reals.Rtrigo]
cos_in [definition, in Coq.Reals.Rtrigo_def]
cos_increasing_0 [lemma, in Coq.Reals.Rtrigo]
cos_increasing_1 [lemma, in Coq.Reals.Rtrigo]
cos_incr_0 [lemma, in Coq.Reals.Rtrigo]
cos_incr_1 [lemma, in Coq.Reals.Rtrigo]
cos_lb [definition, in Coq.Reals.Rtrigo]
cos_le_0 [lemma, in Coq.Reals.Rtrigo]
cos_lt_0 [lemma, in Coq.Reals.Rtrigo]
cos_minus [lemma, in Coq.Reals.Rtrigo]
cos_n [definition, in Coq.Reals.Rtrigo_def]
cos_neg [lemma, in Coq.Reals.Rtrigo]
cos_period [lemma, in Coq.Reals.Rtrigo]
cos_PI [lemma, in Coq.Reals.Rtrigo]
cos_PI2 [lemma, in Coq.Reals.Rtrigo]
cos_PI3 [lemma, in Coq.Reals.Rtrigo_calc]
cos_PI4 [lemma, in Coq.Reals.Rtrigo_calc]
cos_PI6 [lemma, in Coq.Reals.Rtrigo_calc]
cos_plus [lemma, in Coq.Reals.Cos_plus]
Cos_plus [library]
cos_plus_form [lemma, in Coq.Reals.Cos_rel]
Cos_rel [library]
cos_shift [lemma, in Coq.Reals.Rtrigo]
cos_sin [lemma, in Coq.Reals.Rtrigo]
cos_sin_0 [lemma, in Coq.Reals.Rtrigo]
cos_sin_0_var [lemma, in Coq.Reals.Rtrigo]
cos_sym [lemma, in Coq.Reals.Rtrigo_def]
cos_term [definition, in Coq.Reals.Rtrigo_alt]
cos_ub [definition, in Coq.Reals.Rtrigo]
cos_0 [lemma, in Coq.Reals.Rtrigo_def]
cos_2a [lemma, in Coq.Reals.Rtrigo]
cos_2a_cos [lemma, in Coq.Reals.Rtrigo]
cos_2a_sin [lemma, in Coq.Reals.Rtrigo]
cos_2PI [lemma, in Coq.Reals.Rtrigo]
cos_2PI3 [lemma, in Coq.Reals.Rtrigo_calc]
cos_3PI2 [lemma, in Coq.Reals.Rtrigo]
cos_5PI4 [lemma, in Coq.Reals.Rtrigo_calc]
count_occ [definition, in Coq.Lists.List]
count_occ_cons_eq [lemma, in Coq.Lists.List]
count_occ_cons_neq [lemma, in Coq.Lists.List]
count_occ_In [lemma, in Coq.Lists.List]
count_occ_inv_nil [lemma, in Coq.Lists.List]
count_occ_nil [lemma, in Coq.Lists.List]
Couple [inductive, in Coq.Sets.Ensembles]
Couple_as_union [lemma, in Coq.Sets.Powerset_facts]
Couple_inv [lemma, in Coq.Sets.Constructive_sets]
Couple_l [constructor, in Coq.Sets.Ensembles]
Couple_r [constructor, in Coq.Sets.Ensembles]
Covariant [constructor, in Coq.Setoids.Setoid]
covering [definition, in Coq.Reals.Rtopology]
covering_finite [definition, in Coq.Reals.Rtopology]
covering_open_set [definition, in Coq.Reals.Rtopology]
covers [inductive, in Coq.Sets.Partial_Order]
covers_Add [lemma, in Coq.Sets.Powerset_Classical_facts]
covers_is_Add [lemma, in Coq.Sets.Powerset_Classical_facts]
co_interval [definition, in Coq.Reals.RiemannInt_SF]
Cpo [inductive, in Coq.Sets.Cpo]
Cpo [library]
CVN_CVU [lemma, in Coq.Reals.PSeries_reg]
CVN_r [definition, in Coq.Reals.PSeries_reg]
CVN_R [definition, in Coq.Reals.PSeries_reg]
CVN_R_cos [lemma, in Coq.Reals.Rtrigo_reg]
CVN_R_CVS [lemma, in Coq.Reals.PSeries_reg]
CVN_R_sin [lemma, in Coq.Reals.Rtrigo_reg]
CVU [definition, in Coq.Reals.PSeries_reg]
CVU_continuity [lemma, in Coq.Reals.PSeries_reg]
CV_ALT [lemma, in Coq.Reals.AltSeries]
CV_ALT_step0 [lemma, in Coq.Reals.AltSeries]
CV_ALT_step1 [lemma, in Coq.Reals.AltSeries]
CV_ALT_step2 [lemma, in Coq.Reals.AltSeries]
CV_ALT_step3 [lemma, in Coq.Reals.AltSeries]
CV_ALT_step4 [lemma, in Coq.Reals.AltSeries]
CV_Cauchy [lemma, in Coq.Reals.SeqProp]
cv_cauchy_1 [lemma, in Coq.Reals.PartSum]
cv_cauchy_2 [lemma, in Coq.Reals.PartSum]
cv_cvabs [lemma, in Coq.Reals.SeqProp]
cv_dicho [lemma, in Coq.Reals.Rsqrt_def]
cv_infty [definition, in Coq.Reals.SeqProp]
cv_infty_cv_R0 [lemma, in Coq.Reals.SeqProp]
CV_minus [lemma, in Coq.Reals.SeqProp]
CV_mult [lemma, in Coq.Reals.SeqProp]
CV_opp [lemma, in Coq.Reals.SeqProp]
CV_plus [lemma, in Coq.Reals.SeqProp]
cv_speed_pow_fact [lemma, in Coq.Reals.SeqProp]
C1 [definition, in Coq.Reals.Cos_rel]
C1_cvg [lemma, in Coq.Reals.Cos_rel]
C1_fun [inductive, in Coq.Reals.RiemannInt]
C_maj [lemma, in Coq.Reals.Rprod]
c_sqrt [constructor, in Coq.ZArith.Zsqrt]
| 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 | _ | (7984 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 | _ | (401 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (5228 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 | _ | (292 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 | _ | (184 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 | _ | (1519 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (85 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 | _ | (275 entries) |