| 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 | (276 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 | (10 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 | (17 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 | (9 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 | (148 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 | (4 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 | (4 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 | (17 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 | (3 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 | (10 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 | (3 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 | (48 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 | (3 entries) |
Global Index
A
agree [definition, in Model]agree_unique [lemma, in ST]
AxWF [projection, in Model]
B
Basic [section, in ST]_ ! _ [notation, in ST]
bounded_small [lemma, in ST]
bsur [definition, in Embedding]
bsur_rep [lemma, in Embedding]
btot [definition, in Embedding]
btot_rep [lemma, in Embedding]
btot_power [lemma, in Embedding]
btot_union [lemma, in Embedding]
btot_eset [lemma, in Embedding]
btot_bsur [lemma, in Embedding]
C
Cantor [lemma, in ST]Categoricity [section, in Categoricity]
Categoricity [library]
Categoricity.F [variable, in Categoricity]
Categoricity.FG [variable, in Categoricity]
Categoricity.G [variable, in Categoricity]
Categoricity.GF [variable, in Categoricity]
class_not_sub [lemma, in ST]
closed_rep' [definition, in Stage]
closed_rep [definition, in Stage]
closed_stage [definition, in Stage]
closed_sep [definition, in Stage]
closed_upair [definition, in Stage]
closed_power [definition, in Stage]
closed_union [definition, in Stage]
Cons [section, in Embedding]
D
delta [definition, in ST]delta_spec [lemma, in ST]
delta_eq [lemma, in ST]
Domain [section, in Embedding]
domain [definition, in Embedding]
domain_Stage_sub [lemma, in Embedding]
domain_universe [lemma, in Embedding]
domain_sub [lemma, in Embedding]
domain_el [lemma, in Embedding]
domain_rep [lemma, in Embedding]
domain_power [lemma, in Embedding]
domain_union [lemma, in Embedding]
E
elem [projection, in Model]embed [definition, in Instances]
Embedding [library]
embed_fun [lemma, in Instances]
Eset [projection, in Model]
eset [projection, in Model]
eset_unique [lemma, in ST]
eset_sub [lemma, in ST]
Ext [projection, in Model]
ex_rank [lemma, in Stage]
F
false [lemma, in Uncountable]frep [definition, in ST]
frep_el [lemma, in ST]
functional [definition, in Model]
G
gel [abbreviation, in Model]H
help [lemma, in Uncountable]I
i [definition, in Embedding]II [constructor, in Embedding]
ij [lemma, in Embedding]
IM [definition, in Instances]
IM_ZF [lemma, in Instances]
IM_universe [lemma, in Minimality]
inhab [abbreviation, in Model]
inhab_neq [lemma, in ST]
inhab_not [lemma, in ST]
injective [definition, in Model]
Instances [library]
Iso [section, in Embedding]
Iso [inductive, in Embedding]
Iso_bijective_ZFn [lemma, in ZFn]
Iso_Un [lemma, in ZFn]
Iso_bijective_equipotent [lemma, in Categoricity]
Iso_bijective_minimal [lemma, in Minimality]
Iso_tricho [lemma, in Embedding]
Iso_max [lemma, in Embedding]
Iso_Stage_max [lemma, in Embedding]
Iso_universe [lemma, in Embedding]
Iso_closed_rep [lemma, in Embedding]
Iso_closed_power [lemma, in Embedding]
Iso_closed_union [lemma, in Embedding]
Iso_trans [lemma, in Embedding]
Iso_Stage [lemma, in Embedding]
Iso_dom' [lemma, in Embedding]
Iso_dom [lemma, in Embedding]
Iso_rep [lemma, in Embedding]
Iso_power [lemma, in Embedding]
Iso_union [lemma, in Embedding]
Iso_eset [lemma, in Embedding]
Iso_mem [lemma, in Embedding]
Iso_inj [lemma, in Embedding]
Iso_res [lemma, in Embedding]
Iso_fun [lemma, in Embedding]
Iso_bsur [lemma, in Embedding]
Iso_btot [lemma, in Embedding]
Iso_sym [lemma, in Embedding]
i_ran [lemma, in Embedding]
i_Iso [lemma, in Embedding]
J
j [definition, in Embedding]ji [lemma, in Embedding]
j_dom [lemma, in Embedding]
j_Iso [lemma, in Embedding]
L
least [definition, in ST]least_unique [lemma, in ST]
limit [definition, 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]
M
M [definition, in Uncountable]M [axiom, in Embedding]
minimal [definition, in Minimality]
Minimality [library]
minimality_cons [lemma, in Minimality]
Model [library]
MtoN [definition, in Embedding]
MtoN_fun [lemma, in Embedding]
MZF [axiom, in Embedding]
N
N [definition, in Uncountable]N [axiom, in Embedding]
not_total_domain [lemma, in Embedding]
not_total_exists [lemma, in Embedding]
Num [definition, in Uncountable]
NZF [axiom, in Embedding]
P
P [definition, in Instances]PI [lemma, in Instances]
Power [projection, in Model]
power [projection, in Model]
power_above [lemma, in ST]
power_inj [lemma, in ST]
power_mono [lemma, in ST]
power_WF [lemma, in ST]
power_trans [lemma, in ST]
power_eager [lemma, in ST]
pseudo_rep_neg [lemma, in Instances]
pseudo_rep_fun [lemma, in Instances]
pseudo_rep [definition, in Instances]
p_rep [projection, in Instances]
p_power [projection, in Instances]
p_union [projection, in Instances]
p_eset [projection, in Instances]
p_trans [projection, in Instances]
R
range [definition, in Embedding]range_domain_small [lemma, in Embedding]
range_domain [lemma, in Embedding]
rank [definition, in Stage]
rank_fun [lemma, in Stage]
reachable [definition, in Stage]
Rep [projection, in Model]
rep [projection, in Model]
rep_closed_equiv [lemma, in Stage]
res [definition, in Instances]
res_fun [lemma, in Instances]
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]
S
sep [definition, in ST]sep_false [lemma, in ST]
sep_true [lemma, in ST]
sep_sub [lemma, in ST]
sep_el [lemma, in ST]
set [projection, in Model]
SetStruct [record, in Model]
set_not_sub [lemma, in ST]
sing [definition, in ST]
sing_union [lemma, in ST]
sing_el [lemma, in ST]
small [definition, in Model]
small_red [lemma, in ST]
ST [library]
Stage [inductive, in Stage]
Stage [section, in Stage]
Stage [library]
StageS [constructor, in Stage]
Stages [section, in Embedding]
StageU [constructor, in Stage]
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]
Stage_Iso [lemma, in Embedding]
Stage_btot [lemma, in Embedding]
sub [definition, in Model]
Sub [section, in Instances]
subset_outside [lemma, in ST]
sub_eset [lemma, in ST]
sub_trans [lemma, in ST]
sub_refl [lemma, in ST]
Sub.p [variable, in Instances]
Sub.PC [variable, in Instances]
Sub.set [variable, in Instances]
Sub.set_ZF [variable, in Instances]
succ [definition, in Stage]
surjective [definition, in Model]
swelled [definition, in Model]
T
total [definition, in Model]tot_sur [lemma, in Embedding]
trans [definition, in Model]
trans_power [lemma, in ST]
U
Un [definition, in ZFn]Uncountable [section, in Uncountable]
Uncountable [library]
Uncountable.f [variable, in Uncountable]
Uncountable.f_sur [variable, in Uncountable]
Uncountable.ident [variable, in Uncountable]
Uncountable.Inf [variable, in Uncountable]
Uncountable.num [variable, in Uncountable]
Uncountable.num_inj [variable, in Uncountable]
Uncountable.omega [variable, in Uncountable]
Uncountable.set [variable, in Uncountable]
Uncountable.ZFS [variable, in Uncountable]
Union [projection, in Model]
union [projection, in Model]
union_power_eq [lemma, in ST]
union_sub_el_sub [lemma, in ST]
union_trans [lemma, in ST]
union_eset [lemma, in ST]
union_gel_eq [lemma, in ST]
union_gel [lemma, in ST]
union_lub [lemma, in ST]
union_mono [lemma, in ST]
union_trans_sub [lemma, in ST]
union_sub [lemma, in ST]
union_el_sub [lemma, in ST]
union_domain [lemma, in Embedding]
unique [definition, in ST]
unis [definition, in ZFn]
universe [definition, in Stage]
Universes [section, in Embedding]
universe_limit [lemma, in Stage]
universe_stage [lemma, in Stage]
universe_rank [lemma, in Stage]
universe_ZF_closed [lemma, in Stage]
universe_swelled [lemma, in Stage]
universe_trans [lemma, in Stage]
upair [definition, in ST]
upair_el [lemma, in ST]
upair_fun [lemma, in ST]
upbnd [abbreviation, in Model]
W
WF [inductive, in Model]WFI [constructor, in Model]
WF_no_loop3 [lemma, in ST]
WF_no_loop2 [lemma, in ST]
WF_no_loop [lemma, in ST]
WF_reachable [lemma, in Stage]
X
xm_upbnd [lemma, in Stage]Z
ZF [record, in Model]ZFn [library]
ZF_closed [record, in Instances]
other
_ <=s _ [notation, in Model]_ <=c _ [notation, in Model]
_ <=p _ [notation, in Model]
_ << _ [notation, in Model]
_ <<= _ [notation, in Model]
_ nel _ [notation, in Model]
_ el _ [notation, in Model]
_ ! _ [notation, in ST]
0 [notation, in Model]
Notation Index
B
_ ! _ [in ST]other
_ <=s _ [in Model]_ <=c _ [in Model]
_ <=p _ [in Model]
_ << _ [in Model]
_ <<= _ [in Model]
_ nel _ [in Model]
_ el _ [in Model]
_ ! _ [in ST]
0 [in Model]
Variable Index
C
Categoricity.F [in Categoricity]Categoricity.FG [in Categoricity]
Categoricity.G [in Categoricity]
Categoricity.GF [in Categoricity]
S
Sub.p [in Instances]Sub.PC [in Instances]
Sub.set [in Instances]
Sub.set_ZF [in Instances]
U
Uncountable.f [in Uncountable]Uncountable.f_sur [in Uncountable]
Uncountable.ident [in Uncountable]
Uncountable.Inf [in Uncountable]
Uncountable.num [in Uncountable]
Uncountable.num_inj [in Uncountable]
Uncountable.omega [in Uncountable]
Uncountable.set [in Uncountable]
Uncountable.ZFS [in Uncountable]
Library Index
C
CategoricityE
EmbeddingI
InstancesM
MinimalityModel
S
STStage
U
UncountableZ
ZFnLemma Index
A
agree_unique [in ST]B
bounded_small [in ST]bsur_rep [in Embedding]
btot_rep [in Embedding]
btot_power [in Embedding]
btot_union [in Embedding]
btot_eset [in Embedding]
btot_bsur [in Embedding]
C
Cantor [in ST]class_not_sub [in ST]
D
delta_spec [in ST]delta_eq [in ST]
domain_Stage_sub [in Embedding]
domain_universe [in Embedding]
domain_sub [in Embedding]
domain_el [in Embedding]
domain_rep [in Embedding]
domain_power [in Embedding]
domain_union [in Embedding]
E
embed_fun [in Instances]eset_unique [in ST]
eset_sub [in ST]
ex_rank [in Stage]
F
false [in Uncountable]frep_el [in ST]
H
help [in Uncountable]I
ij [in Embedding]IM_ZF [in Instances]
IM_universe [in Minimality]
inhab_neq [in ST]
inhab_not [in ST]
Iso_bijective_ZFn [in ZFn]
Iso_Un [in ZFn]
Iso_bijective_equipotent [in Categoricity]
Iso_bijective_minimal [in Minimality]
Iso_tricho [in Embedding]
Iso_max [in Embedding]
Iso_Stage_max [in Embedding]
Iso_universe [in Embedding]
Iso_closed_rep [in Embedding]
Iso_closed_power [in Embedding]
Iso_closed_union [in Embedding]
Iso_trans [in Embedding]
Iso_Stage [in Embedding]
Iso_dom' [in Embedding]
Iso_dom [in Embedding]
Iso_rep [in Embedding]
Iso_power [in Embedding]
Iso_union [in Embedding]
Iso_eset [in Embedding]
Iso_mem [in Embedding]
Iso_inj [in Embedding]
Iso_res [in Embedding]
Iso_fun [in Embedding]
Iso_bsur [in Embedding]
Iso_btot [in Embedding]
Iso_sym [in Embedding]
i_ran [in Embedding]
i_Iso [in Embedding]
J
ji [in Embedding]j_dom [in Embedding]
j_Iso [in Embedding]
L
least_unique [in ST]limit_sep [in Stage]
limit_upair [in Stage]
limit_power [in Stage]
limit_union [in Stage]
limit_closed_stage [in Stage]
M
minimality_cons [in Minimality]MtoN_fun [in Embedding]
N
not_total_domain [in Embedding]not_total_exists [in Embedding]
P
PI [in Instances]power_above [in ST]
power_inj [in ST]
power_mono [in ST]
power_WF [in ST]
power_trans [in ST]
power_eager [in ST]
pseudo_rep_neg [in Instances]
pseudo_rep_fun [in Instances]
R
range_domain_small [in Embedding]range_domain [in Embedding]
rank_fun [in Stage]
rep_closed_equiv [in Stage]
res_fun [in Instances]
rho_rank [in Stage]
rho_rho' [in Stage]
rho_rank_ex [in Stage]
rho'_rank [in Stage]
S
sep_false [in ST]sep_true [in ST]
sep_sub [in ST]
sep_el [in ST]
set_not_sub [in ST]
sing_union [in ST]
sing_el [in ST]
small_red [in ST]
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]
Stage_Iso [in Embedding]
Stage_btot [in Embedding]
subset_outside [in ST]
sub_eset [in ST]
sub_trans [in ST]
sub_refl [in ST]
T
tot_sur [in Embedding]trans_power [in ST]
U
union_power_eq [in ST]union_sub_el_sub [in ST]
union_trans [in ST]
union_eset [in ST]
union_gel_eq [in ST]
union_gel [in ST]
union_lub [in ST]
union_mono [in ST]
union_trans_sub [in ST]
union_sub [in ST]
union_el_sub [in ST]
union_domain [in Embedding]
universe_limit [in Stage]
universe_stage [in Stage]
universe_rank [in Stage]
universe_ZF_closed [in Stage]
universe_swelled [in Stage]
universe_trans [in Stage]
upair_el [in ST]
upair_fun [in ST]
W
WF_no_loop3 [in ST]WF_no_loop2 [in ST]
WF_no_loop [in ST]
WF_reachable [in Stage]
X
xm_upbnd [in Stage]Constructor Index
I
II [in Embedding]S
StageS [in Stage]StageU [in Stage]
W
WFI [in Model]Axiom Index
M
M [in Embedding]MZF [in Embedding]
N
N [in Embedding]NZF [in Embedding]
Projection Index
A
AxWF [in Model]E
elem [in Model]Eset [in Model]
eset [in Model]
Ext [in Model]
P
Power [in Model]power [in Model]
p_rep [in Instances]
p_power [in Instances]
p_union [in Instances]
p_eset [in Instances]
p_trans [in Instances]
R
Rep [in Model]rep [in Model]
S
set [in Model]U
Union [in Model]union [in Model]
Inductive Index
I
Iso [in Embedding]S
Stage [in Stage]W
WF [in Model]Section Index
B
Basic [in ST]C
Categoricity [in Categoricity]Cons [in Embedding]
D
Domain [in Embedding]I
Iso [in Embedding]S
Stage [in Stage]Stages [in Embedding]
Sub [in Instances]
U
Uncountable [in Uncountable]Universes [in Embedding]
Abbreviation Index
G
gel [in Model]I
inhab [in Model]U
upbnd [in Model]Definition Index
A
agree [in Model]B
bsur [in Embedding]btot [in Embedding]
C
closed_rep' [in Stage]closed_rep [in Stage]
closed_stage [in Stage]
closed_sep [in Stage]
closed_upair [in Stage]
closed_power [in Stage]
closed_union [in Stage]
D
delta [in ST]domain [in Embedding]
E
embed [in Instances]F
frep [in ST]functional [in Model]
I
i [in Embedding]IM [in Instances]
injective [in Model]
J
j [in Embedding]L
least [in ST]limit [in Stage]
M
M [in Uncountable]minimal [in Minimality]
MtoN [in Embedding]
N
N [in Uncountable]Num [in Uncountable]
P
P [in Instances]pseudo_rep [in Instances]
R
range [in Embedding]rank [in Stage]
reachable [in Stage]
res [in Instances]
rho [in Stage]
rho' [in Stage]
S
sep [in ST]sing [in ST]
small [in Model]
sub [in Model]
succ [in Stage]
surjective [in Model]
swelled [in Model]
T
total [in Model]trans [in Model]
U
Un [in ZFn]unique [in ST]
unis [in ZFn]
universe [in Stage]
upair [in ST]
Record Index
S
SetStruct [in Model]Z
ZF [in Model]ZF_closed [in Instances]
| 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 | (276 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 | (10 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 | (17 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 | (9 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 | (148 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 | (4 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 | (4 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 | (17 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 | (3 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 | (10 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 | (3 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 | (48 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 | (3 entries) |