Global Index

B

bar [library]
bool_hset [lemma, in hlemmas]

C [inductive, in withlpo]
C [inductive, in exercise]
cantor [definition, in ninfty]
CB [lemma, in withpem]
CB [section, in withpem]
CB [lemma, in withlpo]
CB [section, in withlpo]
CB [lemma, in exercise]
CB [section, in exercise]
CB.A [variable, in withlpo]
CB.A [variable, in exercise]
CB.B [variable, in withlpo]
CB.B [variable, in exercise]
CB.CB [section, in withpem]
CB.CB.A [variable, in withpem]
CB.CB.Aset [variable, in withpem]
CB.CB.B [variable, in withpem]
CB.CB.Bset [variable, in withpem]
CB.CB.f [variable, in withpem]
CB.CB.f_inj [variable, in withpem]
CB.CB.g [variable, in withpem]
CB.CB.g_inj [variable, in withpem]
CB.dec_range_g [variable, in withlpo]
CB.dec_range_f [variable, in withlpo]
CB.EM [variable, in exercise]
CB.f [variable, in withlpo]
CB.f [variable, in exercise]
CB.f_inj [variable, in withlpo]
CB.f_inj [variable, in exercise]
CB.g [variable, in withlpo]
CB.g [variable, in exercise]
CB.g_inj [variable, in withlpo]
CB.g_inj [variable, in exercise]
CB.lpo [variable, in withlpo]
CB.PEM [variable, in withpem]
ø [notation, in withlpo]
cond [definition, in bar]
crucial [lemma, in topem]
curry [definition, in prelude]
C_FCω [lemma, in withlpo]
C_i [constructor, in withlpo]
C_i [constructor, in exercise]

decidable [definition, in prelude]
decrange [lemma, in withpem]
decreasing [definition, in ninfty]
dec_C [lemma, in withlpo]
dec_FC_n [lemma, in withlpo]
dec_FC [lemma, in withlpo]
dense [lemma, in ninfty]

EMA_nat_hset [lemma, in bar]
exercise [library]
explicit_CB [lemma, in exercise]

f [definition, in bar]
falseright [lemma, in ninfty]
FC [inductive, in withlpo]
FC_i [constructor, in withlpo]
FCω_C [lemma, in withlpo]
firstzeronat [lemma, in ninfty]
forall_hset [lemma, in hlemmas]
forall_hprop [lemma, in hlemmas]
frompluseqleft [definition, in hlemmas]
frompluseqright [definition, in hlemmas]
f_inv_f_eq [lemma, in withlpo]
f_f_inv_eq [lemma, in withlpo]
f_inv [definition, in withlpo]
f_inv_f_eq [lemma, in exercise]
f_f_inv_eq [lemma, in exercise]
f_inv [definition, in exercise]

g [definition, in bar]
g_inv_g_eq [lemma, in withlpo]
g_g_inv_eq [lemma, in withlpo]
g_inv [definition, in withlpo]
g_inv_g_eq [lemma, in exercise]
g_g_inv_eq [lemma, in exercise]
g_inv [definition, in exercise]

hedberg [lemma, in hlemmas]
hlemmas [library]
hprop [definition, in prelude]
hpropEM [section, in bar]
hpropEM_hprop [lemma, in hlemmas]
hpropEM.A [variable, in bar]
hpropEM.Aprop [variable, in bar]
hpropEM.explicit_hset_CB [variable, in bar]
hprop_hset [lemma, in prelude]
hprop_implies_hset [lemma, in hlemmas]
hset [definition, in prelude]

injective [definition, in prelude]
injective_g [lemma, in bar]
injective_f [lemma, in bar]
injective_succ_infty [lemma, in ninfty]
inverse [definition, in prelude]
inverse_r_r_inv [lemma, in withlpo]
inverse_r_r_inv [lemma, in exercise]
iso [definition, in bar]
isomorphism [definition, in prelude]
isomorphism_r [lemma, in withlpo]
isomorphism_r [lemma, in exercise]
iter [definition, in prelude]

J [definition, in prelude]
J [definition, in hlemmas]

lpo [definition, in prelude]
lpo_true [lemma, in withpem]
lpo_iff_lpo_min [lemma, in prelude]
lpo_min [definition, in prelude]

omniscient [definition, in prelude]

PEM [lemma, in topem]
PEM [section, in topem]
PEM.A [variable, in topem]
PEM.Aprop [variable, in topem]
PEM.hset_CB [variable, in topem]
plus_hprop [lemma, in hlemmas]
plus_hset [lemma, in hlemmas]
pred_succ_eq [lemma, in ninfty]
pred_infty [lemma, in ninfty]
prelude [library]
prod_hprop [lemma, in hlemmas]

r [definition, in withlpo]
r [definition, in bar]
r [definition, in exercise]
range [definition, in prelude]
range_hprop [lemma, in hlemmas]
rinv_r [lemma, in withlpo]
rinv_r [lemma, in exercise]
rtuple [definition, in bar]
r_rinv [lemma, in withlpo]
r_inv [definition, in withlpo]
r_inv [definition, in bar]
r_rinv [lemma, in exercise]
r_inv [definition, in exercise]