| 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) |
D (lemma)
Dadd [in Coq.Reals.Rderiv]Dcomp [in Coq.Reals.Rderiv]
Dcompare [in Coq.NArith.BinPos]
Dcompare_inf [in Coq.ZArith.ZArith_dec]
Dconst [in Coq.Reals.Rderiv]
DecidableEqDepSet.eq_dep_eq [in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.eq_rect_eq [in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.inj_pairP2 [in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.inj_pair2 [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]
decide [in Coq.Logic.Diaconescu]
decomp_sum [in Coq.Reals.PartSum]
decreasing_cv [in Coq.Reals.SeqProp]
decreasing_growing [in Coq.Reals.SeqProp]
decreasing_ineq [in Coq.Reals.SeqProp]
decreasing_prop [in Coq.Reals.SeqProp]
dec_and [in Coq.Logic.Decidable]
dec_eq [in Coq.ZArith.Zorder]
dec_eq_nat [in Coq.Arith.Peano_dec]
dec_False [in Coq.Logic.Decidable]
dec_ge [in Coq.Arith.Compare_dec]
dec_gt [in Coq.Arith.Compare_dec]
dec_imp [in Coq.Logic.Decidable]
dec_inh_nat_subset_has_unique_least_element [in Coq.Logic.ChoiceFacts]
dec_le [in Coq.Arith.Compare_dec]
dec_lt [in Coq.Arith.Compare_dec]
dec_not [in Coq.Logic.Decidable]
dec_not_not [in Coq.Logic.Decidable]
dec_or [in Coq.Logic.Decidable]
dec_True [in Coq.Logic.Decidable]
dec_Zge [in Coq.ZArith.Zorder]
dec_Zgt [in Coq.ZArith.Zorder]
dec_Zle [in Coq.ZArith.Zorder]
dec_Zlt [in Coq.ZArith.Zorder]
dec_Zne [in Coq.ZArith.Zorder]
deg_rad [in Coq.Reals.Rtrigo_calc]
dependent_unique_choice [in Coq.Logic.ClassicalDescription]
DepOfNodep.compat_P_aux [in Coq.FSets.FSetBridge]
dep_non_dep_functional_choice [in Coq.Logic.ChoiceFacts]
dep_non_dep_functional_rel_reification [in Coq.Logic.ChoiceFacts]
derivable_comp [in Coq.Reals.Ranalysis1]
derivable_const [in Coq.Reals.Ranalysis1]
derivable_continuous [in Coq.Reals.Ranalysis1]
derivable_continuous_pt [in Coq.Reals.Ranalysis1]
derivable_cos [in Coq.Reals.Rtrigo_reg]
derivable_cosh [in Coq.Reals.Ranalysis4]
derivable_derive [in Coq.Reals.Ranalysis1]
derivable_div [in Coq.Reals.Ranalysis3]
derivable_exp [in Coq.Reals.Ranalysis4]
derivable_finite_sum [in Coq.Reals.Ranalysis4]
derivable_id [in Coq.Reals.Ranalysis1]
derivable_inv [in Coq.Reals.Ranalysis4]
derivable_minus [in Coq.Reals.Ranalysis1]
derivable_mult [in Coq.Reals.Ranalysis1]
derivable_opp [in Coq.Reals.Ranalysis1]
derivable_plus [in Coq.Reals.Ranalysis1]
derivable_pow [in Coq.Reals.Ranalysis1]
derivable_pt_comp [in Coq.Reals.Ranalysis1]
derivable_pt_const [in Coq.Reals.Ranalysis1]
derivable_pt_cos [in Coq.Reals.Rtrigo_reg]
derivable_pt_cosh [in Coq.Reals.Ranalysis4]
derivable_pt_div [in Coq.Reals.Ranalysis3]
derivable_pt_exp [in Coq.Reals.Ranalysis4]
derivable_pt_finite_sum [in Coq.Reals.Ranalysis4]
derivable_pt_id [in Coq.Reals.Ranalysis1]
derivable_pt_inv [in Coq.Reals.Ranalysis4]
derivable_pt_lim_comp [in Coq.Reals.Ranalysis1]
derivable_pt_lim_const [in Coq.Reals.Ranalysis1]
derivable_pt_lim_cos [in Coq.Reals.Rtrigo_reg]
derivable_pt_lim_cosh [in Coq.Reals.Ranalysis4]
derivable_pt_lim_cos_0 [in Coq.Reals.Rtrigo_reg]
derivable_pt_lim_div [in Coq.Reals.Ranalysis3]
derivable_pt_lim_D_in [in Coq.Reals.Ranalysis1]
derivable_pt_lim_exp [in Coq.Reals.Exp_prop]
derivable_pt_lim_exp_0 [in Coq.Reals.Exp_prop]
derivable_pt_lim_finite_sum [in Coq.Reals.Ranalysis4]
derivable_pt_lim_fs [in Coq.Reals.Ranalysis4]
derivable_pt_lim_id [in Coq.Reals.Ranalysis1]
derivable_pt_lim_ln [in Coq.Reals.Rpower]
derivable_pt_lim_minus [in Coq.Reals.Ranalysis1]
derivable_pt_lim_mult [in Coq.Reals.Ranalysis1]
derivable_pt_lim_opp [in Coq.Reals.Ranalysis1]
derivable_pt_lim_plus [in Coq.Reals.Ranalysis1]
derivable_pt_lim_pow [in Coq.Reals.Ranalysis1]
derivable_pt_lim_power [in Coq.Reals.Rpower]
derivable_pt_lim_pow_pos [in Coq.Reals.Ranalysis1]
derivable_pt_lim_Rsqr [in Coq.Reals.Ranalysis1]
derivable_pt_lim_scal [in Coq.Reals.Ranalysis1]
derivable_pt_lim_sin [in Coq.Reals.Rtrigo_reg]
derivable_pt_lim_sinh [in Coq.Reals.Ranalysis4]
derivable_pt_lim_sin_0 [in Coq.Reals.Rtrigo_reg]
derivable_pt_lim_sqrt [in Coq.Reals.Sqrt_reg]
derivable_pt_minus [in Coq.Reals.Ranalysis1]
derivable_pt_mult [in Coq.Reals.Ranalysis1]
derivable_pt_opp [in Coq.Reals.Ranalysis1]
derivable_pt_plus [in Coq.Reals.Ranalysis1]
derivable_pt_pow [in Coq.Reals.Ranalysis1]
derivable_pt_Rsqr [in Coq.Reals.Ranalysis1]
derivable_pt_scal [in Coq.Reals.Ranalysis1]
derivable_pt_sin [in Coq.Reals.Rtrigo_reg]
derivable_pt_sinh [in Coq.Reals.Ranalysis4]
derivable_pt_sqrt [in Coq.Reals.Sqrt_reg]
derivable_Rsqr [in Coq.Reals.Ranalysis1]
derivable_scal [in Coq.Reals.Ranalysis1]
derivable_sin [in Coq.Reals.Rtrigo_reg]
derivable_sinh [in Coq.Reals.Ranalysis4]
derive_increasing_interv [in Coq.Reals.MVT]
derive_increasing_interv_ax [in Coq.Reals.MVT]
derive_increasing_interv_var [in Coq.Reals.MVT]
derive_pt_comp [in Coq.Reals.Ranalysis1]
derive_pt_const [in Coq.Reals.Ranalysis1]
derive_pt_cos [in Coq.Reals.Rtrigo_reg]
derive_pt_cosh [in Coq.Reals.Ranalysis4]
derive_pt_div [in Coq.Reals.Ranalysis3]
derive_pt_D_in [in Coq.Reals.Ranalysis1]
derive_pt_eq [in Coq.Reals.Ranalysis1]
derive_pt_eq_0 [in Coq.Reals.Ranalysis1]
derive_pt_eq_1 [in Coq.Reals.Ranalysis1]
derive_pt_exp [in Coq.Reals.Ranalysis4]
derive_pt_id [in Coq.Reals.Ranalysis1]
derive_pt_inv [in Coq.Reals.Ranalysis4]
derive_pt_minus [in Coq.Reals.Ranalysis1]
derive_pt_mult [in Coq.Reals.Ranalysis1]
derive_pt_opp [in Coq.Reals.Ranalysis1]
derive_pt_plus [in Coq.Reals.Ranalysis1]
derive_pt_pow [in Coq.Reals.Ranalysis1]
derive_pt_Rsqr [in Coq.Reals.Ranalysis1]
derive_pt_scal [in Coq.Reals.Ranalysis1]
derive_pt_sin [in Coq.Reals.Rtrigo_reg]
derive_pt_sinh [in Coq.Reals.Ranalysis4]
derive_pt_sqrt [in Coq.Reals.Sqrt_reg]
deriv_constant2 [in Coq.Reals.Ranalysis1]
deriv_maximum [in Coq.Reals.Ranalysis1]
deriv_minimum [in Coq.Reals.Ranalysis1]
description_rel_choice_imp_funct_choice [in Coq.Logic.ChoiceFacts]
desc_end [in Coq.Wellfounded.Lexicographic_Exponentiation]
desc_prefix [in Coq.Wellfounded.Lexicographic_Exponentiation]
desc_tail [in Coq.Wellfounded.Lexicographic_Exponentiation]
destruct_list [in Coq.Lists.List]
Diagram [in Coq.Relations.Newman]
dicho_comp [in Coq.Reals.Rsqrt_def]
dicho_lb_car [in Coq.Reals.Rsqrt_def]
dicho_lb_cv [in Coq.Reals.Rsqrt_def]
dicho_lb_dicho_up [in Coq.Reals.Rsqrt_def]
dicho_lb_growing [in Coq.Reals.Rsqrt_def]
dicho_lb_maj [in Coq.Reals.Rsqrt_def]
dicho_lb_maj_y [in Coq.Reals.Rsqrt_def]
dicho_up_car [in Coq.Reals.Rsqrt_def]
dicho_up_cv [in Coq.Reals.Rsqrt_def]
dicho_up_decreasing [in Coq.Reals.Rsqrt_def]
dicho_up_min [in Coq.Reals.Rsqrt_def]
dicho_up_min_x [in Coq.Reals.Rsqrt_def]
diff_false_true [in Coq.Bool.Bool]
diff_true_false [in Coq.Bool.Bool]
discrete_nat [in Coq.Arith.Compare]
disc_P1 [in Coq.Reals.Rtopology]
distance_refl [in Coq.Reals.Rgeom]
distance_symm [in Coq.Reals.Rgeom]
Distributivity [in Coq.Sets.Powerset_facts]
Distributivity' [in Coq.Sets.Powerset_facts]
distr_rev [in Coq.Lists.List]
dist_aux [in Coq.Wellfounded.Lexicographic_Exponentiation]
dist_Desc_concat [in Coq.Wellfounded.Lexicographic_Exponentiation]
div1 [in Coq.Arith.Div]
div2 [in Coq.Arith.Div]
div2_double [in Coq.Arith.Div2]
div2_double [in Coq.Reals.Exp_prop]
div2_double_plus_one [in Coq.Arith.Div2]
div2_even [in Coq.Arith.Div2]
div2_not_R0 [in Coq.Reals.Exp_prop]
div2_odd [in Coq.Arith.Div2]
div2_S_double [in Coq.Reals.Exp_prop]
div_eq_inv [in Coq.Reals.Ranalysis1]
Dln [in Coq.Reals.Rpower]
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]
double_eq_one_discr [in Coq.NArith.BinPos]
double_eq_zero_inversion [in Coq.NArith.BinPos]
double_even [in Coq.Arith.Div2]
double_moins_un_xO_discr [in Coq.NArith.BinPos]
double_odd [in Coq.Arith.Div2]
double_plus [in Coq.Arith.Div2]
double_plus_one_eq_one_inversion [in Coq.NArith.BinPos]
double_plus_one_zero_discr [in Coq.NArith.BinPos]
double_S [in Coq.Arith.Div2]
double_var [in Coq.Reals.RIneq]
Dpower [in Coq.Reals.Rpower]
Dx [in Coq.Reals.Rderiv]
Dx_pow_n [in Coq.Reals.Rderiv]
D_in_ext [in Coq.Reals.Rpower]
D_in_imp [in Coq.Reals.Rpower]
D_pow_n [in Coq.Reals.Rderiv]
D_x_no_cond [in Coq.Reals.Ranalysis2]
| 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) |