Standard Library | The Coq Proof Assistant

Global Index

(23135 entries)

Notation Index

F

J

K

T

X

Y

_

(950 entries)

Module Index

J

X

Y

_

other

(746 entries)

Variable Index

H

J

Q

V

X

Y

_

other

(1491 entries)

Library Index

K

X

Y

_

other

(545 entries)

Lemma Index

other

(10708 entries)

Constructor Index

K

Y

_

other

(946 entries)

Axiom Index

K

V

X

Y

_

other

(603 entries)

Projection Index

G

K

V

X

Y

_

other

(461 entries)

Inductive Index

K

X

Y

_

other

(291 entries)

Section Index

H

J

Q

X

Y

_

other

(473 entries)

Instance Index

J

V

X

Y

_

other

(760 entries)

Abbreviation Index

J

Y

_

other

(1145 entries)

Definition Index

_

other

(3854 entries)

Record Index

J

V

X

Y

_

other

(162 entries)

D (lemma)

Dadd [in Coq.Reals.Rderiv]
Datan_eq_DatanSeq_interv [in Coq.Reals.Ratan]
Datan_continuity [in Coq.Reals.Ratan]
Datan_is_datan [in Coq.Reals.Ratan]
Datan_CVU_prelim [in Coq.Reals.Ratan]
Datan_lim [in Coq.Reals.Ratan]
Datan_seq_CV_0 [in Coq.Reals.Ratan]
Datan_seq_decreasing [in Coq.Reals.Ratan]
Datan_seq_increasing [in Coq.Reals.Ratan]
Datan_sum_eq [in Coq.Reals.Ratan]
Datan_seq_pos [in Coq.Reals.Ratan]
Datan_seq_Rabs [in Coq.Reals.Ratan]
Dcomp [in Coq.Reals.Rderiv]
Dcompare [in Coq.PArith.BinPos]
Dcompare_inf [in Coq.ZArith.ZArith_dec]
Dconst [in Coq.Reals.Rderiv]
DDcut_limit [in Coq.Reals.ConstructiveRealsLUB]
DDlow_below_up [in Coq.Reals.ConstructiveRealsLUB]
DecidableEqDepSet.eq_dep_eq [in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.eq_rect_eq [in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.inj_pair2 [in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.inj_pairP2 [in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.Streicher_K [in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.UIP [in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.UIP_refl [in Coq.Logic.Eqdep_dec]
DecidableEqDep.eq_dep_eq [in Coq.Logic.Eqdep_dec]
DecidableEqDep.eq_rect_eq [in Coq.Logic.Eqdep_dec]
DecidableEqDep.inj_pairP2 [in Coq.Logic.Eqdep_dec]
DecidableEqDep.inj_pairT2 [in Coq.Logic.Eqdep_dec]
DecidableEqDep.Streicher_K [in Coq.Logic.Eqdep_dec]
DecidableEqDep.UIP [in Coq.Logic.Eqdep_dec]
DecidableEqDep.UIP_refl [in Coq.Logic.Eqdep_dec]
Decidable_complete_alt [in Coq.btauto.Algebra]
Decidable_sound_alt [in Coq.btauto.Algebra]
Decidable_complete [in Coq.btauto.Algebra]
Decidable_sound [in Coq.btauto.Algebra]
Decidable_complete_alt [in Coq.Classes.DecidableClass]
Decidable_sound_alt [in Coq.Classes.DecidableClass]
Decidable_complete [in Coq.Classes.DecidableClass]
Decidable_sound [in Coq.Classes.DecidableClass]
decide [in Coq.Logic.Diaconescu]
decide_right [in Coq.Init.Tactics]
decide_left [in Coq.Init.Tactics]
decomp_sum [in Coq.Reals.PartSum]
decPcases [in Coq.ssr.ssrbool]
decrease_seq_transit [in Coq.Reals.Runcountable]
decreasing_prop [in Coq.Reals.SeqProp]
decreasing_ineq [in Coq.Reals.SeqProp]
decreasing_cv [in Coq.Reals.SeqProp]
decreasing_growing [in Coq.Reals.SeqProp]
dec_inh_nat_subset_has_unique_least_element [in Coq.Arith.Wf_nat]
dec_functional_relation [in Coq.Logic.Decidable]
dec_iff [in Coq.Logic.Decidable]
dec_imp [in Coq.Logic.Decidable]
dec_not [in Coq.Logic.Decidable]
dec_and [in Coq.Logic.Decidable]
dec_or [in Coq.Logic.Decidable]
dec_False [in Coq.Logic.Decidable]
dec_True [in Coq.Logic.Decidable]
dec_not_not [in Coq.Logic.Decidable]
dec_Zge [in Coq.ZArith.Zorder]
dec_Zgt [in Coq.ZArith.Zorder]
dec_Zne [in Coq.ZArith.Zorder]
dec_eq_nat [in Coq.Arith.Peano_dec]
dec_ge [in Coq.Arith.Compare_dec]
dec_gt [in Coq.Arith.Compare_dec]
dec_lt [in Coq.Arith.Compare_dec]
dec_le [in Coq.Arith.Compare_dec]
default_isIn_ok [in Coq.setoid_ring.Field_theory]
deg_rad [in Coq.Reals.Rtrigo_calc]
deletion [in Coq.Program.Equality]
denorm_correct [in Coq.micromega.RingMicromega]
depair_sanity [in Coq.Vectors.Fin]
dependent_choice [in Coq.Init.Specif]
dependent_unique_choice [in Coq.Logic.ClassicalDescription]
DepOfNodep.choose_equal [in Coq.FSets.FSetBridge]
DepOfNodep.choose_ok2 [in Coq.FSets.FSetBridge]
DepOfNodep.choose_ok1 [in Coq.FSets.FSetBridge]
DepOfNodep.compat_P_aux [in Coq.FSets.FSetBridge]
dep_iff_non_dep_functional_rel_reification [in Coq.Logic.ChoiceFacts]
dep_non_dep_functional_rel_reification [in Coq.Logic.ChoiceFacts]
dep_non_dep_functional_choice [in Coq.Logic.ChoiceFacts]
derivable_pt_lim_exp [in Coq.Reals.Exp_prop]
derivable_pt_lim_exp_0 [in Coq.Reals.Exp_prop]
derivable_pow [in Coq.Reals.Ranalysis1]
derivable_pt_pow [in Coq.Reals.Ranalysis1]
derivable_pt_lim_pow [in Coq.Reals.Ranalysis1]
derivable_pt_lim_pow_pos [in Coq.Reals.Ranalysis1]
derivable_comp [in Coq.Reals.Ranalysis1]
derivable_Rsqr [in Coq.Reals.Ranalysis1]
derivable_id [in Coq.Reals.Ranalysis1]
derivable_scal [in Coq.Reals.Ranalysis1]
derivable_const [in Coq.Reals.Ranalysis1]
derivable_mult [in Coq.Reals.Ranalysis1]
derivable_minus [in Coq.Reals.Ranalysis1]
derivable_opp [in Coq.Reals.Ranalysis1]
derivable_plus [in Coq.Reals.Ranalysis1]
derivable_pt_comp [in Coq.Reals.Ranalysis1]
derivable_pt_Rsqr [in Coq.Reals.Ranalysis1]
derivable_pt_id [in Coq.Reals.Ranalysis1]
derivable_pt_scal [in Coq.Reals.Ranalysis1]
derivable_pt_const [in Coq.Reals.Ranalysis1]
derivable_pt_mult [in Coq.Reals.Ranalysis1]
derivable_pt_minus [in Coq.Reals.Ranalysis1]
derivable_pt_opp [in Coq.Reals.Ranalysis1]
derivable_pt_plus [in Coq.Reals.Ranalysis1]
derivable_pt_lim_comp [in Coq.Reals.Ranalysis1]
derivable_pt_lim_Rsqr [in Coq.Reals.Ranalysis1]
derivable_pt_lim_id [in Coq.Reals.Ranalysis1]
derivable_pt_lim_scal_right [in Coq.Reals.Ranalysis1]
derivable_pt_lim_div_scal [in Coq.Reals.Ranalysis1]
derivable_pt_lim_scal [in Coq.Reals.Ranalysis1]
derivable_pt_lim_const [in Coq.Reals.Ranalysis1]
derivable_pt_lim_mult [in Coq.Reals.Ranalysis1]
derivable_pt_lim_minus [in Coq.Reals.Ranalysis1]
derivable_pt_lim_opp [in Coq.Reals.Ranalysis1]
derivable_pt_lim_plus [in Coq.Reals.Ranalysis1]
derivable_continuous [in Coq.Reals.Ranalysis1]
derivable_continuous_pt [in Coq.Reals.Ranalysis1]
derivable_derive [in Coq.Reals.Ranalysis1]
derivable_pt_lim_locally_ext [in Coq.Reals.Ranalysis1]
derivable_pt_lim_ext [in Coq.Reals.Ranalysis1]
derivable_pt_lim_D_in [in Coq.Reals.Ranalysis1]
derivable_pt_sqrt [in Coq.Reals.Sqrt_reg]
derivable_pt_lim_sqrt [in Coq.Reals.Sqrt_reg]
derivable_div [in Coq.Reals.Ranalysis3]
derivable_pt_div [in Coq.Reals.Ranalysis3]
derivable_pt_lim_div [in Coq.Reals.Ranalysis3]
derivable_cos [in Coq.Reals.Rtrigo_reg]
derivable_sin [in Coq.Reals.Rtrigo_reg]
derivable_pt_cos [in Coq.Reals.Rtrigo_reg]
derivable_pt_sin [in Coq.Reals.Rtrigo_reg]
derivable_pt_lim_cos [in Coq.Reals.Rtrigo_reg]
derivable_pt_lim_sin [in Coq.Reals.Rtrigo_reg]
derivable_pt_lim_cos_0 [in Coq.Reals.Rtrigo_reg]
derivable_pt_lim_sin_0 [in Coq.Reals.Rtrigo_reg]
derivable_sinh [in Coq.Reals.Ranalysis4]
derivable_cosh [in Coq.Reals.Ranalysis4]
derivable_exp [in Coq.Reals.Ranalysis4]
derivable_pt_sinh [in Coq.Reals.Ranalysis4]
derivable_pt_cosh [in Coq.Reals.Ranalysis4]
derivable_pt_exp [in Coq.Reals.Ranalysis4]
derivable_pt_lim_sinh [in Coq.Reals.Ranalysis4]
derivable_pt_lim_cosh [in Coq.Reals.Ranalysis4]
derivable_finite_sum [in Coq.Reals.Ranalysis4]
derivable_pt_finite_sum [in Coq.Reals.Ranalysis4]
derivable_pt_lim_finite_sum [in Coq.Reals.Ranalysis4]
derivable_pt_lim_fs [in Coq.Reals.Ranalysis4]
derivable_inv [in Coq.Reals.Ranalysis4]
derivable_pt_inv [in Coq.Reals.Ranalysis4]
derivable_pt_lim_arcsinh [in Coq.Reals.Rpower]
derivable_pt_lim_power [in Coq.Reals.Rpower]
derivable_pt_lim_ln [in Coq.Reals.Rpower]
derivable_pt_ps_atan [in Coq.Reals.Ratan]
derivable_pt_lim_ps_atan [in Coq.Reals.Ratan]
derivable_pt_lim_atan [in Coq.Reals.Ratan]
derivable_pt_atan [in Coq.Reals.Ratan]
derivable_pt_tan [in Coq.Reals.Ratan]
derivable_pt_lim_CVU [in Coq.Reals.Ranalysis5]
derivable_pt_recip_interv [in Coq.Reals.Ranalysis5]
derivable_pt_recip_interv_prelim1 [in Coq.Reals.Ranalysis5]
derivable_pt_recip_interv_prelim0 [in Coq.Reals.Ranalysis5]
derivable_pt_lim_recip_interv [in Coq.Reals.Ranalysis5]
derivable_pt_id_interv [in Coq.Reals.Ranalysis5]
derive_pt_pow [in Coq.Reals.Ranalysis1]
derive_pt_comp [in Coq.Reals.Ranalysis1]
derive_pt_Rsqr [in Coq.Reals.Ranalysis1]
derive_pt_id [in Coq.Reals.Ranalysis1]
derive_pt_scal [in Coq.Reals.Ranalysis1]
derive_pt_const [in Coq.Reals.Ranalysis1]
derive_pt_mult [in Coq.Reals.Ranalysis1]
derive_pt_minus [in Coq.Reals.Ranalysis1]
derive_pt_opp [in Coq.Reals.Ranalysis1]
derive_pt_plus [in Coq.Reals.Ranalysis1]
derive_pt_D_in [in Coq.Reals.Ranalysis1]
derive_pt_eq_1 [in Coq.Reals.Ranalysis1]
derive_pt_eq_0 [in Coq.Reals.Ranalysis1]
derive_pt_eq [in Coq.Reals.Ranalysis1]
derive_pt_sqrt [in Coq.Reals.Sqrt_reg]
derive_pt_div [in Coq.Reals.Ranalysis3]
derive_pt_cos [in Coq.Reals.Rtrigo_reg]
derive_pt_sin [in Coq.Reals.Rtrigo_reg]
derive_pt_sinh [in Coq.Reals.Ranalysis4]
derive_pt_cosh [in Coq.Reals.Ranalysis4]
derive_pt_exp [in Coq.Reals.Ranalysis4]
derive_pt_inv [in Coq.Reals.Ranalysis4]
derive_increasing_interv_var [in Coq.Reals.MVT]
derive_increasing_interv [in Coq.Reals.MVT]
derive_increasing_interv_ax [in Coq.Reals.MVT]
derive_pt_atan [in Coq.Reals.Ratan]
derive_increasing_interv [in Coq.Reals.Ratan]
derive_pt_tan [in Coq.Reals.Ratan]
derive_pt_recip_interv [in Coq.Reals.Ranalysis5]
derive_pt_recip_interv_prelim1_1 [in Coq.Reals.Ranalysis5]
derive_pt_recip_interv_prelim1_0 [in Coq.Reals.Ranalysis5]
derive_pt_recip_interv_prelim0 [in Coq.Reals.Ranalysis5]
deriv_constant2 [in Coq.Reals.Ranalysis1]
deriv_minimum [in Coq.Reals.Ranalysis1]
deriv_maximum [in Coq.Reals.Ranalysis1]
desc_end [in Coq.Wellfounded.Lexicographic_Exponentiation]
desc_tail [in Coq.Wellfounded.Lexicographic_Exponentiation]
desc_prefix [in Coq.Wellfounded.Lexicographic_Exponentiation]
destruct_list [in Coq.Lists.List]
diagonal_inverse2 [in Coq.Logic.ExtensionalityFacts]
diagonal_inverse1 [in Coq.Logic.ExtensionalityFacts]
diagonal_projs_same_behavior [in Coq.Logic.ExtensionalityFacts]
dicho_up_car [in Coq.Reals.Rsqrt_def]
dicho_lb_car [in Coq.Reals.Rsqrt_def]
dicho_lb_dicho_up [in Coq.Reals.Rsqrt_def]
dicho_up_cv [in Coq.Reals.Rsqrt_def]
dicho_lb_cv [in Coq.Reals.Rsqrt_def]
dicho_up_min [in Coq.Reals.Rsqrt_def]
dicho_up_min_x [in Coq.Reals.Rsqrt_def]
dicho_lb_maj [in Coq.Reals.Rsqrt_def]
dicho_lb_maj_y [in Coq.Reals.Rsqrt_def]
dicho_up_decreasing [in Coq.Reals.Rsqrt_def]
dicho_lb_growing [in Coq.Reals.Rsqrt_def]
dicho_comp [in Coq.Reals.Rsqrt_def]
diff_false_true [in Coq.Bool.Bool]
diff_true_false [in Coq.Bool.Bool]
dimemo_get_correct [in Coq.Lists.StreamMemo]
discrete_nat [in Coq.Arith.Compare]
disc_P1 [in Coq.Reals.Rtopology]
Disjoint_Intersection [in Coq.Sets.Powerset_facts]
distance_symm [in Coq.Reals.Rgeom]
distance_refl [in Coq.Reals.Rgeom]
Distributivity [in Coq.Sets.Powerset_facts]
Distributivity_l [in Coq.Sets.Powerset_facts]
Distributivity' [in Coq.Sets.Powerset_facts]
dist_Desc_concat [in Coq.Wellfounded.Lexicographic_Exponentiation]
dist_aux [in Coq.Wellfounded.Lexicographic_Exponentiation]
diveucl_21_spec_aux [in Coq.Numbers.Cyclic.Int63.Int63]
diveucl_spec [in Coq.Numbers.Cyclic.Int63.Int63]
diveucl_spec_aux [in Coq.Numbers.Cyclic.Int63.Cyclic63]
div_eq_inv [in Coq.Reals.Ranalysis1]
div_lt [in Coq.Numbers.Cyclic.Int63.Cyclic63]
div_le_0 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
div_Zdiv [in Coq.ZArith.Zdiv]
div2_not_R0 [in Coq.Reals.Exp_prop]
div2_S_double [in Coq.Reals.Exp_prop]
div2_double [in Coq.Reals.Exp_prop]
div2_phi [in Coq.Numbers.Cyclic.Int63.Int63]
div2_double_plus_one [in Coq.Arith.Div2]
div2_double [in Coq.Arith.Div2]
div2_odd [in Coq.Arith.Div2]
div2_even [in Coq.Arith.Div2]
div31_phi [in Coq.Numbers.Cyclic.Int31.Cyclic31]
div312_phi [in Coq.Numbers.Cyclic.Int31.Cyclic31]
Dln [in Coq.Reals.Rpower]
dmemo_get_correct [in Coq.Lists.StreamMemo]
Dminus [in Coq.Reals.Rderiv]
Dmult [in Coq.Reals.Rderiv]
Dmult_const [in Coq.Reals.Rderiv]
domain_P1 [in Coq.Reals.Rtopology]
Dopp [in Coq.Reals.Rderiv]
double [in Coq.Reals.RIneq]
doubleLeCovariant [in Coq.Reals.ConstructiveRcomplete]
double_var [in Coq.Reals.RIneq]
double_twice_plus_one_firstl [in Coq.Numbers.Cyclic.Int31.Cyclic31]
double_twice_firstl [in Coq.Numbers.Cyclic.Int31.Cyclic31]
double_odd [in Coq.Arith.Div2]
double_even [in Coq.Arith.Div2]
double_plus [in Coq.Arith.Div2]
double_S [in Coq.Arith.Div2]
Dpower [in Coq.Reals.Rpower]
DRealAbstrFalse [in Coq.Reals.ClassicalDedekindReals]
DRealOpen [in Coq.Reals.ClassicalDedekindReals]
DRealQuot1 [in Coq.Reals.ClassicalDedekindReals]
DRealQuot2 [in Coq.Reals.ClassicalDedekindReals]
DRealReprQ [in Coq.Reals.ClassicalDedekindReals]
DRealReprQup [in Coq.Reals.ClassicalDedekindReals]
Dx [in Coq.Reals.Rderiv]
Dx_pow_n [in Coq.Reals.Rderiv]
D_pow_n [in Coq.Reals.Rderiv]
D_x_no_cond [in Coq.Reals.Ranalysis2]
D_in_ext [in Coq.Reals.Rpower]
D_in_imp [in Coq.Reals.Rpower]

Global Index

(23135 entries)

Notation Index

F

J

K

T

X

Y

_

(950 entries)

Module Index

J

X

Y

_

other

(746 entries)

Variable Index

H

J

Q

V

X

Y

_

other

(1491 entries)

Library Index

K

X

Y

_

other

(545 entries)

Lemma Index

other

(10708 entries)

Constructor Index

K

Y

_

other

(946 entries)

Axiom Index

K

V

X

Y

_

other

(603 entries)

Projection Index

G

K

V

X

Y

_

other

(461 entries)

Inductive Index

K

X

Y

_

other

(291 entries)

Section Index

H

J

Q

X

Y

_

other

(473 entries)

Instance Index

J

V

X

Y

_

other

(760 entries)

Abbreviation Index

J

Y

_

other

(1145 entries)

Definition Index

_

other

(3854 entries)

Record Index

J

V

X

Y

_

other

(162 entries)