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 (18816 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 (644 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 _ other (708 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 (1456 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 (407 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 _ other (8932 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 (422 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 (699 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 (209 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 (203 entries)
Instance 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 (550 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 (338 entries)
Abbreviation 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 (1235 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 (2946 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 (67 entries)

I

i [projection, in i]
I [definition, in I]
I [constructor, in I]
IAF [lemma, in IAF]
IAF_var [lemma, in IAF_var]
id [definition, in id]
id [definition, in id]
ID [definition, in ID]
identity [inductive, in identity]
identity_refl [constructor, in identity_refl]
identity_is_a_congruence.B [variable, in B]
identity_sym [lemma, in identity_sym]
identity_is_a_congruence.f [variable, in f]
identity_rect_r [definition, in identity_rect_r]
identity_is_a_congruence.x [variable, in x]
identity_is_a_congruence [section, in identity_is_a_congruence]
identity_ind_r [definition, in identity_ind_r]
identity_congr [lemma, in identity_congr]
identity_rec_r [definition, in identity_rec_r]
identity_is_a_congruence.y [variable, in y]
identity_is_a_congruence.A [variable, in A]
identity_is_a_congruence.z [variable, in z]
identity_trans [lemma, in identity_trans]
ifb [definition, in ifb]
ifdec [definition, in ifdec]
ifdec_right [lemma, in ifdec_right]
ifdec_left [lemma, in ifdec_left]
iff [definition, in iff]
Iffalse [constructor, in Iffalse]
Iffalse_inv [lemma, in Iffalse_inv]
iff_Reflexive [instance, in iff_Reflexive]
iff_stepl [lemma, in iff_stepl]
iff_and [lemma, in iff_and]
iff_impl_subrelation [instance, in iff_impl_subrelation]
iff_equivalence [instance, in iff_equivalence]
iff_sym [lemma, in iff_sym]
iff_refl [lemma, in iff_refl]
iff_inverse_impl_subrelation [instance, in iff_inverse_impl_subrelation]
iff_iff_iff_impl_morphism [instance, in iff_iff_iff_impl_morphism]
iff_reflect [lemma, in iff_reflect]
iff_Symmetric [instance, in iff_Symmetric]
iff_to_and [lemma, in iff_to_and]
iff_trans [lemma, in iff_trans]
iff_setoid [instance, in iff_setoid]
iff_Transitive [instance, in iff_Transitive]
IfProp [inductive, in IfProp]
IFProp [definition, in IFProp]
IfProp [library]
IfProp_true [lemma, in IfProp_true]
IfProp_false [lemma, in IfProp_false]
IfProp_or [lemma, in IfProp_or]
IfProp_sum [lemma, in IfProp_sum]
Iftrue [constructor, in Iftrue]
Iftrue_inv [lemma, in Iftrue_inv]
if_eqA_refl [lemma, in if_eqA_refl]
if_eqA [instance, in if_eqA]
if_eqA_then [lemma, in if_eqA_then]
if_eqA_rewrite_l [lemma, in if_eqA_rewrite_l]
if_eqA_rewrite_r [lemma, in if_eqA_rewrite_r]
if_eqA_else [lemma, in if_eqA_else]
if_negb [lemma, in if_negb]
IF_then_else [definition, in IF_then_else]
Im [inductive, in Im]
Image [section, in Image]
Image [library]
Image_set_continuous [lemma, in Image_set_continuous]
image_rec [definition, in image_rec]
image_dir [definition, in image_dir]
image_empty [lemma, in image_empty]
Image_set_continuous' [lemma, in Image_set_continuous']
Image.U [variable, in U]
Image.V [variable, in V]
imemo_make [definition, in imemo_make]
imemo_get_correct [lemma, in imemo_get_correct]
imemo_list [definition, in imemo_list]
impl [definition, in impl]
implb [definition, in implb]
imply_and_or [lemma, in imply_and_or]
imply_to_or [lemma, in imply_to_or]
imply_and_or2 [lemma, in imply_and_or2]
imply_to_and [lemma, in imply_to_and]
impl_Reflexive [instance, in impl_Reflexive]
impl_Transitive [instance, in impl_Transitive]
imp_simp [lemma, in imp_simp]
imp_not_l [lemma, in imp_not_l]
Im_def [lemma, in Im_def]
Im_inv [lemma, in Im_inv]
Im_add [lemma, in Im_add]
Im_intro [constructor, in Im_intro]
In [inductive, in In]
In [definition, in In]
In [definition, in In]
In [definition, in In]
In [definition, in In]
In [definition, in In]
IN [module, in IN]
InA [inductive, in InA]
InA_compat [instance, in InA_compat]
InA_cons [lemma, in InA_cons]
InA_app [lemma, in InA_app]
InA_nil [lemma, in InA_nil]
InA_cons_tl [constructor, in InA_cons_tl]
InA_dec [lemma, in InA_dec]
InA_InfA [lemma, in InA_InfA]
InA_alt [lemma, in InA_alt]
InA_eqA [lemma, in InA_eqA]
InA_rev [lemma, in InA_rev]
InA_app_idem [lemma, in InA_app_idem]
InA_double_head [lemma, in InA_double_head]
InA_altdef [lemma, in InA_altdef]
InA_split [lemma, in InA_split]
InA_singleton [lemma, in InA_singleton]
InA_permute_heads [lemma, in InA_permute_heads]
InA_cons_hd [constructor, in InA_cons_hd]
InA_app_iff [lemma, in InA_app_iff]
incl [definition, in incl]
incl [definition, in incl]
inclA [definition, in inclA]
included [definition, in included]
Included [definition, in Included]
Included_Add [lemma, in Included_Add]
Included_Strict_Included [lemma, in Included_Strict_Included]
included_trans [lemma, in included_trans]
Included_Empty [lemma, in Included_Empty]
inclusion [definition, in inclusion]
Inclusion [library]
Inclusion_is_an_order [lemma, in Inclusion_is_an_order]
Inclusion_is_transitive [lemma, in Inclusion_is_transitive]
incl_tran [lemma, in incl_tran]
incl_tl [lemma, in incl_tl]
incl_app [lemma, in incl_app]
incl_cons [lemma, in incl_cons]
incl_soustr [lemma, in incl_soustr]
incl_st_add_soustr [lemma, in incl_st_add_soustr]
incl_refl [lemma, in incl_refl]
incl_right [lemma, in incl_right]
incl_add_x [lemma, in incl_add_x]
incl_appr [lemma, in incl_appr]
incl_nil [lemma, in incl_nil]
incl_st_card_lt [lemma, in incl_st_card_lt]
incl_left [lemma, in incl_left]
incl_card_le [lemma, in incl_card_le]
incl_appl [lemma, in incl_appl]
incl_soustr_add_r [lemma, in incl_soustr_add_r]
incl_add [lemma, in incl_add]
incl_clos_trans [lemma, in incl_clos_trans]
incl_soustr_add_l [lemma, in incl_soustr_add_l]
incl_soustr_in [lemma, in incl_soustr_in]
incr [definition, in incr]
incrbis_aux [definition, in incrbis_aux]
incrbis_aux_equiv [lemma, in incrbis_aux_equiv]
increasing [definition, in increasing]
increasing_decreasing [lemma, in increasing_decreasing]
increasing_decreasing_opp [lemma, in increasing_decreasing_opp]
incr_inv [lemma, in incr_inv]
incr_eqn2 [lemma, in incr_eqn2]
incr_twice [lemma, in incr_twice]
incr_twice_plus_one_firstl [lemma, in incr_twice_plus_one_firstl]
incr_twice_plus_one [lemma, in incr_twice_plus_one]
incr_eqn1 [lemma, in incr_eqn1]
incr_firstr [lemma, in incr_firstr]
ind [projection, in ind]
IndefiniteDescription [library]
IndependenceOfGeneralPremises [definition, in IndependenceOfGeneralPremises]
IndependenceOfGeneralPremises [definition, in IndependenceOfGeneralPremises]
independence_general_premises_right_distr_implication_over_disjunction [lemma, in independence_general_premises_right_distr_implication_over_disjunction]
independence_general_premises_drinker [lemma, in independence_general_premises_drinker]
independence_general_premises_Godel_Dummett [lemma, in independence_general_premises_Godel_Dummett]
index [definition, in index]
index_correct4 [lemma, in index_correct4]
index_correct2 [lemma, in index_correct2]
index_correct3 [lemma, in index_correct3]
index_correct1 [lemma, in index_correct1]
induct [definition, in induct]
induction_gtof1 [lemma, in induction_gtof1]
induction_gtof2 [lemma, in induction_gtof2]
induction_ltof1 [lemma, in induction_ltof1]
induction_ltof2 [lemma, in induction_ltof2]
ind_0_1_SS [lemma, in ind_0_1_SS]
InfA [abbreviation, in InfA]
InfA_alt [lemma, in InfA_alt]
InfA_ltA [lemma, in InfA_ltA]
InfA_compat [instance, in InfA_compat]
InfA_eqA [lemma, in InfA_eqA]
InfA_app [lemma, in InfA_app]
Infinite_sets.U [variable, in U]
infinite_sum [definition, in infinite_sum]
Infinite_sets [section, in Infinite_sets]
Infinite_sets.V [variable, in V]
Infinite_sets [library]
infinit_sum [abbreviation, in infinit_sum]
InfoTyp [module, in InfoTyp]
InfoTyp.t [axiom, in t]
infty [constructor, in infty]
Inhabited [inductive, in Inhabited]
inhabited [abbreviation, in inhabited]
inhabited [abbreviation, in inhabited]
inhabited [abbreviation, in inhabited]
inhabited [inductive, in inhabited]
Inhabited_Setminus [lemma, in Inhabited_Setminus]
Inhabited_not_empty [lemma, in Inhabited_not_empty]
Inhabited_intro [constructor, in Inhabited_intro]
Inhabited_add [lemma, in Inhabited_add]
inhabits [constructor, in inhabits]
inh_card_gt_O [lemma, in inh_card_gt_O]
Init [library]
injective [definition, in injective]
injective_projections [lemma, in injective_projections]
injective_preserves_cardinal [lemma, in injective_preserves_cardinal]
inject_Z_opp [lemma, in inject_Z_opp]
inject_Z_plus [lemma, in inject_Z_plus]
inject_Z [definition, in inject_Z]
inject_Z_injective [lemma, in inject_Z_injective]
inject_Z_mult [lemma, in inject_Z_mult]
injs [definition, in injs]
inj_ge_iff [abbreviation, in inj_ge_iff]
inj_max [abbreviation, in inj_max]
inj_lt [definition, in inj_lt]
inj_lt_rev [abbreviation, in inj_lt_rev]
inj_minus1 [abbreviation, in inj_minus1]
inj_mult [abbreviation, in inj_mult]
inj_pairT2_refl [lemma, in inj_pairT2_refl]
inj_eq_rev [abbreviation, in inj_eq_rev]
inj_gt_iff [abbreviation, in inj_gt_iff]
inj_gt_rev [abbreviation, in inj_gt_rev]
Inj_dep_pair [definition, in Inj_dep_pair]
inj_ge_rev [abbreviation, in inj_ge_rev]
inj_plus [abbreviation, in inj_plus]
inj_0 [abbreviation, in inj_0]
inj_ge [definition, in inj_ge]
inj_compare [abbreviation, in inj_compare]
inj_right_pair [lemma, in inj_right_pair]
inj_eq [definition, in inj_eq]
inj_le_rev [abbreviation, in inj_le_rev]
inj_min [abbreviation, in inj_min]
inj_minus2 [lemma, in inj_minus2]
inj_eq_iff [abbreviation, in inj_eq_iff]
inj_le [definition, in inj_le]
inj_S [abbreviation, in inj_S]
inj_pair2_eq_dec [lemma, in inj_pair2_eq_dec]
inj_le_iff [abbreviation, in inj_le_iff]
inj_Zabs_nat [abbreviation, in inj_Zabs_nat]
inj_lt_iff [abbreviation, in inj_lt_iff]
Inj_dep_pairS [abbreviation, in Inj_dep_pairS]
inj_gt [definition, in inj_gt]
inj_minus [abbreviation, in inj_minus]
Inj_dep_pairT [abbreviation, in Inj_dep_pairT]
inj_neq [lemma, in inj_neq]
inl [constructor, in inl]
inleft [constructor, in inleft]
inr [constructor, in inr]
INR [definition, in INR]
inright [constructor, in inright]
INR_fact_neq_0 [lemma, in INR_fact_neq_0]
INR_pos [abbreviation, in INR_pos]
INR_IZR_INZ [lemma, in INR_IZR_INZ]
INR_lt_1 [abbreviation, in INR_lt_1]
INR_lt [lemma, in INR_lt]
INR_fact_lt_0 [lemma, in INR_fact_lt_0]
INR_not_0 [lemma, in INR_not_0]
INR_eq [lemma, in INR_eq]
INR_le [lemma, in INR_le]
insert [lemma, in insert]
insert [definition, in insert]
insert_spec [inductive, in insert_spec]
insert_exist [constructor, in insert_exist]
inser_trans_R [lemma, in inser_trans_R]
inst [lemma, in inst]
Int [module, in Int]
Int [library]
Integers [inductive, in Integers]
Integers [library]
Integers_infinite [lemma, in Integers_infinite]
Integers_sect [section, in Integers_sect]
Integers_defn [constructor, in Integers_defn]
Integers_has_no_ub [lemma, in Integers_has_no_ub]
Integration [library]
interior [definition, in interior]
interior_P1 [lemma, in interior_P1]
interior_P3 [lemma, in interior_P3]
interior_P2 [lemma, in interior_P2]
interp_carry [definition, in interp_carry]
Intersection [inductive, in Intersection]
intersection_vide_finite_in [definition, in intersection_vide_finite_in]
Intersection_decreases_l [lemma, in Intersection_decreases_l]
Intersection_decreases_r [lemma, in Intersection_decreases_r]
Intersection_is_Glb [lemma, in Intersection_is_Glb]
intersection_family [definition, in intersection_family]
Intersection_intro [constructor, in Intersection_intro]
Intersection_commutative [lemma, in Intersection_commutative]
intersection_domain [definition, in intersection_domain]
Intersection_preserves_finite [lemma, in Intersection_preserves_finite]
Intersection_inv [lemma, in Intersection_inv]
Intersection_maximal [lemma, in Intersection_maximal]
intersection_vide_in [definition, in intersection_vide_in]
IntMake [module, in IntMake]
IntMake [module, in IntMake]
IntMake_ord.cons_Cmp [lemma, in cons_Cmp]
IntMake_ord.eq_refl [lemma, in eq_refl]
IntMake_ord.LO [module, in IntMake_ord.LO]
IntMake_ord.cardinal_e_2 [definition, in cardinal_e_2]
IntMake_ord.MD [module, in IntMake_ord.MD]
IntMake_ord.eq_seq [lemma, in eq_seq]
IntMake_ord.cardinal_e [definition, in cardinal_e]
IntMake_ord.eq_1 [lemma, in eq_1]
IntMake_ord.seq [definition, in seq]
IntMake_ord.compare_Cmp [lemma, in compare_Cmp]
IntMake_ord.t [definition, in t]
IntMake_ord.elements [definition, in elements]
IntMake_ord.Cmp [definition, in Cmp]
IntMake_ord.compare [definition, in compare]
IntMake_ord.eq_2 [lemma, in eq_2]
IntMake_ord.cmp [definition, in cmp]
IntMake_ord.selements [definition, in selements]
IntMake_ord.eq_sym [lemma, in eq_sym]
IntMake_ord.lt_not_eq [lemma, in lt_not_eq]
IntMake_ord.Data [module, in IntMake_ord.Data]
IntMake_ord.lt_trans [lemma, in lt_trans]
IntMake_ord [module, in IntMake_ord]
IntMake_ord.eq_trans [lemma, in eq_trans]
IntMake_ord.slt [definition, in slt]
IntMake_ord.MapS [module, in IntMake_ord.MapS]
IntMake_ord.lt_slt [lemma, in lt_slt]
IntMake_ord.cons_cardinal_e [lemma, in cons_cardinal_e]
IntMake_ord.lt [definition, in lt]
IntMake_ord.eq [definition, in eq]
IntMake_ord.compare_aux_Cmp [lemma, in compare_aux_Cmp]
IntMake.add [definition, in add]
IntMake.add_1 [lemma, in add_1]
IntMake.add_2 [lemma, in add_2]
IntMake.add_3 [lemma, in add_3]
IntMake.AvlProofs [module, in IntMake.AvlProofs]
IntMake.Bbst [constructor, in Bbst]
IntMake.bbst [record, in bbst]
IntMake.cardinal [definition, in cardinal]
IntMake.cardinal_1 [lemma, in cardinal_1]
IntMake.E [module, in IntMake.E]
IntMake.elements [definition, in elements]
IntMake.elements_3w [lemma, in elements_3w]
IntMake.elements_3 [lemma, in elements_3]
IntMake.elements_1 [lemma, in elements_1]
IntMake.elements_2 [lemma, in elements_2]
IntMake.Elt [section, in Elt]
IntMake.Elt.elt [variable, in elt]
IntMake.Elt.elt' [variable, in elt']
IntMake.Elt.elt'' [variable, in elt'']
IntMake.empty [definition, in empty]
IntMake.Empty [definition, in Empty]
IntMake.empty_1 [lemma, in empty_1]
IntMake.equal [definition, in equal]
IntMake.Equal [definition, in Equal]
IntMake.equal_2 [lemma, in equal_2]
IntMake.equal_1 [lemma, in equal_1]
IntMake.Equiv [definition, in Equiv]
IntMake.Equivb [definition, in Equivb]
IntMake.Equivb_Equivb [lemma, in Equivb_Equivb]
IntMake.eq_key_elt [definition, in eq_key_elt]
IntMake.eq_key [definition, in eq_key]
IntMake.find [definition, in find]
IntMake.find_2 [lemma, in find_2]
IntMake.find_1 [lemma, in find_1]
IntMake.fold [definition, in fold]
IntMake.fold_1 [lemma, in fold_1]
IntMake.In [definition, in In]
IntMake.is_avl [projection, in is_avl]
IntMake.is_empty_1 [lemma, in is_empty_1]
IntMake.is_bst [projection, in is_bst]
IntMake.is_empty [definition, in is_empty]
IntMake.is_empty_2 [lemma, in is_empty_2]
IntMake.key [definition, in key]
IntMake.lt_key [definition, in lt_key]
IntMake.map [definition, in map]
IntMake.mapi [definition, in mapi]
IntMake.mapi_2 [lemma, in mapi_2]
IntMake.mapi_1 [lemma, in mapi_1]
IntMake.MapsTo [definition, in MapsTo]
IntMake.MapsTo_1 [lemma, in MapsTo_1]
IntMake.map_1 [lemma, in map_1]
IntMake.map_2 [lemma, in map_2]
IntMake.map2 [definition, in map2]
IntMake.map2_2 [lemma, in map2_2]
IntMake.map2_1 [lemma, in map2_1]
IntMake.mem [definition, in mem]
IntMake.mem_1 [lemma, in mem_1]
IntMake.mem_2 [lemma, in mem_2]
IntMake.MSet [module, in IntMake.MSet]
IntMake.remove [definition, in remove]
IntMake.remove_2 [lemma, in remove_2]
IntMake.remove_1 [lemma, in remove_1]
IntMake.remove_3 [lemma, in remove_3]
IntMake.t [definition, in t]
IntMake.this [projection, in this]
IntMake.X' [module, in IntMake.X']
Int_part_INR [lemma, in Int_part_INR]
Int_SF [definition, in Int_SF]
Int_part [definition, in Int_part]
Int.eq_dec [axiom, in eq_dec]
Int.ge_lt_dec [axiom, in ge_lt_dec]
Int.gt_le_dec [axiom, in gt_le_dec]
Int.int [definition, in int]
Int.i2z [axiom, in i2z]
Int.i2z_2 [axiom, in i2z_2]
Int.i2z_mult [axiom, in i2z_mult]
Int.i2z_max [axiom, in i2z_max]
Int.i2z_eq [axiom, in i2z_eq]
Int.i2z_1 [axiom, in i2z_1]
Int.i2z_plus [axiom, in i2z_plus]
Int.i2z_0 [axiom, in i2z_0]
Int.i2z_minus [axiom, in i2z_minus]
Int.i2z_3 [axiom, in i2z_3]
Int.i2z_opp [axiom, in i2z_opp]
Int.max [axiom, in max]
Int.minus [axiom, in minus]
Int.mult [axiom, in mult]
Int.opp [axiom, in opp]
Int.plus [axiom, in plus]
Int.t [axiom, in t]
Int._2 [axiom, in _2]
Int._0 [axiom, in _0]
Int._1 [axiom, in _1]
Int._3 [axiom, in _3]
_ == _ (Int_scope) [notation, in :Int_scope:x_'=='_x]
_ < _ <= _ (Int_scope) [notation, in :Int_scope:x_'<'_x_'<='_x]
_ <= _ < _ (Int_scope) [notation, in :Int_scope:x_'<='_x_'<'_x]
2 (Int_scope) [notation, in :Int_scope:'2']
0 (Int_scope) [notation, in :Int_scope:'0']
_ <= _ (Int_scope) [notation, in :Int_scope:x_'<='_x]
_ - _ (Int_scope) [notation, in :Int_scope:x_'-'_x]
_ >= _ (Int_scope) [notation, in :Int_scope:x_'>='_x]
_ + _ (Int_scope) [notation, in :Int_scope:x_'+'_x]
3 (Int_scope) [notation, in :Int_scope:'3']
_ < _ (Int_scope) [notation, in :Int_scope:x_'<'_x]
1 (Int_scope) [notation, in :Int_scope:'1']
- _ (Int_scope) [notation, in :Int_scope:'-'_x]
_ * _ (Int_scope) [notation, in :Int_scope:x_'*'_x]
_ < _ < _ (Int_scope) [notation, in :Int_scope:x_'<'_x_'<'_x]
_ > _ (Int_scope) [notation, in :Int_scope:x_'>'_x]
_ <= _ <= _ (Int_scope) [notation, in :Int_scope:x_'<='_x_'<='_x]
int31 [inductive, in int31]
Int31 [library]
Int31Cyclic [module, in Int31Cyclic]
Int31Cyclic.ops [definition, in ops]
Int31Cyclic.specs [definition, in specs]
Int31Cyclic.t [definition, in t]
Int31Ring [lemma, in Int31Ring]
Int31ring [module, in Int31ring]
Int31_canonic [lemma, in Int31_canonic]
int31_ind_sneakl [lemma, in int31_ind_sneakl]
int31_ind_twice [lemma, in int31_ind_twice]
[| _ |] [notation, in ::'[|'_x_'|]']
[|| _ ||] [notation, in ::'[||'_x_'||]']
Int31_Specs [section, in Int31_Specs]
int31_ops [instance, in int31_ops]
[-| _ |] [notation, in ::'[-|'_x_'|]']
int31_specs [instance, in int31_specs]
[+| _ |] [notation, in ::'[+|'_x_'|]']
inv [projection, in inv]
Inverse [module, in Inverse]
inverse [abbreviation, in inverse]
Inverse_Image.B [variable, in B]
inverse_respectful [lemma, in inverse_respectful]
inverse_pointwise_relation [lemma, in inverse_pointwise_relation]
Inverse_Image [section, in Inverse_Image]
Inverse_Image.R [variable, in R]
Inverse_Image.f [variable, in f]
inverse_image_of_equivalence [lemma, in inverse_image_of_equivalence]
Inverse_Image.Rof [variable, in Rof]
Inverse_Image.F [variable, in F]
inverse_arrow [lemma, in inverse_arrow]
inverse_atom [lemma, in inverse_atom]
Inverse_Image.RoF [variable, in RoF]
inverse_image_of_eq [lemma, in inverse_image_of_eq]
Inverse_Image.A [variable, in A]
Inverse_Image [library]
Inverse.Hom12 [module, in Inverse.Hom12]
Inverse.Hom21 [module, in Inverse.Hom21]
Inverse.h12 [abbreviation, in h12]
Inverse.h21 [abbreviation, in h21]
Inverse.inverse_nat_iso [lemma, in inverse_nat_iso]
Inverse.NBasePropMod1 [module, in Inverse.NBasePropMod1]
_ == _ [notation, in ::x_'=='_x]
inverse1 [lemma, in inverse1]
inverse2 [lemma, in inverse2]
invert_heap [lemma, in invert_heap]
inv_lt_rel [definition, in inv_lt_rel]
inv_fct [definition, in inv_fct]
inv_before_witness [definition, in inv_before_witness]
inv2 [projection, in inv2]
in_left [abbreviation, in in_left]
In_rev [abbreviation, in In_rev]
in_right [abbreviation, in in_right]
in_eq [lemma, in in_eq]
In_split [abbreviation, in In_split]
in_combine_l [lemma, in in_combine_l]
in_int_lt [lemma, in in_int_lt]
in_nil [lemma, in in_nil]
in_int_intro [lemma, in in_int_intro]
in_map [lemma, in in_map]
In_cons_tl [constructor, in In_cons_tl]
in_int [definition, in in_int]
in_int [definition, in in_int]
in_inv [lemma, in in_inv]
in_rev [lemma, in in_rev]
in_cons [lemma, in in_cons]
in_int_exists [lemma, in in_int_exists]
in_prod [lemma, in in_prod]
In_InA [lemma, in In_InA]
in_int_p_Sq [lemma, in in_int_p_Sq]
in_dec [lemma, in in_dec]
in_or_app [lemma, in in_or_app]
in_split [lemma, in in_split]
In_cons_hd [constructor, in In_cons_hd]
in_prod_aux [lemma, in in_prod_aux]
in_split_l [lemma, in in_split_l]
in_combine_r [lemma, in in_combine_r]
in_app_or [lemma, in in_app_or]
In_InfA [lemma, in In_InfA]
in_flat_map [lemma, in in_flat_map]
In_singleton [constructor, in In_singleton]
in_int_Sp_q [lemma, in in_int_Sp_q]
in_map_iff [lemma, in in_map_iff]
in_int_S [lemma, in in_int_S]
in_app_iff [lemma, in in_app_iff]
in_int_between [lemma, in in_int_between]
in_split_r [lemma, in in_split_r]
In_dec [abbreviation, in In_dec]
In_Image_elim [lemma, in In_Image_elim]
in_prod_iff [lemma, in in_prod_iff]
IN.Empty [definition, in Empty]
IN.Equal [definition, in Equal]
IN.In [axiom, in In]
IN.In_compat [instance, in In_compat]
IN.t [axiom, in t]
iota [definition, in iota]
iota [definition, in iota]
IotaStatement [abbreviation, in IotaStatement]
IotaStatement_on [definition, in IotaStatement_on]
iota_imp_constructive_definite_description [lemma, in iota_imp_constructive_definite_description]
iota_statement [lemma, in iota_statement]
iota_spec [definition, in iota_spec]
iota_spec [definition, in iota_spec]
Irreflexive [record, in Irreflexive]
Irreflexive [inductive, in Irreflexive]
irreflexivity [projection, in irreflexivity]
irreflexivity [constructor, in irreflexivity]
IsAddSubMul [module, in IsAddSubMul]
IsAddSubMul.add_succ_l [axiom, in add_succ_l]
IsAddSubMul.add_0_l [axiom, in add_0_l]
IsAddSubMul.add_wd [instance, in add_wd]
IsAddSubMul.mul_succ_l [axiom, in mul_succ_l]
IsAddSubMul.mul_0_l [axiom, in mul_0_l]
IsAddSubMul.mul_wd [instance, in mul_wd]
IsAddSubMul.sub_wd [instance, in sub_wd]
IsAddSubMul.sub_succ_r [axiom, in sub_succ_r]
IsAddSubMul.sub_0_r [axiom, in sub_0_r]
IsEq [module, in IsEq]
IsEqOrig [module, in IsEqOrig]
IsEqOrig.eq_refl [axiom, in eq_refl]
IsEqOrig.eq_sym [axiom, in eq_sym]
IsEqOrig.eq_trans [axiom, in eq_trans]
Isequence [section, in Isequence]
Isequence.An [variable, in An]
IsEq.eq_equiv [instance, in eq_equiv]
IsNeg [abbreviation, in IsNeg]
IsNul [abbreviation, in IsNul]
IsNZDomain [module, in IsNZDomain]
IsNZDomain.bi_induction [axiom, in bi_induction]
IsNZDomain.pred_succ [axiom, in pred_succ]
IsNZDomain.pred_wd [instance, in pred_wd]
IsNZDomain.succ_wd [instance, in succ_wd]
IsNZOrd [module, in IsNZOrd]
IsNZOrd.lt_irrefl [axiom, in lt_irrefl]
IsNZOrd.lt_eq_cases [axiom, in lt_eq_cases]
IsNZOrd.lt_succ_r [axiom, in lt_succ_r]
IsNZOrd.lt_wd [instance, in lt_wd]
isometric_rotation_0 [lemma, in isometric_rotation_0]
isometric_trans_rot [lemma, in isometric_trans_rot]
isometric_translation [lemma, in isometric_translation]
isometric_rot_trans [lemma, in isometric_rot_trans]
isometric_rotation [lemma, in isometric_rotation]
Isomorphism [module, in Isomorphism]
Isomorphism.Hom12 [module, in Isomorphism.Hom12]
Isomorphism.Hom21 [module, in Isomorphism.Hom21]
Isomorphism.h12 [abbreviation, in h12]
Isomorphism.h21 [abbreviation, in h21]
Isomorphism.Inverse12 [module, in Isomorphism.Inverse12]
Isomorphism.Inverse21 [module, in Isomorphism.Inverse21]
Isomorphism.isomorphism [definition, in isomorphism]
Isomorphism.iso_nat_iso [lemma, in iso_nat_iso]
IsOneTwo [module, in IsOneTwo]
IsOneTwo.one_succ [axiom, in one_succ]
IsOneTwo.two_succ [axiom, in two_succ]
IsOpp [module, in IsOpp]
IsOpp.opp_succ [axiom, in opp_succ]
IsOpp.opp_wd [instance, in opp_wd]
IsOpp.opp_0 [axiom, in opp_0]
IsPos [abbreviation, in IsPos]
IsStepFun [definition, in IsStepFun]
IsStrOrder [module, in IsStrOrder]
IsStrOrder.lt_compat [instance, in lt_compat]
IsStrOrder.lt_strorder [instance, in lt_strorder]
IsSucc [definition, in IsSucc]
iszero [definition, in iszero]
iszero_eq0 [lemma, in iszero_eq0]
iszero_not_eq0 [lemma, in iszero_not_eq0]
is_heap [inductive, in is_heap]
Is_true [definition, in Is_true]
is_upper_bound [definition, in is_upper_bound]
is_even [definition, in is_even]
is_lub [definition, in is_lub]
is_one_one [lemma, in is_one_one]
is_heap_rect [lemma, in is_heap_rect]
Is_power_or [lemma, in Is_power_or]
Is_true_eq_true [lemma, in Is_true_eq_true]
is_lub_u [lemma, in is_lub_u]
is_subdivision [definition, in is_subdivision]
is_heap_rec [lemma, in is_heap_rec]
is_subrelation [projection, in is_subrelation]
is_subrelation [constructor, in is_subrelation]
is_true [definition, in is_true]
Is_power_correct [lemma, in Is_power_correct]
is_one [definition, in is_one]
Is_true_eq_left [lemma, in Is_true_eq_left]
Is_true_eq_true2 [abbreviation, in Is_true_eq_true2]
is_eq_true [constructor, in is_eq_true]
Is_true_eq_right [lemma, in Is_true_eq_right]
is_eq [definition, in is_eq]
Is_power [definition, in Is_power]
iter [abbreviation, in iter]
ITERATORS [section, in ITERATORS]
iter_nat_of_Z [lemma, in iter_nat_of_Z]
iter_pos_invariant [abbreviation, in iter_pos_invariant]
iter_pos_swap_gen [abbreviation, in iter_pos_swap_gen]
iter_pos_succ [abbreviation, in iter_pos_succ]
iter_nat_of_P [abbreviation, in iter_nat_of_P]
iter_pos_plus [abbreviation, in iter_pos_plus]
iter_pos [abbreviation, in iter_pos]
iter_nat_plus [abbreviation, in iter_nat_plus]
iter_int31 [definition, in iter_int31]
iter_int31_iter_nat [lemma, in iter_int31_iter_nat]
iter_nat_invariant [abbreviation, in iter_nat_invariant]
iter_nat [abbreviation, in iter_nat]
iter_pos_swap [abbreviation, in iter_pos_swap]
iter31_sqrt [definition, in iter31_sqrt]
iter31_sqrt_correct [lemma, in iter31_sqrt_correct]
iter312_sqrt [definition, in iter312_sqrt]
iter312_sqrt_correct [lemma, in iter312_sqrt_correct]
IVT [lemma, in IVT]
IVT_interv_prelim1 [lemma, in IVT_interv_prelim1]
IVT_interv_prelim0 [lemma, in IVT_interv_prelim0]
IVT_interv [lemma, in IVT_interv]
IVT_cor [lemma, in IVT_cor]
IZN [lemma, in IZN]
IZN_var [lemma, in IZN_var]
IZR [definition, in IZR]
IZR_lt [lemma, in IZR_lt]
IZR_ge [lemma, in IZR_ge]
IZR_le [lemma, in IZR_le]
IZR_nz [lemma, in IZR_nz]
IZR_neq [lemma, in IZR_neq]
IZR_eq [lemma, in IZR_eq]
i2 [projection, in i2]
i2l [definition, in i2l]
i2l_sneakl [lemma, in i2l_sneakl]
i2l_length [lemma, in i2l_length]
i2l_l2i [lemma, in i2l_l2i]
i2l_nshiftl [lemma, in i2l_nshiftl]
i2l_sneakr [lemma, in i2l_sneakr]
I31 [constructor, in I31]



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 (18816 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 (644 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 _ other (708 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 (1456 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 (407 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 _ other (8932 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 (422 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 (699 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 (209 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 (203 entries)
Instance 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 (550 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 (338 entries)
Abbreviation 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 (1235 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 (2946 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 (67 entries)