Global Index

other

(793 entries)

Notation Index

other

(10 entries)

Variable Index

other

(26 entries)

Library Index

other

(15 entries)

Lemma Index

other

(443 entries)

Constructor Index

other

(8 entries)

Axiom Index

other

(6 entries)

Projection Index

other

(48 entries)

Inductive Index

other

(6 entries)

Section Index

other

(22 entries)

Instance Index

other

(30 entries)

Abbreviation Index

other

(7 entries)

Definition Index

other

(157 entries)

Record Index

other

(15 entries)

Global Index

A

AC [definition, in Categoricity]
AC [section, in Categoricity]
ACZ [instance, in Quotient_TD]
Acz [inductive, in Aczel]
Aczel [library]
AczSS [definition, in Aczel]
AczZS [definition, in Aczel]
Acz_ZF [instance, in Quotient_TD]
Acz_Inf [lemma, in Aczel]
Acz_ZF' [instance, in Aczel]
Acz_ZS [lemma, in Aczel]
ACZ' [instance, in Aczel]
AC_ZFn [lemma, in Categoricity]
AC.M [variable, in Categoricity]
AC.MZF [variable, in Categoricity]
adj [definition, in Infinity]
adj_sub [lemma, in Infinity]
adj_union [lemma, in Infinity]
adj_power [lemma, in Infinity]
adj_sep [lemma, in Infinity]
adj_el [lemma, in Infinity]
AEmpty [definition, in Aczel]
AEmptyAx [lemma, in Aczel]
Aeq [definition, in Aczel]
Aeq_equiv [lemma, in Aczel]
Aeq_ASubq [lemma, in Aczel]
Aeq_ext [lemma, in Aczel]
aeq_equiv [instance, in Aczel]
Aeq_tra [lemma, in Aczel]
Aeq_sym [lemma, in Aczel]
Aeq_ref' [lemma, in Aczel]
Aeq_ref [lemma, in Aczel]
Aeq_NS_eq [lemma, in Quotient_CR]
Aeq_p1_eq [lemma, in Quotient_CR]
Aeq_p1_NS_eq [lemma, in Quotient_CR]
Aeq_p1_NS [lemma, in Quotient_CR]
Aeq_eqclass [lemma, in Quotient_CE]
agree [definition, in Prelims]
agree_unique [lemma, in Basics]
Ain [definition, in Aczel]
Ain_AWF [lemma, in Aczel]
Ain_proper [instance, in Aczel]
Ain_mor [lemma, in Aczel]
Ain_pi [lemma, in Aczel]
Ain_Asup [lemma, in Aczel]
Ain_IN_NS_p1 [lemma, in Quotient_CR]
Ain_IN_p1_NS [lemma, in Quotient_CR]
Ain_IN_NS [lemma, in Quotient_CR]
Ain_IN_p1 [lemma, in Quotient_CR]
antifounded [lemma, in Permutation]
Aom [definition, in Aczel]
Aom_spec [lemma, in Aczel]
Apower [definition, in Aczel]
ApowerAx [lemma, in Aczel]
Apower_proper [instance, in Aczel]
Apower_mor [lemma, in Aczel]
Arepl [definition, in Aczel]
AreplAx [lemma, in Aczel]
Arepl_proper [lemma, in Aczel]
Arepl_proper' [lemma, in Aczel]
Arepl_mor [lemma, in Aczel]
Asep [definition, in Aczel]
AsepAx [lemma, in Aczel]
Asep_proper [lemma, in Aczel]
Asep_proper' [lemma, in Aczel]
Asep_mor [lemma, in Aczel]
ASubq [definition, in Aczel]
ASubq_proper [instance, in Aczel]
ASubq_Subq_p1 [lemma, in Quotient_CR]
Asup [constructor, in Aczel]
Asup_inj [lemma, in Aczel]
ATS [definition, in Quotient_TD]
ATS_strength [lemma, in Quotient_TD]
ATS_universe [lemma, in Quotient_TD]
ATS_sur [lemma, in Quotient_TD]
ATS_mor [lemma, in Quotient_TD]
Aunion [definition, in Aczel]
AunionAx [lemma, in Aczel]
Aunion_proper [instance, in Aczel]
Aunion_mor [lemma, in Aczel]
Aupair [definition, in Aczel]
AupairAx [lemma, in Aczel]
Aupair_proper [instance, in Aczel]
Aupair_mor [lemma, in Aczel]
AWF_Aeq [lemma, in Aczel]
AxWF [projection, in Prelims]
ax_rep' [lemma, in Truncation]

B

Basic [section, in Basics]
Basics [library]
binunion [abbreviation, in Prelims]
binunion_adj [lemma, in Infinity]
binunion_eset [lemma, in Infinity]
binunion_el [lemma, in Infinity]
bounded_small [lemma, in Basics]
bsur [definition, in Zermelo]
bsur_rep [lemma, in Zermelo]
btot [definition, in Zermelo]
btot_rep [lemma, in Zermelo]
btot_power [lemma, in Zermelo]
btot_union [lemma, in Zermelo]
btot_eset [lemma, in Zermelo]
btot_bsur [lemma, in Zermelo]

C

D

delta [projection, in Prelims]
delta_eq [lemma, in Basics]
delta_spec [lemma, in Basics]
delta_equiv [lemma, in Embeddings]
delta_equal [lemma, in Truncation]
delta' [definition, in Basics]
delta'_fun [lemma, in Basics]
desc [definition, in Quotient_TD]
desc [definition, in Truncation]
descAx [lemma, in Quotient_TD]
descAx1 [lemma, in Quotient_TD]
descAx2 [lemma, in Quotient_TD]
descp [definition, in Truncation]
desc_p [lemma, in Truncation]
desc_nissing [lemma, in Truncation]
desc_issing [lemma, in Truncation]
Desc1 [projection, in Prelims]
Desc2 [projection, in Prelims]
Domain [section, in Zermelo]
domain [definition, in Zermelo]
domain_Stage_sub [lemma, in Zermelo]
domain_universe [lemma, in Zermelo]
domain_ZF [lemma, in Zermelo]
domain_sub [lemma, in Zermelo]
domain_el [lemma, in Zermelo]
domain_rep [lemma, in Zermelo]
domain_power [lemma, in Zermelo]
domain_union [lemma, in Zermelo]
dom_rep [definition, in Basics]

E

ele [definition, in Permutation]
ele [definition, in Quotient_CE]
elem [projection, in Prelims]
elem_proper [instance, in Prelims]
elem_proper' [lemma, in Prelims]
ele_WF [lemma, in Quotient_CE]
em [definition, in Large]
Embed [section, in Large]
embed [definition, in Truncation]
Embeddings [library]
embed_delta [lemma, in Truncation]
embed_unique [lemma, in Truncation]
emclass [definition, in Truncation]
emc_issing [lemma, in Truncation]
emfun [definition, in Quotient_CR]
emfun_Aeq [lemma, in Quotient_CR]
empred [definition, in Quotient_CR]
empred [definition, in Quotient_CE]
empred_Aeq [lemma, in Quotient_CR]
empred_Aeq [lemma, in Quotient_CE]
empty [definition, in Permutation]
empty [definition, in Quotient_CE]
emptyAx [lemma, in Permutation]
emptyE [lemma, in Quotient_CR]
emptyE [lemma, in Quotient_CE]
em_sur [lemma, in Large]
em_mor [lemma, in Large]
em_equiv [lemma, in Large]
em_rec [lemma, in Large]
em_invar [lemma, in Large]
em' [definition, in Large]
eqcl [abbreviation, in Prelims]
eqclass [definition, in Quotient_CE]
equiv [definition, in Prelims]
equiv_em [lemma, in Large]
equiv_equiv [instance, in Prelims]
eq_equiv [lemma, in Prelims]
Eset [projection, in Prelims]
eset [projection, in Prelims]
eset_unique [lemma, in Basics]
eset_sub [lemma, in Basics]
eset_HF [lemma, in Infinity]
exmp [definition, in Truncation]
Ext [lemma, in Basics]
extAx [lemma, in Permutation]
ex_rank [lemma, in Stage]

F

F [definition, in Permutation]
false [lemma, in Uncountable]
FG [lemma, in Permutation]
Fin [inductive, in Infinity]
FinA [constructor, in Infinity]
FinE [constructor, in Infinity]
finpow [definition, in Prelims]
Fin_chain_max [lemma, in Infinity]
Fin_binunion [lemma, in Infinity]
Fin_frep [lemma, in Infinity]
Fin_rep [lemma, in Infinity]
Fin_subset [lemma, in Infinity]
FM_ZFS [lemma, in Permutation]
FM_ZS [lemma, in Permutation]
Fneq [lemma, in Permutation]
Frep [projection, in Prelims]
frep [projection, in Prelims]
frepAx [lemma, in Permutation]
frepl [definition, in Permutation]
frep_el [lemma, in Basics]
frep' [definition, in Basics]
frep'_el [lemma, in Basics]
fres [definition, in Prelims]
fress [lemma, in Truncation]
fres_eq [lemma, in Basics]
fres_equiv [lemma, in Aczel]
functional [definition, in Prelims]
F0 [lemma, in Permutation]
F1 [lemma, in Permutation]

G

G [definition, in Permutation]
gel [abbreviation, in Prelims]
GF [lemma, in Permutation]
Gneq [lemma, in Permutation]
G0 [lemma, in Permutation]
G1 [lemma, in Permutation]

H

help [lemma, in Uncountable]
HF [inductive, in Infinity]
HFI [constructor, in Infinity]
HF_OM [lemma, in Infinity]
HF_rho [lemma, in Infinity]
HF_ZF [lemma, in Infinity]
HF_union [lemma, in Infinity]
HF_eset [lemma, in Infinity]
HF_ctrans [lemma, in Infinity]
HF_power [lemma, in Infinity]
HF_rep [lemma, in Infinity]
HF_Fin [lemma, in Infinity]
HiZ [projection, in Prelims]
HiZF [projection, in Prelims]
HiZF' [projection, in Prelims]
HZ [projection, in Prelims]
HZF [projection, in Prelims]
HZFS [projection, in Prelims]
HZF' [projection, in Prelims]
h_strength [lemma, in Embeddings]
h_const [lemma, in Embeddings]
h_universe [lemma, in Embeddings]
h_frep2 [lemma, in Embeddings]
h_frep1 [lemma, in Embeddings]
h_power [lemma, in Embeddings]
h_union [lemma, in Embeddings]
h_upair [lemma, in Embeddings]
h_eset [lemma, in Embeddings]
h_swelled2 [lemma, in Embeddings]
h_swelled1 [lemma, in Embeddings]
h_trans2 [lemma, in Embeddings]
h_trans1 [lemma, in Embeddings]
h_sur_sub [lemma, in Embeddings]
h_cres [lemma, in Embeddings]
h_Proper [instance, in Embeddings]
h_equiv [lemma, in Embeddings]
h_sub [lemma, in Embeddings]

I

i [definition, in Zermelo]
II [constructor, in Zermelo]
ij [lemma, in Zermelo]
IM [definition, in Truncation]
img [definition, in Embeddings]
img_ZF [lemma, in Embeddings]
img_frep2 [lemma, in Embeddings]
img_frep1 [lemma, in Embeddings]
img_Z2 [lemma, in Embeddings]
img_Z1 [lemma, in Embeddings]
img_cswelled2 [lemma, in Embeddings]
img_cswelled1 [lemma, in Embeddings]
img_ctrans2 [lemma, in Embeddings]
img_ctrans1 [lemma, in Embeddings]
img_cres [lemma, in Embeddings]
img_P [lemma, in Embeddings]
img_Proper [instance, in Embeddings]
img_agree [lemma, in Embeddings]
IMISO [section, in Truncation]
IMISO.p [variable, in Truncation]
IMISO.PC [variable, in Truncation]
IM_strength [lemma, in Truncation]
IM_universe [lemma, in Truncation]
IM_ZF [lemma, in Truncation]
IN [definition, in Quotient_CR]
Inf [definition, in Prelims]
Inf [section, in Infinity]
Infinity [lemma, in Uncountable]
Infinity [lemma, in Infinity]
Infinity [section, in Infinity]
Infinity [library]
Infinity' [lemma, in Uncountable]
Infinity' [lemma, in Infinity]
Infinity.MI [variable, in Infinity]
inhab [abbreviation, in Prelims]
inhab_neq [lemma, in Basics]
inhab_not [lemma, in Basics]
injective [definition, in Prelims]
Instance [section, in Permutation]
1 [notation, in Permutation]
IN_WF [lemma, in Quotient_CR]
IN_Ain_NS_p1 [lemma, in Quotient_CR]
IN_Ain_p1_NS [lemma, in Quotient_CR]
IN_Ain_NS [lemma, in Quotient_CR]
IN_Ain_p1 [lemma, in Quotient_CR]
iseqcl [definition, in Prelims]
Iso [section, in Zermelo]
iso [definition, in Zermelo]
Iso [inductive, in Zermelo]
Iso_tricho [lemma, in Zermelo]
Iso_max [lemma, in Zermelo]
Iso_Stage_max [lemma, in Zermelo]
Iso_strength [lemma, in Zermelo]
Iso_universe [lemma, in Zermelo]
Iso_closed_rep [lemma, in Zermelo]
Iso_closed_power [lemma, in Zermelo]
Iso_closed_union [lemma, in Zermelo]
Iso_trans [lemma, in Zermelo]
Iso_Stage [lemma, in Zermelo]
Iso_dom' [lemma, in Zermelo]
Iso_dom [lemma, in Zermelo]
Iso_rep [lemma, in Zermelo]
Iso_power [lemma, in Zermelo]
Iso_union [lemma, in Zermelo]
Iso_eset [lemma, in Zermelo]
Iso_mem [lemma, in Zermelo]
Iso_inj [lemma, in Zermelo]
Iso_res [lemma, in Zermelo]
Iso_fun [lemma, in Zermelo]
Iso_bsur [lemma, in Zermelo]
Iso_btot [lemma, in Zermelo]
Iso_sym [lemma, in Zermelo]
Iso_parti [lemma, in Categoricity]
issing [definition, in Truncation]
issing_ext [lemma, in Truncation]
iZ [record, in Prelims]
iZF [record, in Prelims]
iZF' [record, in Prelims]
iZS [record, in Prelims]
i_ran [lemma, in Zermelo]
i_Iso [lemma, in Zermelo]

J

j [definition, in Zermelo]
ji [lemma, in Zermelo]
j_dom [lemma, in Zermelo]
j_Iso [lemma, in Zermelo]

L

Large [library]
least [definition, in Prelims]
least_unique [lemma, in Basics]
limit [definition, in Stage]
limit_Z [lemma, in Stage]
limit_sep [lemma, in Stage]
limit_upair [lemma, in Stage]
limit_power [lemma, in Stage]
limit_union [lemma, in Stage]
limit_closed_stage [lemma, in Stage]
limit_infinite [lemma, in Infinity]
limit_OM [lemma, in Infinity]

M

M [definition, in Uncountable]
Main [section, in Zermelo]
MI [lemma, in Infinity]
Mor [section, in Embeddings]
Morph [projection, in Prelims]
Mor.h [variable, in Embeddings]
Mor.h_sur [variable, in Embeddings]
Mor.h_mor [variable, in Embeddings]
MP [definition, in Truncation]
MPZF [instance, in Truncation]
MTN [definition, in Embeddings]
MTN_fres [definition, in Embeddings]
MtoN [definition, in Zermelo]
MtoN_fun [lemma, in Zermelo]
MZF [instance, in Infinity]
M_ZF [definition, in Permutation]
M_ZF' [definition, in Permutation]
M_ZS [definition, in Permutation]
M_SS [definition, in Permutation]

N

N [definition, in Quotient_TD]
N [definition, in Uncountable]
N [projection, in Quotient_CR]
nat_bool [lemma, in Aczel]
Norm [instance, in Quotient_TD]
Normalizer [record, in Quotient_CR]
not_total_domain [lemma, in Zermelo]
not_total_exists [lemma, in Zermelo]
NS [definition, in Quotient_CR]
NS_powit [lemma, in Quotient_CR]
NS_p1_eq [lemma, in Quotient_CR]
NS_eq_Aeq_p1 [lemma, in Quotient_CR]
NTM [definition, in Embeddings]
NTM_fres [lemma, in Embeddings]
Num [definition, in Uncountable]
N_proper [instance, in Quotient_CR]
N_eq_Aeq [lemma, in Quotient_CR]
N_idem [lemma, in Quotient_CR]

O

om [definition, in Uncountable]
OM [definition, in Infinity]
om [definition, in Infinity]
OM_least [lemma, in Infinity]
OM_least_limit [lemma, in Infinity]
om_infinite [lemma, in Infinity]
om_limit [lemma, in Infinity]
OM_ZF1 [lemma, in Infinity]
OM_universe [lemma, in Infinity]
OM_repclosed [lemma, in Infinity]
OM_rho_el [lemma, in Infinity]
OM_Fin [lemma, in Infinity]
OM_limit [lemma, in Infinity]
OM_stage [lemma, in Infinity]
OM_eset [lemma, in Infinity]
OM_ex_powit [lemma, in Infinity]
OM_powit [lemma, in Infinity]

P

P [definition, in Truncation]
Pair [projection, in Prelims]
pair [definition, in Permutation]
pairAx [lemma, in Permutation]
pair_el [lemma, in Basics]
parti [definition, in Categoricity]
Perm [section, in Permutation]
Permutation [library]
Perm.F [variable, in Permutation]
Perm.FG [variable, in Permutation]
Perm.G [variable, in Permutation]
Perm.GF [variable, in Permutation]
PI [axiom, in Quotient_TD]
PI [projection, in Quotient_CR]
PI [axiom, in Quotient_CE]
pi [definition, in Truncation]
PI [lemma, in Truncation]
pi_Ain [lemma, in Aczel]
PI_eq [lemma, in Quotient_CR]
pi_sur [lemma, in Truncation]
pi_mor [lemma, in Truncation]
pi1 [definition, in Aczel]
pi2 [definition, in Aczel]
pow [definition, in Permutation]
Power [projection, in Prelims]
power [projection, in Prelims]
power [definition, in Quotient_CE]
powerAx [lemma, in Permutation]
powerAx [lemma, in Quotient_CR]
powerAx [lemma, in Quotient_CE]
power_above [lemma, in Basics]
power_inj [lemma, in Basics]
power_mono [lemma, in Basics]
power_trans [lemma, in Basics]
power_eager [lemma, in Basics]
power_proper [instance, in Prelims]
power_proper' [lemma, in Prelims]
power_Fin [lemma, in Infinity]
power_welldef [lemma, in Quotient_CE]
power_eqclass [lemma, in Quotient_CE]
power' [definition, in Quotient_CE]
powit [definition, in Prelims]
powit_inj [lemma, in Uncountable]
powit_Fin [lemma, in Infinity]
powit_HF [lemma, in Infinity]
powit_stage [lemma, in Infinity]
pow_eset [lemma, in Infinity]
preim [definition, in Embeddings]
preim_equiv' [lemma, in Embeddings]
preim_equiv [lemma, in Embeddings]
Prelims [library]
Proper [section, in Prelims]
PS [definition, in Truncation]
PZ [definition, in Truncation]
PZF' [definition, in Truncation]
P_ZF' [lemma, in Truncation]
P_Z [lemma, in Truncation]
P_WF [lemma, in Truncation]
P_Ext [lemma, in Truncation]
P_proj [lemma, in Truncation]
P_eq [lemma, in Truncation]

Q

quine [lemma, in Permutation]
Quotient_CE [library]
Quotient_CR [library]
Quotient_TD [library]

R

R [definition, in Permutation]
range [definition, in Zermelo]
range_universe [lemma, in Zermelo]
range_domain_small [lemma, in Zermelo]
range_domain [lemma, in Zermelo]
rank [definition, in Stage]
rank_fun [lemma, in Stage]
reachable [definition, in Stage]
Rep [lemma, in Basics]
rep [definition, in Basics]
replAx [lemma, in Quotient_CR]
rep_delta [lemma, in Basics]
rep_frep [lemma, in Basics]
rep_sep [lemma, in Basics]
rep_upair [lemma, in Basics]
rep_adj [lemma, in Infinity]
rep_sing [lemma, in Infinity]
rep_eset [lemma, in Infinity]
rep' [definition, in Truncation]
rho [definition, in Stage]
rho_rank [lemma, in Stage]
rho_rho' [lemma, in Stage]
rho_rank_ex [lemma, in Stage]
rho' [definition, in Stage]
rho'_rank [lemma, in Stage]
R_unique [lemma, in Permutation]
R' [definition, in Permutation]
R'_unique [lemma, in Permutation]

S

Sempty [definition, in Quotient_CR]
Sep [projection, in Prelims]
sep [projection, in Prelims]
sep [definition, in Quotient_CE]
sepa [definition, in Permutation]
sepAx [lemma, in Permutation]
sepAx [lemma, in Quotient_CR]
sepAx [lemma, in Quotient_CE]
sep_sub [lemma, in Basics]
sep_el [lemma, in Basics]
sep_cswelled [lemma, in Prelims]
sep_welldef [lemma, in Quotient_CE]
sep_eqclass [lemma, in Quotient_CE]
sep_false [lemma, in Truncation]
sep_true [lemma, in Truncation]
sep' [definition, in Basics]
sep' [definition, in Quotient_CE]
sep'_el [lemma, in Basics]
set [projection, in Prelims]
SET [instance, in Quotient_TD]
SET [instance, in Quotient_CE]
SETSS [definition, in Quotient_CR]
SETSS [definition, in Quotient_CE]
SetStruct [record, in Prelims]
SETZF_Inf [lemma, in Quotient_CR]
SETZF_ZF' [lemma, in Quotient_CR]
SETZF_Z [lemma, in Quotient_CR]
SETZF' [definition, in Quotient_CR]
SETZS [definition, in Quotient_CR]
SET_ZF [instance, in Quotient_TD]
set_not_sub [lemma, in Stage]
set_ext [lemma, in Quotient_CR]
SET_Inf [lemma, in Quotient_CE]
SET_Z [instance, in Quotient_CE]
set_ext [lemma, in Quotient_CE]
SET' [definition, in Quotient_CR]
SET' [definition, in Quotient_CE]
shrink [lemma, in Truncation]
sing [abbreviation, in Prelims]
sing_union [lemma, in Basics]
sing_el [lemma, in Basics]
sing_neq [lemma, in Aczel]
sing_Aeq [lemma, in Aczel]
sing_eqcl [lemma, in Truncation]
sing1 [definition, in Aczel]
sing2 [definition, in Aczel]
small [definition, in Prelims]
small_red [lemma, in Basics]
Spower [definition, in Quotient_CR]
Srepl [definition, in Quotient_CR]
Ssep [definition, in Quotient_CR]
ST [definition, in Large]
Stage [inductive, in Stage]
Stage [section, in Stage]
Stage [library]
Stages [section, in Zermelo]
StageS [constructor, in Stage]
StageU [constructor, in Stage]
Stage_Iso [lemma, in Zermelo]
Stage_btot [lemma, in Zermelo]
Stage_inhab [lemma, in Stage]
Stage_succ_limit [lemma, in Stage]
Stage_dicho [lemma, in Stage]
Stage_least [lemma, in Stage]
Stage_tricho [lemma, in Stage]
Stage_lin_el [lemma, in Stage]
Stage_lin [lemma, in Stage]
Stage_lin_succ [lemma, in Stage]
Stage_double_ind [lemma, in Stage]
Stage_inc [lemma, in Stage]
Stage_sep [lemma, in Stage]
Stage_upair [lemma, in Stage]
Stage_power [lemma, in Stage]
Stage_union [lemma, in Stage]
Stage_swelled [lemma, in Stage]
Stage_trans [lemma, in Stage]
Stage_eset [lemma, in Stage]
step [lemma, in Large]
strength [definition, in Prelims]
strength_weak [lemma, in Basics]
strength_proper [instance, in Prelims]
strength_proper' [lemma, in Prelims]
sub [definition, in Prelims]
sub [definition, in Permutation]
sub [definition, in Quotient_CE]
Sub [section, in Truncation]
Subq [definition, in Quotient_CR]
subset_outside [lemma, in Basics]
sub_eset [lemma, in Basics]
sub_trans [lemma, in Basics]
sub_refl [lemma, in Basics]
sub_proper [instance, in Prelims]
Sub.p [variable, in Truncation]
Sub.PC [variable, in Truncation]
Sub.PWF [variable, in Truncation]
Sub.set [variable, in Truncation]
Sub.set_ZF [variable, in Truncation]
succ [definition, in Stage]
Sunion [definition, in Quotient_CR]
Supair [definition, in Quotient_CR]
surjective [definition, in Prelims]
swelled [definition, in Prelims]
swelled_sep [lemma, in Prelims]

T

tdelta [axiom, in Quotient_TD]
TDesc1 [axiom, in Quotient_TD]
TDesc2 [axiom, in Quotient_TD]
toP [definition, in Truncation]
total [definition, in Prelims]
tot_sur [lemma, in Zermelo]
trace [definition, in Categoricity]
trans [definition, in Prelims]
trans_strength [lemma, in Basics]
trans_power [lemma, in Basics]
trans_strength [lemma, in Large]
Truncation [library]

U

W

X

xm_upbnd [lemma, in Stage]

Z

Z [record, in Prelims]
Zermelo [library]
ZExt [projection, in Prelims]
ZF [record, in Prelims]
ZFExt [projection, in Prelims]
ZFExt' [projection, in Prelims]
ZFge [definition, in Prelims]
ZFge_cons [lemma, in Large]
ZFge0 [lemma, in Large]
ZFn [definition, in Prelims]
ZFn_ZFw [lemma, in Large]
ZFn_cons_not_provable [lemma, in Large]
ZFS [record, in Prelims]
ZFSDesc [lemma, in Truncation]
ZFSDesc1 [projection, in Prelims]
ZFSDesc2 [projection, in Prelims]
ZFset [projection, in Prelims]
ZFset' [projection, in Prelims]
ZFSExt [projection, in Prelims]
ZFSFrep [projection, in Prelims]
ZFStruct [record, in Prelims]
ZFStruct' [record, in Prelims]
ZFS_model [lemma, in Permutation]
ZFw [definition, in Prelims]
ZF_rep [lemma, in Basics]
ZF_rep' [lemma, in Basics]
ZF_proper [instance, in Prelims]
ZF_proper' [lemma, in Prelims]
ZF_ZFS [lemma, in Truncation]
ZF' [record, in Prelims]
Zset [projection, in Prelims]
ZStruct [record, in Prelims]
Z_rep [lemma, in Basics]

other

_ <=s _ [notation, in Prelims]
_ <=c _ [notation, in Prelims]
_ <=p _ [notation, in Prelims]
_ == _ [notation, in Prelims]
_ << _ [notation, in Prelims]
_ <<= _ [notation, in Prelims]
_ nel _ [notation, in Prelims]
_ el _ [notation, in Prelims]
0 [notation, in Prelims]

Notation Index

I

1 [in Permutation]

other

_ <=s _ [in Prelims]
_ <=c _ [in Prelims]
_ <=p _ [in Prelims]
_ == _ [in Prelims]
_ << _ [in Prelims]
_ <<= _ [in Prelims]
_ nel _ [in Prelims]
_ el _ [in Prelims]
0 [in Prelims]

Variable Index

A

AC.M [in Categoricity]
AC.MZF [in Categoricity]

C

Categoricity.F [in Categoricity]
Categoricity.FG [in Categoricity]
Categoricity.G [in Categoricity]
Categoricity.GF [in Categoricity]

I

IMISO.p [in Truncation]
IMISO.PC [in Truncation]
Infinity.MI [in Infinity]

M

Mor.h [in Embeddings]
Mor.h_sur [in Embeddings]
Mor.h_mor [in Embeddings]

P

Perm.F [in Permutation]
Perm.FG [in Permutation]
Perm.G [in Permutation]
Perm.GF [in Permutation]

S

Sub.p [in Truncation]
Sub.PC [in Truncation]
Sub.PWF [in Truncation]
Sub.set [in Truncation]
Sub.set_ZF [in Truncation]

U

Uncountable.f [in Uncountable]
Uncountable.f_sur [in Uncountable]
Uncountable.set [in Uncountable]
Uncountable.SI [in Uncountable]
Uncountable.SZF [in Uncountable]

Library Index

A

Aczel

B

Basics

C

Categoricity

E

Embeddings

I

Infinity

L

Large

P

Permutation
Prelims

Q

Quotient_CE
Quotient_CR
Quotient_TD

S

Stage

T

Truncation

U

Uncountable

Z

Zermelo

Lemma Index

A

Acz_Inf [in Aczel]
Acz_ZS [in Aczel]
AC_ZFn [in Categoricity]
adj_sub [in Infinity]
adj_union [in Infinity]
adj_power [in Infinity]
adj_sep [in Infinity]
adj_el [in Infinity]
AEmptyAx [in Aczel]
Aeq_equiv [in Aczel]
Aeq_ASubq [in Aczel]
Aeq_ext [in Aczel]
Aeq_tra [in Aczel]
Aeq_sym [in Aczel]
Aeq_ref' [in Aczel]
Aeq_ref [in Aczel]
Aeq_NS_eq [in Quotient_CR]
Aeq_p1_eq [in Quotient_CR]
Aeq_p1_NS_eq [in Quotient_CR]
Aeq_p1_NS [in Quotient_CR]
Aeq_eqclass [in Quotient_CE]
agree_unique [in Basics]
Ain_AWF [in Aczel]
Ain_mor [in Aczel]
Ain_pi [in Aczel]
Ain_Asup [in Aczel]
Ain_IN_NS_p1 [in Quotient_CR]
Ain_IN_p1_NS [in Quotient_CR]
Ain_IN_NS [in Quotient_CR]
Ain_IN_p1 [in Quotient_CR]
antifounded [in Permutation]
Aom_spec [in Aczel]
ApowerAx [in Aczel]
Apower_mor [in Aczel]
AreplAx [in Aczel]
Arepl_proper [in Aczel]
Arepl_proper' [in Aczel]
Arepl_mor [in Aczel]
AsepAx [in Aczel]
Asep_proper [in Aczel]
Asep_proper' [in Aczel]
Asep_mor [in Aczel]
ASubq_Subq_p1 [in Quotient_CR]
Asup_inj [in Aczel]
ATS_strength [in Quotient_TD]
ATS_universe [in Quotient_TD]
ATS_sur [in Quotient_TD]
ATS_mor [in Quotient_TD]
AunionAx [in Aczel]
Aunion_mor [in Aczel]
AupairAx [in Aczel]
Aupair_mor [in Aczel]
AWF_Aeq [in Aczel]
ax_rep' [in Truncation]

B

binunion_adj [in Infinity]
binunion_eset [in Infinity]
binunion_el [in Infinity]
bounded_small [in Basics]
bsur_rep [in Zermelo]
btot_rep [in Zermelo]
btot_power [in Zermelo]
btot_union [in Zermelo]
btot_eset [in Zermelo]
btot_bsur [in Zermelo]

C

Cantor [in Basics]
cat_ZFn [in Categoricity]
cat_card [in Categoricity]
chain_sub [in Infinity]
choice_AC [in Categoricity]
choice_ZFn [in Categoricity]
choice_el [in Categoricity]
classof_powit [in Quotient_CE]
classof_sub [in Quotient_CE]
classof_ele [in Quotient_CE]
classof_eq [in Quotient_CE]
classof_class [in Quotient_CE]
classof_ex [in Quotient_CE]
class_not_sub [in Stage]
class_eq [in Quotient_CE]
const_ZF [in Prelims]
cress [in Truncation]
cres_eq [in Basics]
cres_cl [in Prelims]
cres_equiv [in Aczel]
CR1 [in Quotient_TD]
CR2 [in Quotient_TD]
cswelled_sep [in Prelims]

D

delta_eq [in Basics]
delta_spec [in Basics]
delta_equiv [in Embeddings]
delta_equal [in Truncation]
delta'_fun [in Basics]
descAx [in Quotient_TD]
descAx1 [in Quotient_TD]
descAx2 [in Quotient_TD]
desc_p [in Truncation]
desc_nissing [in Truncation]
desc_issing [in Truncation]
domain_Stage_sub [in Zermelo]
domain_universe [in Zermelo]
domain_ZF [in Zermelo]
domain_sub [in Zermelo]
domain_el [in Zermelo]
domain_rep [in Zermelo]
domain_power [in Zermelo]
domain_union [in Zermelo]

E

elem_proper' [in Prelims]
ele_WF [in Quotient_CE]
embed_delta [in Truncation]
embed_unique [in Truncation]
emc_issing [in Truncation]
emfun_Aeq [in Quotient_CR]
empred_Aeq [in Quotient_CR]
empred_Aeq [in Quotient_CE]
emptyAx [in Permutation]
emptyE [in Quotient_CR]
emptyE [in Quotient_CE]
em_sur [in Large]
em_mor [in Large]
em_equiv [in Large]
em_rec [in Large]
em_invar [in Large]
equiv_em [in Large]
eq_equiv [in Prelims]
eset_unique [in Basics]
eset_sub [in Basics]
eset_HF [in Infinity]
Ext [in Basics]
extAx [in Permutation]
ex_rank [in Stage]

F

false [in Uncountable]
FG [in Permutation]
Fin_chain_max [in Infinity]
Fin_binunion [in Infinity]
Fin_frep [in Infinity]
Fin_rep [in Infinity]
Fin_subset [in Infinity]
FM_ZFS [in Permutation]
FM_ZS [in Permutation]
Fneq [in Permutation]
frepAx [in Permutation]
frep_el [in Basics]
frep'_el [in Basics]
fress [in Truncation]
fres_eq [in Basics]
fres_equiv [in Aczel]
F0 [in Permutation]
F1 [in Permutation]

G

GF [in Permutation]
Gneq [in Permutation]
G0 [in Permutation]
G1 [in Permutation]

H

help [in Uncountable]
HF_OM [in Infinity]
HF_rho [in Infinity]
HF_ZF [in Infinity]
HF_union [in Infinity]
HF_eset [in Infinity]
HF_ctrans [in Infinity]
HF_power [in Infinity]
HF_rep [in Infinity]
HF_Fin [in Infinity]
h_strength [in Embeddings]
h_const [in Embeddings]
h_universe [in Embeddings]
h_frep2 [in Embeddings]
h_frep1 [in Embeddings]
h_power [in Embeddings]
h_union [in Embeddings]
h_upair [in Embeddings]
h_eset [in Embeddings]
h_swelled2 [in Embeddings]
h_swelled1 [in Embeddings]
h_trans2 [in Embeddings]
h_trans1 [in Embeddings]
h_sur_sub [in Embeddings]
h_cres [in Embeddings]
h_equiv [in Embeddings]
h_sub [in Embeddings]

I

J

ji [in Zermelo]
j_dom [in Zermelo]
j_Iso [in Zermelo]

L

least_unique [in Basics]
limit_Z [in Stage]
limit_sep [in Stage]
limit_upair [in Stage]
limit_power [in Stage]
limit_union [in Stage]
limit_closed_stage [in Stage]
limit_infinite [in Infinity]
limit_OM [in Infinity]

M

MI [in Infinity]
MtoN_fun [in Zermelo]

N

nat_bool [in Aczel]
not_total_domain [in Zermelo]
not_total_exists [in Zermelo]
NS_powit [in Quotient_CR]
NS_p1_eq [in Quotient_CR]
NS_eq_Aeq_p1 [in Quotient_CR]
NTM_fres [in Embeddings]
N_eq_Aeq [in Quotient_CR]
N_idem [in Quotient_CR]

O

OM_least [in Infinity]
OM_least_limit [in Infinity]
om_infinite [in Infinity]
om_limit [in Infinity]
OM_ZF1 [in Infinity]
OM_universe [in Infinity]
OM_repclosed [in Infinity]
OM_rho_el [in Infinity]
OM_Fin [in Infinity]
OM_limit [in Infinity]
OM_stage [in Infinity]
OM_eset [in Infinity]
OM_ex_powit [in Infinity]
OM_powit [in Infinity]

P

pairAx [in Permutation]
pair_el [in Basics]
PI [in Truncation]
pi_Ain [in Aczel]
PI_eq [in Quotient_CR]
pi_sur [in Truncation]
pi_mor [in Truncation]
powerAx [in Permutation]
powerAx [in Quotient_CR]
powerAx [in Quotient_CE]
power_above [in Basics]
power_inj [in Basics]
power_mono [in Basics]
power_trans [in Basics]
power_eager [in Basics]
power_proper' [in Prelims]
power_Fin [in Infinity]
power_welldef [in Quotient_CE]
power_eqclass [in Quotient_CE]
powit_inj [in Uncountable]
powit_Fin [in Infinity]
powit_HF [in Infinity]
powit_stage [in Infinity]
pow_eset [in Infinity]
preim_equiv' [in Embeddings]
preim_equiv [in Embeddings]
P_ZF' [in Truncation]
P_Z [in Truncation]
P_WF [in Truncation]
P_Ext [in Truncation]
P_proj [in Truncation]
P_eq [in Truncation]

Q

quine [in Permutation]

R

range_universe [in Zermelo]
range_domain_small [in Zermelo]
range_domain [in Zermelo]
rank_fun [in Stage]
Rep [in Basics]
replAx [in Quotient_CR]
rep_delta [in Basics]
rep_frep [in Basics]
rep_sep [in Basics]
rep_upair [in Basics]
rep_adj [in Infinity]
rep_sing [in Infinity]
rep_eset [in Infinity]
rho_rank [in Stage]
rho_rho' [in Stage]
rho_rank_ex [in Stage]
rho'_rank [in Stage]
R_unique [in Permutation]
R'_unique [in Permutation]

S

sepAx [in Permutation]
sepAx [in Quotient_CR]
sepAx [in Quotient_CE]
sep_sub [in Basics]
sep_el [in Basics]
sep_cswelled [in Prelims]
sep_welldef [in Quotient_CE]
sep_eqclass [in Quotient_CE]
sep_false [in Truncation]
sep_true [in Truncation]
sep'_el [in Basics]
SETZF_Inf [in Quotient_CR]
SETZF_ZF' [in Quotient_CR]
SETZF_Z [in Quotient_CR]
set_not_sub [in Stage]
set_ext [in Quotient_CR]
SET_Inf [in Quotient_CE]
set_ext [in Quotient_CE]
shrink [in Truncation]
sing_union [in Basics]
sing_el [in Basics]
sing_neq [in Aczel]
sing_Aeq [in Aczel]
sing_eqcl [in Truncation]
small_red [in Basics]
Stage_Iso [in Zermelo]
Stage_btot [in Zermelo]
Stage_inhab [in Stage]
Stage_succ_limit [in Stage]
Stage_dicho [in Stage]
Stage_least [in Stage]
Stage_tricho [in Stage]
Stage_lin_el [in Stage]
Stage_lin [in Stage]
Stage_lin_succ [in Stage]
Stage_double_ind [in Stage]
Stage_inc [in Stage]
Stage_sep [in Stage]
Stage_upair [in Stage]
Stage_power [in Stage]
Stage_union [in Stage]
Stage_swelled [in Stage]
Stage_trans [in Stage]
Stage_eset [in Stage]
step [in Large]
strength_weak [in Basics]
strength_proper' [in Prelims]
subset_outside [in Basics]
sub_eset [in Basics]
sub_trans [in Basics]
sub_refl [in Basics]
swelled_sep [in Prelims]

T

tot_sur [in Zermelo]
trans_strength [in Basics]
trans_power [in Basics]
trans_strength [in Large]

U

unionAx [in Permutation]
unionAx [in Quotient_CR]
unionAx [in Quotient_CE]
union_power_eq [in Basics]
union_sub_el_sub [in Basics]
union_trans [in Basics]
union_eset [in Basics]
union_gel_eq [in Basics]
union_gel [in Basics]
union_lub [in Basics]
union_mono [in Basics]
union_trans_sub [in Basics]
union_sub [in Basics]
union_el_sub [in Basics]
union_proper' [in Prelims]
union_domain [in Zermelo]
union_welldef [in Quotient_CE]
union_eqclass [in Quotient_CE]
universe_least [in Stage]
universe_limit [in Stage]
universe_limit_frep [in Stage]
universe_limit' [in Stage]
universe_stage [in Stage]
universe_rank [in Stage]
universe_swelled [in Stage]
universe_trans [in Stage]
uni_strength [in Basics]
uni_strength [in Large]
upairAx [in Quotient_CR]
upairAx [in Quotient_CE]
upair_fun [in Basics]
upair_proper' [in Prelims]
upair_welldef [in Quotient_CE]
upair_eqclass [in Quotient_CE]
upair'_el [in Basics]
U_strength [in Large]
U_universe [in Large]

W

WF_no_loop3 [in Basics]
WF_no_loop2 [in Basics]
WF_no_loop [in Basics]
WF_sub [in Basics]
WF_model [in Permutation]
WF_ZF [in Permutation]
WF_Z [in Permutation]
WF_frep [in Permutation]
WF_sep [in Permutation]
WF_power [in Permutation]
WF_union [in Permutation]
WF_upair [in Permutation]
WF_eset [in Permutation]
WF_swelled [in Permutation]
WF_trans [in Permutation]
WF_reachable [in Stage]

X

xm_upbnd [in Stage]

Z

ZFge_cons [in Large]
ZFge0 [in Large]
ZFn_ZFw [in Large]
ZFn_cons_not_provable [in Large]
ZFSDesc [in Truncation]
ZFS_model [in Permutation]
ZF_rep [in Basics]
ZF_rep' [in Basics]
ZF_proper' [in Prelims]
ZF_ZFS [in Truncation]
Z_rep [in Basics]

Constructor Index

A

Asup [in Aczel]

F

FinA [in Infinity]
FinE [in Infinity]

H

HFI [in Infinity]

I

II [in Zermelo]

S

StageS [in Stage]
StageU [in Stage]

W

WFI [in Prelims]

Axiom Index

C

CE [in Quotient_CE]

P

PI [in Quotient_TD]
PI [in Quotient_CE]

T

tdelta [in Quotient_TD]
TDesc1 [in Quotient_TD]
TDesc2 [in Quotient_TD]

Projection Index

A

AxWF [in Prelims]

C

CR1 [in Quotient_CR]
CR2 [in Quotient_CR]

D

delta [in Prelims]
Desc1 [in Prelims]
Desc2 [in Prelims]

E

elem [in Prelims]
Eset [in Prelims]
eset [in Prelims]

F

Frep [in Prelims]
frep [in Prelims]

H

HiZ [in Prelims]
HiZF [in Prelims]
HiZF' [in Prelims]
HZ [in Prelims]
HZF [in Prelims]
HZFS [in Prelims]
HZF' [in Prelims]

M

Morph [in Prelims]

N

N [in Quotient_CR]

P

Pair [in Prelims]
PI [in Quotient_CR]
Power [in Prelims]
power [in Prelims]

S

Sep [in Prelims]
sep [in Prelims]
set [in Prelims]

U

Union [in Prelims]
union [in Prelims]
upair [in Prelims]
U_frep [in Prelims]
U_Z [in Prelims]
U_sep [in Prelims]
U_power [in Prelims]
U_union [in Prelims]
U_upair [in Prelims]
U_eset [in Prelims]
U_trans [in Prelims]

Z

ZExt [in Prelims]
ZFExt [in Prelims]
ZFExt' [in Prelims]
ZFSDesc1 [in Prelims]
ZFSDesc2 [in Prelims]
ZFset [in Prelims]
ZFset' [in Prelims]
ZFSExt [in Prelims]
ZFSFrep [in Prelims]
Zset [in Prelims]

Inductive Index

A

Acz [in Aczel]

F

Fin [in Infinity]

H

HF [in Infinity]

I

Iso [in Zermelo]

S

Stage [in Stage]

W

WF [in Prelims]

Section Index

A

AC [in Categoricity]

B

Basic [in Basics]

C

Categoricity [in Categoricity]
Cons [in Zermelo]
CR [in Quotient_CR]

D

Domain [in Zermelo]

E

Embed [in Large]

I

IMISO [in Truncation]
Inf [in Infinity]
Infinity [in Infinity]
Instance [in Permutation]
Iso [in Zermelo]

M

Main [in Zermelo]
Mor [in Embeddings]

P

Perm [in Permutation]
Proper [in Prelims]

S

Stage [in Stage]
Stages [in Zermelo]
Sub [in Truncation]

U

Uncountable [in Uncountable]
Universes [in Zermelo]

W

WF [in Permutation]

Instance Index

A

ACZ [in Quotient_TD]
Acz_ZF [in Quotient_TD]
Acz_ZF' [in Aczel]
ACZ' [in Aczel]
aeq_equiv [in Aczel]
Ain_proper [in Aczel]
Apower_proper [in Aczel]
ASubq_proper [in Aczel]
Aunion_proper [in Aczel]
Aupair_proper [in Aczel]

C

cequiv_equiv [in Prelims]

E

elem_proper [in Prelims]
equiv_equiv [in Prelims]

H

h_Proper [in Embeddings]

I

img_Proper [in Embeddings]

M

MPZF [in Truncation]
MZF [in Infinity]

N

Norm [in Quotient_TD]
N_proper [in Quotient_CR]

P

power_proper [in Prelims]

S

SET [in Quotient_TD]
SET [in Quotient_CE]
SET_ZF [in Quotient_TD]
SET_Z [in Quotient_CE]
strength_proper [in Prelims]
sub_proper [in Prelims]

U

union_proper [in Prelims]
universe_proper [in Prelims]
upair_proper [in Prelims]

Z

ZF_proper [in Prelims]

Abbreviation Index

B

binunion [in Prelims]

C

cl [in Prelims]

E

eqcl [in Prelims]

G

gel [in Prelims]

I

inhab [in Prelims]

S

sing [in Prelims]

U

upbnd [in Prelims]

Definition Index

A

AC [in Categoricity]
AczSS [in Aczel]
AczZS [in Aczel]
adj [in Infinity]
AEmpty [in Aczel]
Aeq [in Aczel]
agree [in Prelims]
Ain [in Aczel]
Aom [in Aczel]
Apower [in Aczel]
Arepl [in Aczel]
Asep [in Aczel]
ASubq [in Aczel]
ATS [in Quotient_TD]
Aunion [in Aczel]
Aupair [in Aczel]

B

bsur [in Zermelo]
btot [in Zermelo]

C

cequiv [in Prelims]
chain [in Infinity]
choice_type [in Categoricity]
class [in Quotient_CE]
classof [in Quotient_CE]
closed_rep [in Basics]
closed_frep [in Prelims]
closed_sep [in Prelims]
closed_power [in Prelims]
closed_union [in Prelims]
closed_upair [in Prelims]
closed_stage [in Stage]
const [in Prelims]
cres [in Prelims]
cswelled [in Prelims]
ctrans [in Prelims]

D

delta' [in Basics]
desc [in Quotient_TD]
desc [in Truncation]
descp [in Truncation]
domain [in Zermelo]
dom_rep [in Basics]

E

ele [in Permutation]
ele [in Quotient_CE]
em [in Large]
embed [in Truncation]
emclass [in Truncation]
emfun [in Quotient_CR]
empred [in Quotient_CR]
empred [in Quotient_CE]
empty [in Permutation]
empty [in Quotient_CE]
em' [in Large]
eqclass [in Quotient_CE]
equiv [in Prelims]
exmp [in Truncation]

F

F [in Permutation]
finpow [in Prelims]
frepl [in Permutation]
frep' [in Basics]
fres [in Prelims]
functional [in Prelims]

G

G [in Permutation]

I

i [in Zermelo]
IM [in Truncation]
img [in Embeddings]
IN [in Quotient_CR]
Inf [in Prelims]
injective [in Prelims]
iseqcl [in Prelims]
iso [in Zermelo]
issing [in Truncation]

J

j [in Zermelo]

L

least [in Prelims]
limit [in Stage]

M

M [in Uncountable]
MP [in Truncation]
MTN [in Embeddings]
MTN_fres [in Embeddings]
MtoN [in Zermelo]
M_ZF [in Permutation]
M_ZF' [in Permutation]
M_ZS [in Permutation]
M_SS [in Permutation]

N

N [in Quotient_TD]
N [in Uncountable]
NS [in Quotient_CR]
NTM [in Embeddings]
Num [in Uncountable]

O

om [in Uncountable]
OM [in Infinity]
om [in Infinity]

P

P [in Truncation]
pair [in Permutation]
parti [in Categoricity]
pi [in Truncation]
pi1 [in Aczel]
pi2 [in Aczel]
pow [in Permutation]
power [in Quotient_CE]
power' [in Quotient_CE]
powit [in Prelims]
preim [in Embeddings]
PS [in Truncation]
PZ [in Truncation]
PZF' [in Truncation]

R

R [in Permutation]
range [in Zermelo]
rank [in Stage]
reachable [in Stage]
rep [in Basics]
rep' [in Truncation]
rho [in Stage]
rho' [in Stage]
R' [in Permutation]

S

Sempty [in Quotient_CR]
sep [in Quotient_CE]
sepa [in Permutation]
sep' [in Basics]
sep' [in Quotient_CE]
SETSS [in Quotient_CR]
SETSS [in Quotient_CE]
SETZF' [in Quotient_CR]
SETZS [in Quotient_CR]
SET' [in Quotient_CR]
SET' [in Quotient_CE]
sing1 [in Aczel]
sing2 [in Aczel]
small [in Prelims]
Spower [in Quotient_CR]
Srepl [in Quotient_CR]
Ssep [in Quotient_CR]
ST [in Large]
strength [in Prelims]
sub [in Prelims]
sub [in Permutation]
sub [in Quotient_CE]
Subq [in Quotient_CR]
succ [in Stage]
Sunion [in Quotient_CR]
Supair [in Quotient_CR]
surjective [in Prelims]
swelled [in Prelims]

T

toP [in Truncation]
total [in Prelims]
trace [in Categoricity]
trans [in Prelims]

U

U [in Large]
uni [in Permutation]
union [in Quotient_CE]
union' [in Quotient_CE]
unique [in Prelims]
universe [in Prelims]
upair [in Quotient_CE]
upair' [in Basics]
upair' [in Quotient_CE]

Z

ZFge [in Prelims]
ZFn [in Prelims]
ZFw [in Prelims]

Record Index

C

closed_ZF [in Prelims]
closed_Z [in Prelims]

I

iZ [in Prelims]
iZF [in Prelims]
iZF' [in Prelims]
iZS [in Prelims]

N

Normalizer [in Quotient_CR]

S

SetStruct [in Prelims]

Z

Z [in Prelims]
ZF [in Prelims]
ZFS [in Prelims]
ZFStruct [in Prelims]
ZFStruct' [in Prelims]
ZF' [in Prelims]
ZStruct [in Prelims]

Global Index

other

(793 entries)

Notation Index

other

(10 entries)

Variable Index

other

(26 entries)

Library Index

other

(15 entries)

Lemma Index

other

(443 entries)

Constructor Index

other

(8 entries)

Axiom Index

other

(6 entries)

Projection Index

other

(48 entries)

Inductive Index

other

(6 entries)

Section Index

other

(22 entries)

Instance Index

other

(30 entries)

Abbreviation Index

other

(7 entries)

Definition Index

other

(157 entries)

Record Index

other

(15 entries)