| 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 | (394 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 | (289 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 | (3 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 | (5 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 | (81 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 | (9 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 | (7 entries) |
Global Index
A
a [definition, in g_proof]AC [definition, in g_proof]
antisymmetric [definition, in b_functions]
app [definition, in b_functions]
app_inj [lemma, in b_functions]
app_sur [lemma, in b_functions]
app_eq [lemma, in b_functions]
app_cor2 [lemma, in b_functions]
app_cor1 [lemma, in b_functions]
app_cor [lemma, in b_functions]
asymmetric [definition, in b_functions]
asym_irref [lemma, in b_functions]
a_ex [lemma, in g_proof]
a_inf [lemma, in g_proof]
a_ordinal [lemma, in g_proof]
a_subs [lemma, in g_proof]
a_el [lemma, in g_proof]
a_R [lemma, in g_proof]
a_least [lemma, in g_proof]
a_sets [library]
B
bijection [definition, in b_functions]bijective [definition, in b_functions]
bijec_empty [lemma, in b_functions]
bij_app [lemma, in b_functions]
bran [definition, in g_proof]
B_tao [lemma, in e_recursion]
B_tao_app2 [lemma, in e_recursion]
B_tao_TU [lemma, in e_recursion]
B_tao_app1 [lemma, in e_recursion]
b_functions [library]
C
comp [definition, in e_recursion]comp [definition, in b_functions]
compB [definition, in e_recursion]
comp_exists [lemma, in e_recursion]
comp_agree [lemma, in e_recursion]
comp_res_eq [lemma, in e_recursion]
comp_linear [lemma, in e_recursion]
comp_subs [lemma, in e_recursion]
comp_unique [lemma, in e_recursion]
comp_eq [lemma, in e_recursion]
comp_res [lemma, in e_recursion]
comp_bij [lemma, in b_functions]
comp_inj [lemma, in b_functions]
comp_sur [lemma, in b_functions]
comp_app [lemma, in b_functions]
comp_fun [lemma, in b_functions]
comp_fct [lemma, in b_functions]
comp_tot [lemma, in b_functions]
comp_rel [lemma, in b_functions]
c_ordinals [library]
D
dom [definition, in b_functions]doms [definition, in g_proof]
doms_str [lemma, in g_proof]
doms_ordinal [lemma, in g_proof]
d_isomorphy [library]
E
elorder [definition, in c_ordinals]elorder_linear [lemma, in c_ordinals]
elorder_worder [lemma, in c_ordinals]
elorder_trans [lemma, in c_ordinals]
elorder_succ [lemma, in c_ordinals]
elorder_subs [lemma, in c_ordinals]
elorder_res [lemma, in c_ordinals]
elorder_element [lemma, in c_ordinals]
elorder_el' [lemma, in c_ordinals]
elorder_el [lemma, in c_ordinals]
el_su [lemma, in c_ordinals]
el_succ_subs [lemma, in c_ordinals]
el_succ [lemma, in c_ordinals]
empty_ordinal [lemma, in c_ordinals]
equi [definition, in b_functions]
equivalence [definition, in b_functions]
equi_trans [lemma, in b_functions]
equi_com [lemma, in b_functions]
equi_subs [lemma, in b_functions]
equi_empty [lemma, in b_functions]
exhausted [lemma, in g_proof]
e_recursion [library]
F
f [definition, in e_recursion]F [definition, in e_recursion]
f [definition, in g_proof]
fa_surjective [lemma, in g_proof]
fa_ran [lemma, in g_proof]
fa_fun [lemma, in g_proof]
fa_M [lemma, in g_proof]
ff [lemma, in g_proof]
fg [lemma, in g_proof]
field [definition, in b_functions]
fset [definition, in e_recursion]
function [definition, in b_functions]
functional [definition, in b_functions]
fun_subs_res [lemma, in b_functions]
fun_subs [lemma, in b_functions]
fun_res_eq [lemma, in b_functions]
fun_eq_gen [lemma, in b_functions]
fun_eq [lemma, in b_functions]
fun_subs2 [lemma, in b_functions]
fun_subs1 [lemma, in b_functions]
fun_ran [lemma, in b_functions]
fun_shrink [lemma, in b_functions]
fun_appel [lemma, in b_functions]
fun_app [lemma, in b_functions]
fun_expand [lemma, in b_functions]
fun_step [lemma, in b_functions]
fun_step_fun [lemma, in b_functions]
fun_step_tot [lemma, in b_functions]
fun_step_rel [lemma, in b_functions]
fun_ran_subs [lemma, in b_functions]
fun_el_ran [lemma, in b_functions]
fun_el_dom [lemma, in b_functions]
fun_el2 [lemma, in b_functions]
fun_el1 [lemma, in b_functions]
fun_pair2 [lemma, in b_functions]
fun_pair1 [lemma, in b_functions]
fun_pi2 [lemma, in b_functions]
fun_pi1 [lemma, in b_functions]
fun_product [lemma, in b_functions]
fun_pair [lemma, in b_functions]
fun_pi [lemma, in b_functions]
f_unique [lemma, in e_recursion]
f_rec [lemma, in e_recursion]
f_funB [lemma, in e_recursion]
f_fun [lemma, in e_recursion]
F_eq2 [lemma, in e_recursion]
F_fun [lemma, in e_recursion]
f_inj [lemma, in g_proof]
f_seq [lemma, in g_proof]
f_rel [lemma, in g_proof]
f_hartogs [library]
G
G [definition, in e_recursion]g [definition, in g_proof]
g_proof [library]
g2f [lemma, in g_proof]
H
h [definition, in f_hartogs]hartogs [lemma, in f_hartogs]
hartogs_ordinal [lemma, in f_hartogs]
hartogs_el [lemma, in f_hartogs]
h_ordiso [lemma, in f_hartogs]
I
id [definition, in b_functions]id_fun [lemma, in b_functions]
id_rel [lemma, in b_functions]
id_equal [lemma, in b_functions]
id_app [lemma, in b_functions]
id_bijection [lemma, in b_functions]
image [definition, in b_functions]
image_oisomorph2 [lemma, in d_isomorphy]
image_oisomorph [lemma, in d_isomorphy]
image_ran [lemma, in b_functions]
image_bij [lemma, in b_functions]
image_bijection [lemma, in b_functions]
image_sur [lemma, in b_functions]
image_tot [lemma, in b_functions]
image_rel [lemma, in b_functions]
image_res [lemma, in b_functions]
image_el [lemma, in b_functions]
image_empty [lemma, in b_functions]
image_subs [lemma, in b_functions]
im_el [lemma, in b_functions]
im_cor [lemma, in b_functions]
inj [definition, in b_functions]
injection [definition, in b_functions]
injective [definition, in b_functions]
inverse [definition, in b_functions]
inv_idem [lemma, in b_functions]
inv_element [lemma, in b_functions]
inv_el [lemma, in b_functions]
inv_bij [lemma, in b_functions]
inv_el2 [lemma, in b_functions]
inv_el1 [lemma, in b_functions]
inv1 [lemma, in b_functions]
inv2 [lemma, in b_functions]
iorder [definition, in c_ordinals]
iorder_wf [lemma, in c_ordinals]
iorder_lin [lemma, in c_ordinals]
iorder_trans [lemma, in c_ordinals]
iorder_asym [lemma, in c_ordinals]
iorder_dom2 [lemma, in c_ordinals]
iorder_dom1 [lemma, in c_ordinals]
iorder_el' [lemma, in c_ordinals]
iorder_el [lemma, in c_ordinals]
irreflexive [definition, in b_functions]
irref_asym [lemma, in b_functions]
iseg [definition, in d_isomorphy]
iseg_oisoeq [lemma, in e_recursion]
iseg_res [lemma, in d_isomorphy]
iseg_ordinal [lemma, in d_isomorphy]
iseg_ordinal_eq [lemma, in d_isomorphy]
iseg_equal [lemma, in d_isomorphy]
iseg_worder [lemma, in d_isomorphy]
iseg_eq [lemma, in d_isomorphy]
iseg_subs [lemma, in d_isomorphy]
iseg_el [lemma, in d_isomorphy]
iseg_nel [lemma, in d_isomorphy]
L
lam [definition, in b_functions]lam_inj [lemma, in b_functions]
lam_sur [lemma, in b_functions]
lam_subs [lemma, in b_functions]
lam_app2 [lemma, in b_functions]
lam_app [lemma, in b_functions]
lam_fun [lemma, in b_functions]
lam_el [lemma, in b_functions]
least [definition, in b_functions]
linear [definition, in b_functions]
lordering [definition, in b_functions]
O
oiseg [definition, in d_isomorphy]oiseg_lin [lemma, in d_isomorphy]
oiseg_eq [lemma, in d_isomorphy]
oiso [definition, in d_isomorphy]
oisomorphism [definition, in d_isomorphy]
oiso_eq [lemma, in d_isomorphy]
oiso_images [lemma, in d_isomorphy]
oiso_iseg [lemma, in d_isomorphy]
oiso_trans [lemma, in d_isomorphy]
oiso_com [lemma, in d_isomorphy]
oiso_ref [lemma, in d_isomorphy]
Olemrez [lemma, in g_proof]
one [definition, in c_ordinals]
opres [definition, in d_isomorphy]
ord [definition, in f_hartogs]
ordertype [definition, in f_hartogs]
ordinal [definition, in c_ordinals]
ordinals_sosubset [lemma, in c_ordinals]
ordinal_iso [lemma, in e_recursion]
ordinal_ordiso [lemma, in e_recursion]
ordinal_wf [lemma, in e_recursion]
ordinal_wo [lemma, in c_ordinals]
ordinal_iorder [lemma, in c_ordinals]
ordinal_noset [lemma, in c_ordinals]
ordinal_bunion [lemma, in c_ordinals]
ordinal_union [lemma, in c_ordinals]
ordinal_set [lemma, in c_ordinals]
ordinal_set_wf [lemma, in c_ordinals]
ordinal_set_trans [lemma, in c_ordinals]
ordinal_set_asym [lemma, in c_ordinals]
ordinal_wfounded [lemma, in c_ordinals]
ordinal_linear [lemma, in c_ordinals]
ordinal_inter [lemma, in c_ordinals]
ordinal_anti [lemma, in c_ordinals]
ordinal_trans [lemma, in c_ordinals]
ordinal_nel [lemma, in c_ordinals]
ordinal_subs [lemma, in c_ordinals]
ordinal_eltrans [lemma, in c_ordinals]
ordinal_el [lemma, in c_ordinals]
ordiso [definition, in d_isomorphy]
ordiso_eq [lemma, in e_recursion]
ordiso_trans [lemma, in d_isomorphy]
ord_order2 [lemma, in f_hartogs]
ord_order1 [lemma, in f_hartogs]
ord_norder2 [lemma, in f_hartogs]
ord_norder1 [lemma, in f_hartogs]
ord_unique [lemma, in f_hartogs]
ord_ordinal [lemma, in f_hartogs]
ord_otype [lemma, in f_hartogs]
otype_unique [lemma, in f_hartogs]
otype_ordiso [lemma, in f_hartogs]
otype_ordinal [lemma, in f_hartogs]
otype_stransitive [lemma, in f_hartogs]
otype_elord [lemma, in f_hartogs]
otype_eliso [lemma, in f_hartogs]
otype_empty [lemma, in f_hartogs]
P
pow_nempty [lemma, in g_proof]pow_subs [lemma, in g_proof]
pow' [definition, in g_proof]
proof [section, in g_proof]
proof.c [variable, in g_proof]
proof.choice [variable, in g_proof]
proof.M [variable, in g_proof]
R
R [definition, in g_proof]ran [definition, in b_functions]
ran_subs [lemma, in g_proof]
rec [lemma, in g_proof]
reflexive [definition, in b_functions]
relation [definition, in b_functions]
relations [definition, in f_hartogs]
relres_wf [lemma, in b_functions]
relres_linear [lemma, in b_functions]
relres_trans [lemma, in b_functions]
relres_asym [lemma, in b_functions]
relres_rel [lemma, in b_functions]
rel_restriction [definition, in b_functions]
rel_pi2 [lemma, in b_functions]
rel_pi1 [lemma, in b_functions]
rel_pair2 [lemma, in b_functions]
rel_pair1 [lemma, in b_functions]
rel_pi [lemma, in b_functions]
rel_pair [lemma, in b_functions]
rep [definition, in f_hartogs]
rep_oisomorphism [lemma, in f_hartogs]
rep_opr [lemma, in f_hartogs]
rep_bijection [lemma, in f_hartogs]
rep_function [lemma, in f_hartogs]
rep_el [lemma, in f_hartogs]
restriction [definition, in b_functions]
res_oisomorph [lemma, in d_isomorphy]
res_res [lemma, in b_functions]
res_opair [lemma, in b_functions]
res_eq [lemma, in b_functions]
res_el [lemma, in b_functions]
res_fun [lemma, in b_functions]
res_injective [lemma, in b_functions]
res_functional [lemma, in b_functions]
R_ne [lemma, in g_proof]
R_subs [lemma, in g_proof]
R1 [definition, in e_recursion]
R1_subs [lemma, in e_recursion]
R1_el [lemma, in e_recursion]
R2 [definition, in e_recursion]
R2_subs [lemma, in e_recursion]
S
sequences [definition, in g_proof]space [definition, in e_recursion]
spec [definition, in f_hartogs]
spec_eq [lemma, in f_hartogs]
spec_iseg_M [lemma, in f_hartogs]
spec_step [lemma, in f_hartogs]
spec_ordiso [lemma, in f_hartogs]
spec_el [lemma, in f_hartogs]
stransitive [definition, in c_ordinals]
succ [definition, in c_ordinals]
succ_ordinal [lemma, in c_ordinals]
succ_trans [lemma, in c_ordinals]
succ_fun [lemma, in c_ordinals]
succ_subset [lemma, in c_ordinals]
succ_el [lemma, in c_ordinals]
succ_subs [lemma, in c_ordinals]
sur [definition, in b_functions]
surjection [definition, in b_functions]
surjective [definition, in b_functions]
sur_ran [lemma, in b_functions]
sur_ran2 [lemma, in b_functions]
sur_ran1 [lemma, in b_functions]
symmetric [definition, in b_functions]
T
T [definition, in e_recursion]t [definition, in e_recursion]
tao [definition, in e_recursion]
tao_res [lemma, in e_recursion]
tao_eq [lemma, in e_recursion]
tao_app [lemma, in e_recursion]
tao_t [lemma, in e_recursion]
tao_unique [lemma, in e_recursion]
tao_comp [lemma, in e_recursion]
tao_compB [lemma, in e_recursion]
tao_compB_step [lemma, in e_recursion]
tao_TU [lemma, in e_recursion]
tao_x [lemma, in e_recursion]
tao_fun [lemma, in e_recursion]
tao_T [lemma, in e_recursion]
total [definition, in b_functions]
tot_dom [lemma, in b_functions]
tot_dom2 [lemma, in b_functions]
tot_dom1 [lemma, in b_functions]
transitive [definition, in b_functions]
TransRec [section, in e_recursion]
TransRecB [section, in e_recursion]
TransRecB.a [variable, in e_recursion]
TransRecB.AO [variable, in e_recursion]
TransRecB.B [variable, in e_recursion]
TransRecB.g [variable, in e_recursion]
TransRecB.GF [variable, in e_recursion]
TransRec.G [variable, in e_recursion]
trans_rec_b [lemma, in e_recursion]
trans_rec [lemma, in e_recursion]
trans_ind [lemma, in e_recursion]
trans_ind_b [lemma, in e_recursion]
trans_asym [lemma, in b_functions]
TU [definition, in e_recursion]
TU_fun [lemma, in e_recursion]
TU_fun2 [lemma, in e_recursion]
TU_fun1 [lemma, in e_recursion]
TU_functional [lemma, in e_recursion]
TU_total [lemma, in e_recursion]
TU_rel [lemma, in e_recursion]
TU_el [lemma, in e_recursion]
T_el [lemma, in e_recursion]
U
u_t [lemma, in e_recursion]W
wfounded [definition, in b_functions]WO [definition, in b_functions]
wordering [definition, in b_functions]
wordering_empty [lemma, in b_functions]
worder_ind [lemma, in e_recursion]
worder_subs [lemma, in b_functions]
worder_space [definition, in f_hartogs]
wo_irr [lemma, in b_functions]
wo_ordinal [lemma, in f_hartogs]
wo_ordiso [lemma, in f_hartogs]
X
xgraph [definition, in b_functions]xgraph_cor [lemma, in b_functions]
ximages [definition, in b_functions]
Z
Z [lemma, in g_proof]Zermelo [lemma, in g_proof]
zero [definition, in c_ordinals]
other
_ ^ [notation, in b_functions]_ [( _ )] [notation, in b_functions]
_ |> _ [notation, in b_functions]
_ | _ [notation, in b_functions]
_ [ _ ] [notation, in b_functions]
Lemma Index
A
app_inj [in b_functions]app_sur [in b_functions]
app_eq [in b_functions]
app_cor2 [in b_functions]
app_cor1 [in b_functions]
app_cor [in b_functions]
asym_irref [in b_functions]
a_ex [in g_proof]
a_inf [in g_proof]
a_ordinal [in g_proof]
a_subs [in g_proof]
a_el [in g_proof]
a_R [in g_proof]
a_least [in g_proof]
B
bijec_empty [in b_functions]bij_app [in b_functions]
B_tao [in e_recursion]
B_tao_app2 [in e_recursion]
B_tao_TU [in e_recursion]
B_tao_app1 [in e_recursion]
C
comp_exists [in e_recursion]comp_agree [in e_recursion]
comp_res_eq [in e_recursion]
comp_linear [in e_recursion]
comp_subs [in e_recursion]
comp_unique [in e_recursion]
comp_eq [in e_recursion]
comp_res [in e_recursion]
comp_bij [in b_functions]
comp_inj [in b_functions]
comp_sur [in b_functions]
comp_app [in b_functions]
comp_fun [in b_functions]
comp_fct [in b_functions]
comp_tot [in b_functions]
comp_rel [in b_functions]
D
doms_str [in g_proof]doms_ordinal [in g_proof]
E
elorder_linear [in c_ordinals]elorder_worder [in c_ordinals]
elorder_trans [in c_ordinals]
elorder_succ [in c_ordinals]
elorder_subs [in c_ordinals]
elorder_res [in c_ordinals]
elorder_element [in c_ordinals]
elorder_el' [in c_ordinals]
elorder_el [in c_ordinals]
el_su [in c_ordinals]
el_succ_subs [in c_ordinals]
el_succ [in c_ordinals]
empty_ordinal [in c_ordinals]
equi_trans [in b_functions]
equi_com [in b_functions]
equi_subs [in b_functions]
equi_empty [in b_functions]
exhausted [in g_proof]
F
fa_surjective [in g_proof]fa_ran [in g_proof]
fa_fun [in g_proof]
fa_M [in g_proof]
ff [in g_proof]
fg [in g_proof]
fun_subs_res [in b_functions]
fun_subs [in b_functions]
fun_res_eq [in b_functions]
fun_eq_gen [in b_functions]
fun_eq [in b_functions]
fun_subs2 [in b_functions]
fun_subs1 [in b_functions]
fun_ran [in b_functions]
fun_shrink [in b_functions]
fun_appel [in b_functions]
fun_app [in b_functions]
fun_expand [in b_functions]
fun_step [in b_functions]
fun_step_fun [in b_functions]
fun_step_tot [in b_functions]
fun_step_rel [in b_functions]
fun_ran_subs [in b_functions]
fun_el_ran [in b_functions]
fun_el_dom [in b_functions]
fun_el2 [in b_functions]
fun_el1 [in b_functions]
fun_pair2 [in b_functions]
fun_pair1 [in b_functions]
fun_pi2 [in b_functions]
fun_pi1 [in b_functions]
fun_product [in b_functions]
fun_pair [in b_functions]
fun_pi [in b_functions]
f_unique [in e_recursion]
f_rec [in e_recursion]
f_funB [in e_recursion]
f_fun [in e_recursion]
F_eq2 [in e_recursion]
F_fun [in e_recursion]
f_inj [in g_proof]
f_seq [in g_proof]
f_rel [in g_proof]
G
g2f [in g_proof]H
hartogs [in f_hartogs]hartogs_ordinal [in f_hartogs]
hartogs_el [in f_hartogs]
h_ordiso [in f_hartogs]
I
id_fun [in b_functions]id_rel [in b_functions]
id_equal [in b_functions]
id_app [in b_functions]
id_bijection [in b_functions]
image_oisomorph2 [in d_isomorphy]
image_oisomorph [in d_isomorphy]
image_ran [in b_functions]
image_bij [in b_functions]
image_bijection [in b_functions]
image_sur [in b_functions]
image_tot [in b_functions]
image_rel [in b_functions]
image_res [in b_functions]
image_el [in b_functions]
image_empty [in b_functions]
image_subs [in b_functions]
im_el [in b_functions]
im_cor [in b_functions]
inv_idem [in b_functions]
inv_element [in b_functions]
inv_el [in b_functions]
inv_bij [in b_functions]
inv_el2 [in b_functions]
inv_el1 [in b_functions]
inv1 [in b_functions]
inv2 [in b_functions]
iorder_wf [in c_ordinals]
iorder_lin [in c_ordinals]
iorder_trans [in c_ordinals]
iorder_asym [in c_ordinals]
iorder_dom2 [in c_ordinals]
iorder_dom1 [in c_ordinals]
iorder_el' [in c_ordinals]
iorder_el [in c_ordinals]
irref_asym [in b_functions]
iseg_oisoeq [in e_recursion]
iseg_res [in d_isomorphy]
iseg_ordinal [in d_isomorphy]
iseg_ordinal_eq [in d_isomorphy]
iseg_equal [in d_isomorphy]
iseg_worder [in d_isomorphy]
iseg_eq [in d_isomorphy]
iseg_subs [in d_isomorphy]
iseg_el [in d_isomorphy]
iseg_nel [in d_isomorphy]
L
lam_inj [in b_functions]lam_sur [in b_functions]
lam_subs [in b_functions]
lam_app2 [in b_functions]
lam_app [in b_functions]
lam_fun [in b_functions]
lam_el [in b_functions]
O
oiseg_lin [in d_isomorphy]oiseg_eq [in d_isomorphy]
oiso_eq [in d_isomorphy]
oiso_images [in d_isomorphy]
oiso_iseg [in d_isomorphy]
oiso_trans [in d_isomorphy]
oiso_com [in d_isomorphy]
oiso_ref [in d_isomorphy]
Olemrez [in g_proof]
ordinals_sosubset [in c_ordinals]
ordinal_iso [in e_recursion]
ordinal_ordiso [in e_recursion]
ordinal_wf [in e_recursion]
ordinal_wo [in c_ordinals]
ordinal_iorder [in c_ordinals]
ordinal_noset [in c_ordinals]
ordinal_bunion [in c_ordinals]
ordinal_union [in c_ordinals]
ordinal_set [in c_ordinals]
ordinal_set_wf [in c_ordinals]
ordinal_set_trans [in c_ordinals]
ordinal_set_asym [in c_ordinals]
ordinal_wfounded [in c_ordinals]
ordinal_linear [in c_ordinals]
ordinal_inter [in c_ordinals]
ordinal_anti [in c_ordinals]
ordinal_trans [in c_ordinals]
ordinal_nel [in c_ordinals]
ordinal_subs [in c_ordinals]
ordinal_eltrans [in c_ordinals]
ordinal_el [in c_ordinals]
ordiso_eq [in e_recursion]
ordiso_trans [in d_isomorphy]
ord_order2 [in f_hartogs]
ord_order1 [in f_hartogs]
ord_norder2 [in f_hartogs]
ord_norder1 [in f_hartogs]
ord_unique [in f_hartogs]
ord_ordinal [in f_hartogs]
ord_otype [in f_hartogs]
otype_unique [in f_hartogs]
otype_ordiso [in f_hartogs]
otype_ordinal [in f_hartogs]
otype_stransitive [in f_hartogs]
otype_elord [in f_hartogs]
otype_eliso [in f_hartogs]
otype_empty [in f_hartogs]
P
pow_nempty [in g_proof]pow_subs [in g_proof]
R
ran_subs [in g_proof]rec [in g_proof]
relres_wf [in b_functions]
relres_linear [in b_functions]
relres_trans [in b_functions]
relres_asym [in b_functions]
relres_rel [in b_functions]
rel_pi2 [in b_functions]
rel_pi1 [in b_functions]
rel_pair2 [in b_functions]
rel_pair1 [in b_functions]
rel_pi [in b_functions]
rel_pair [in b_functions]
rep_oisomorphism [in f_hartogs]
rep_opr [in f_hartogs]
rep_bijection [in f_hartogs]
rep_function [in f_hartogs]
rep_el [in f_hartogs]
res_oisomorph [in d_isomorphy]
res_res [in b_functions]
res_opair [in b_functions]
res_eq [in b_functions]
res_el [in b_functions]
res_fun [in b_functions]
res_injective [in b_functions]
res_functional [in b_functions]
R_ne [in g_proof]
R_subs [in g_proof]
R1_subs [in e_recursion]
R1_el [in e_recursion]
R2_subs [in e_recursion]
S
spec_eq [in f_hartogs]spec_iseg_M [in f_hartogs]
spec_step [in f_hartogs]
spec_ordiso [in f_hartogs]
spec_el [in f_hartogs]
succ_ordinal [in c_ordinals]
succ_trans [in c_ordinals]
succ_fun [in c_ordinals]
succ_subset [in c_ordinals]
succ_el [in c_ordinals]
succ_subs [in c_ordinals]
sur_ran [in b_functions]
sur_ran2 [in b_functions]
sur_ran1 [in b_functions]
T
tao_res [in e_recursion]tao_eq [in e_recursion]
tao_app [in e_recursion]
tao_t [in e_recursion]
tao_unique [in e_recursion]
tao_comp [in e_recursion]
tao_compB [in e_recursion]
tao_compB_step [in e_recursion]
tao_TU [in e_recursion]
tao_x [in e_recursion]
tao_fun [in e_recursion]
tao_T [in e_recursion]
tot_dom [in b_functions]
tot_dom2 [in b_functions]
tot_dom1 [in b_functions]
trans_rec_b [in e_recursion]
trans_rec [in e_recursion]
trans_ind [in e_recursion]
trans_ind_b [in e_recursion]
trans_asym [in b_functions]
TU_fun [in e_recursion]
TU_fun2 [in e_recursion]
TU_fun1 [in e_recursion]
TU_functional [in e_recursion]
TU_total [in e_recursion]
TU_rel [in e_recursion]
TU_el [in e_recursion]
T_el [in e_recursion]
U
u_t [in e_recursion]W
wordering_empty [in b_functions]worder_ind [in e_recursion]
worder_subs [in b_functions]
wo_irr [in b_functions]
wo_ordinal [in f_hartogs]
wo_ordiso [in f_hartogs]
X
xgraph_cor [in b_functions]Z
Z [in g_proof]Zermelo [in g_proof]
Section Index
P
proof [in g_proof]T
TransRec [in e_recursion]TransRecB [in e_recursion]
Notation Index
other
_ ^ [in b_functions]_ [( _ )] [in b_functions]
_ |> _ [in b_functions]
_ | _ [in b_functions]
_ [ _ ] [in b_functions]
Definition Index
A
a [in g_proof]AC [in g_proof]
antisymmetric [in b_functions]
app [in b_functions]
asymmetric [in b_functions]
B
bijection [in b_functions]bijective [in b_functions]
bran [in g_proof]
C
comp [in e_recursion]comp [in b_functions]
compB [in e_recursion]
D
dom [in b_functions]doms [in g_proof]
E
elorder [in c_ordinals]equi [in b_functions]
equivalence [in b_functions]
F
f [in e_recursion]F [in e_recursion]
f [in g_proof]
field [in b_functions]
fset [in e_recursion]
function [in b_functions]
functional [in b_functions]
G
G [in e_recursion]g [in g_proof]
H
h [in f_hartogs]I
id [in b_functions]image [in b_functions]
inj [in b_functions]
injection [in b_functions]
injective [in b_functions]
inverse [in b_functions]
iorder [in c_ordinals]
irreflexive [in b_functions]
iseg [in d_isomorphy]
L
lam [in b_functions]least [in b_functions]
linear [in b_functions]
lordering [in b_functions]
O
oiseg [in d_isomorphy]oiso [in d_isomorphy]
oisomorphism [in d_isomorphy]
one [in c_ordinals]
opres [in d_isomorphy]
ord [in f_hartogs]
ordertype [in f_hartogs]
ordinal [in c_ordinals]
ordiso [in d_isomorphy]
P
pow' [in g_proof]R
R [in g_proof]ran [in b_functions]
reflexive [in b_functions]
relation [in b_functions]
relations [in f_hartogs]
rel_restriction [in b_functions]
rep [in f_hartogs]
restriction [in b_functions]
R1 [in e_recursion]
R2 [in e_recursion]
S
sequences [in g_proof]space [in e_recursion]
spec [in f_hartogs]
stransitive [in c_ordinals]
succ [in c_ordinals]
sur [in b_functions]
surjection [in b_functions]
surjective [in b_functions]
symmetric [in b_functions]
T
T [in e_recursion]t [in e_recursion]
tao [in e_recursion]
total [in b_functions]
transitive [in b_functions]
TU [in e_recursion]
W
wfounded [in b_functions]WO [in b_functions]
wordering [in b_functions]
worder_space [in f_hartogs]
X
xgraph [in b_functions]ximages [in b_functions]
Z
zero [in c_ordinals]Variable Index
P
proof.c [in g_proof]proof.choice [in g_proof]
proof.M [in g_proof]
T
TransRecB.a [in e_recursion]TransRecB.AO [in e_recursion]
TransRecB.B [in e_recursion]
TransRecB.g [in e_recursion]
TransRecB.GF [in e_recursion]
TransRec.G [in e_recursion]
Library Index
A
a_setsB
b_functionsC
c_ordinalsD
d_isomorphyE
e_recursionF
f_hartogsG
g_proof| 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 | (394 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 | (289 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 | (3 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 | (5 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 | (81 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 | (9 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 | (7 entries) |
This page has been generated by coqdoc