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 (309 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 (193 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 (1 entry) 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 (9 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) 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 (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 (68 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 (15 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 (3 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 (5 entries)

# Global Index

## A

antisym [definition, in orderings]

## B

bounded [definition, in cum]
bun [definition, in sets]
bun_incl' [lemma, in sets]
bun_in [lemma, in sets]

## C

Canon [definition, in orderings]
canon_unique [lemma, in orderings]
canon_max [lemma, in orderings]
canon_simi [lemma, in orderings]
canon_simulative2 [lemma, in orderings]
canon_simulative1 [lemma, in orderings]
ccum [definition, in cum]
class [definition, in sets]
clinear [definition, in cum]
complete [definition, in cum]
complete_simi [lemma, in cum]
ctrans [definition, in cum]
cum [definition, in instances]
Cum [definition, in instances]
cum [library]
cumulative [definition, in cum]
cum_seg [lemma, in cum]
cum_least [lemma, in instances]
cum_partition [lemma, in instances]
cum_sub_not [lemma, in instances]
cum_sandwich' [lemma, in instances]
cum_sandwich [lemma, in instances]
cum_linear [lemma, in instances]
cum_wordered [lemma, in instances]
cum_WF [lemma, in instances]
Cum_cum [lemma, in instances]
cum_Cum [lemma, in instances]
cum_pow [lemma, in instances]
cum_trans [lemma, in instances]
Cum_representation [lemma, in instances]
Cum_el_trans [lemma, in instances]
Cum_unreal [lemma, in instances]
Cum_wordered [lemma, in instances]
Cum_tricho [lemma, in instances]
Cum_cumulative [lemma, in instances]
Cum_linear [lemma, in instances]
Cum_WF [lemma, in instances]
cWF [definition, in cum]

## D

des [definition, in linearity]
desc [definition, in sets]
desc_correct [lemma, in sets]
des_unique [lemma, in linearity]
des_correct [lemma, in linearity]
dom [definition, in orderings]

## E

elem [axiom, in sets]
el_bun [lemma, in sets]
el_sing [lemma, in sets]
embedding [lemma, in orderings]
Empty [axiom, in linearity]
empty [axiom, in linearity]
equiv_simi [lemma, in orderings]
eq_sing [lemma, in sets]
eset [definition, in sets]
eset_equal [lemma, in sets]
expansion [definition, in orderings]
expower [definition, in instances]
expower_WF [lemma, in instances]
expower_trans [lemma, in instances]
expower_cumulative [lemma, in instances]
expower_increasing [lemma, in instances]
exp_simi [lemma, in orderings]
exp_simulative2 [lemma, in orderings]
exp_simulative1 [lemma, in orderings]
Ext [axiom, in sets]

## F

F [definition, in instances]
f [variable, in linearity]
FI [variable, in linearity]
fpart [definition, in sets]
frep [definition, in sets]
frep_correct [lemma, in sets]
func [definition, in sets]
functional [definition, in orderings]
func_fpart [lemma, in sets]
F_unique [lemma, in instances]
F_canon_equiv [lemma, in instances]
F_simi [lemma, in instances]
F_surjective [lemma, in instances]
F_rec2 [lemma, in instances]
F_rec1 [lemma, in instances]
F_pres2 [lemma, in instances]
F_pres1 [lemma, in instances]
F_inv_func [lemma, in instances]
F_injective [lemma, in instances]
F_functional [lemma, in instances]
F_total [lemma, in instances]

## G

greatest [definition, in sets]
greatest_unique [lemma, in sets]

## I

Inc [definition, in cum]
increasing [definition, in cum]
increasing [definition, in linearity]
Inc_worder [lemma, in cum]
Inc_complete [lemma, in cum]
Inc_seg_real [lemma, in cum]
Inc_linear [lemma, in cum]
Inc_partial [lemma, in cum]
inc_seg [lemma, in cum]
inc_dom [lemma, in cum]
inhab [definition, in sets]
instances [library]
inv [definition, in orderings]
inv_sub [lemma, in orderings]
in_sing [lemma, in sets]
isomorphism [definition, in orderings]
iso_inv [lemma, in orderings]
iso_rec2 [lemma, in instances]
iso_rec1 [lemma, in instances]

## J

join [definition, in linearity]
join_union [lemma, in linearity]

## L

Least [definition, in orderings]
least [definition, in sets]
least_inhab_linear [lemma, in orderings]
least_inhab [definition, in orderings]
least_unique [lemma, in sets]
linear [definition, in orderings]
linearity [lemma, in linearity]
linearity [library]
linearity_SegB [lemma, in cum]
linear_Segs [lemma, in orderings]

## M

maxisim [definition, in orderings]
maxi_sub [lemma, in orderings]

## N

ninhab_union [lemma, in linearity]
not_inhab [lemma, in sets]

## O

Ord [definition, in instances]
orderings [library]
Ord_representation [lemma, in instances]
Ord_seg_equiv [lemma, in instances]
Ord_transitive [lemma, in instances]
Ord_el_trans [lemma, in instances]
Ord_unreal [lemma, in instances]
Ord_wordered [lemma, in instances]
Ord_tricho [lemma, in instances]
Ord_cumulative [lemma, in instances]
Ord_linear [lemma, in instances]
Ord_WF [lemma, in instances]
orealizable [definition, in cum]

## P

porder [definition, in orderings]
pow [axiom, in sets]
Power [axiom, in sets]
power_trans [lemma, in instances]
power_monotone [lemma, in sets]
power_incl' [lemma, in sets]
power_incl [lemma, in sets]

## R

realizable [definition, in sets]
realizes [definition, in sets]
realizes_unique [lemma, in linearity]
real_unreal_seg [lemma, in cum]
reflexive [definition, in orderings]
relax [lemma, in cum]
Rep [axiom, in sets]
rep [axiom, in sets]
rep_equal [lemma, in cum]
rep_rep [lemma, in cum]
rep_func [lemma, in sets]
Rep1 [definition, in sets]
Rep1_Rep2 [lemma, in sets]
Rep2 [definition, in sets]
res [definition, in orderings]
res_sub [lemma, in orderings]
res_sub2 [lemma, in orderings]
res_sub1 [lemma, in orderings]
res_seg [definition, in orderings]
Russell [lemma, in sets]

## S

SBB [constructor, in cum]
Seg [definition, in orderings]
SegB [inductive, in cum]
SegB_linearity_aux [lemma, in cum]
SegB_sub [lemma, in cum]
Segs [definition, in orderings]
seg_equal [lemma, in orderings]
seg_segs [lemma, in orderings]
seg_equiv [lemma, in cum]
Sep [axiom, in sets]
sep [axiom, in sets]
sep_rep [lemma, in sets]
sep_subc [lemma, in sets]
sep_incl' [lemma, in sets]
sep_incl [lemma, in sets]
sep_realizes [lemma, in sets]
set [axiom, in sets]
sets [definition, in linearity]
sets [library]
set_partition [lemma, in instances]
SFB [constructor, in cum]
shift [lemma, in cum]
sigma [definition, in instances]
sigma_pow [lemma, in instances]
sigma_WF [lemma, in instances]
sigma_trans [lemma, in instances]
sigma_cumulative [lemma, in instances]
sigma_increasing [lemma, in instances]
simi [definition, in orderings]
similarity [definition, in orderings]
similarity_res' [lemma, in orderings]
similarity_res [lemma, in orderings]
simi_trans [lemma, in orderings]
simi_equiv [lemma, in orderings]
simi_sub [lemma, in orderings]
simi_lin [lemma, in orderings]
simi_domain_sub [lemma, in orderings]
simi_agree [lemma, in orderings]
simi_wfounded [lemma, in orderings]
simi_res' [lemma, in orderings]
simi_res [lemma, in orderings]
simi_dom2 [lemma, in orderings]
simi_dom1 [lemma, in orderings]
simi_rewrite [lemma, in orderings]
simi_neq2 [lemma, in orderings]
simi_neq1 [lemma, in orderings]
simi_eq2 [lemma, in orderings]
simi_eq1 [lemma, in orderings]
simi_com [lemma, in orderings]
simi_simu2 [lemma, in orderings]
simi_simu1 [lemma, in orderings]
simi_inv [lemma, in orderings]
simi_realizable_iff [lemma, in cum]
simulation [definition, in orderings]
simulation_dom [lemma, in orderings]
simulative [definition, in orderings]
sing [definition, in sets]
sing_el [lemma, in cum]
sing_injective [lemma, in sets]
SLB [constructor, in cum]
step [lemma, in cum]
sub [definition, in sets]
subcc [definition, in sets]
subcs [definition, in sets]
subsc [definition, in sets]
sub_trans2 [lemma, in orderings]
sub_trans1 [lemma, in orderings]
sub_el [lemma, in cum]
sub_sing [lemma, in sets]
sub_anti [lemma, in sets]
sub_trans [lemma, in sets]
sub_refl [lemma, in sets]
sur [definition, in cum]

## T

Tower [inductive, in cum]
Tower [section, in cum]
Tower [inductive, in linearity]
tower_representation [lemma, in cum]
tower_worder [lemma, in cum]
tower_norealizable [lemma, in cum]
tower_unrealizable [lemma, in cum]
tower_cumulative [lemma, in cum]
tower_sandwich [lemma, in cum]
tower_linear [lemma, in cum]
tower_SegB [lemma, in cum]
tower_WF [lemma, in cum]
tower_trans [lemma, in cum]
tower_reach [lemma, in linearity]
Tower.f [variable, in cum]
trans [definition, in cum]
transitive [definition, in orderings]
trans_pres [definition, in cum]
trans_union [lemma, in cum]
trans_power [lemma, in instances]
TS [constructor, in cum]
TS [constructor, in linearity]
TU [constructor, in cum]
TU [constructor, in linearity]

## U

Union [axiom, in sets]
union [axiom, in sets]
union_power_eq [lemma, in sets]
union_eset_eq [lemma, in sets]
union_monotone [lemma, in sets]
union_sing_eq [lemma, in sets]
union_lub [lemma, in sets]
union_incl [lemma, in sets]
union_el_incl [lemma, in sets]
unrealizable_red [lemma, in sets]
unrealizable_new_el [lemma, in sets]
Upair [axiom, in sets]
upair [axiom, in sets]
upair_sing [lemma, in sets]
upair_injective [lemma, in sets]
upair_inr [lemma, in sets]
upair_inl [lemma, in sets]

## W

W [inductive, in orderings]
WF [inductive, in cum]
WFI [constructor, in cum]
wfounded [definition, in orderings]
WF_pres [definition, in cum]
WF_no_loop [lemma, in cum]
WF_union [lemma, in cum]
WF_pow_sub [lemma, in instances]
WF_cum_least [lemma, in instances]
WF_cum [lemma, in instances]
WI [constructor, in orderings]
worder [definition, in orderings]
wordered [definition, in cum]
worder_wfounded [lemma, in orderings]
worder_equiv [lemma, in orderings]
worder_sub [lemma, in orderings]
worder_Segs [lemma, in orderings]
worder_linear [lemma, in orderings]

## other

_ o=o _ [notation, in orderings]
_ o= _ [notation, in orderings]
_ === _ [notation, in orderings]
_ <<= _ [notation, in orderings]
_ << _ [notation, in sets]
_ <<= _ [notation, in sets]
_ <<= _ [notation, in sets]
_ <<= _ [notation, in sets]
_ <<= _ [notation, in sets]
_ el _ [notation, in sets]

# Lemma Index

## B

bun_incl' [in sets]
bun_in [in sets]

## C

canon_unique [in orderings]
canon_max [in orderings]
canon_simi [in orderings]
canon_simulative2 [in orderings]
canon_simulative1 [in orderings]
complete_simi [in cum]
cum_seg [in cum]
cum_least [in instances]
cum_partition [in instances]
cum_sub_not [in instances]
cum_sandwich' [in instances]
cum_sandwich [in instances]
cum_linear [in instances]
cum_wordered [in instances]
cum_WF [in instances]
Cum_cum [in instances]
cum_Cum [in instances]
cum_pow [in instances]
cum_trans [in instances]
Cum_representation [in instances]
Cum_el_trans [in instances]
Cum_unreal [in instances]
Cum_wordered [in instances]
Cum_tricho [in instances]
Cum_cumulative [in instances]
Cum_linear [in instances]
Cum_WF [in instances]

## D

desc_correct [in sets]
des_unique [in linearity]
des_correct [in linearity]

## E

el_bun [in sets]
el_sing [in sets]
embedding [in orderings]
equiv_simi [in orderings]
eq_sing [in sets]
eset_equal [in sets]
expower_WF [in instances]
expower_trans [in instances]
expower_cumulative [in instances]
expower_increasing [in instances]
exp_simi [in orderings]
exp_simulative2 [in orderings]
exp_simulative1 [in orderings]

## F

frep_correct [in sets]
func_fpart [in sets]
F_unique [in instances]
F_canon_equiv [in instances]
F_simi [in instances]
F_surjective [in instances]
F_rec2 [in instances]
F_rec1 [in instances]
F_pres2 [in instances]
F_pres1 [in instances]
F_inv_func [in instances]
F_injective [in instances]
F_functional [in instances]
F_total [in instances]

## G

greatest_unique [in sets]

## I

Inc_worder [in cum]
Inc_complete [in cum]
Inc_seg_real [in cum]
Inc_linear [in cum]
Inc_partial [in cum]
inc_seg [in cum]
inc_dom [in cum]
inv_sub [in orderings]
in_sing [in sets]
iso_inv [in orderings]
iso_rec2 [in instances]
iso_rec1 [in instances]

## J

join_union [in linearity]

## L

least_inhab_linear [in orderings]
least_unique [in sets]
linearity [in linearity]
linearity_SegB [in cum]
linear_Segs [in orderings]

## M

maxi_sub [in orderings]

## N

ninhab_union [in linearity]
not_inhab [in sets]

## O

Ord_representation [in instances]
Ord_seg_equiv [in instances]
Ord_transitive [in instances]
Ord_el_trans [in instances]
Ord_unreal [in instances]
Ord_wordered [in instances]
Ord_tricho [in instances]
Ord_cumulative [in instances]
Ord_linear [in instances]
Ord_WF [in instances]

## P

power_trans [in instances]
power_monotone [in sets]
power_incl' [in sets]
power_incl [in sets]

## R

realizes_unique [in linearity]
real_unreal_seg [in cum]
relax [in cum]
rep_equal [in cum]
rep_rep [in cum]
rep_func [in sets]
Rep1_Rep2 [in sets]
res_sub [in orderings]
res_sub2 [in orderings]
res_sub1 [in orderings]
Russell [in sets]

## S

SegB_linearity_aux [in cum]
SegB_sub [in cum]
seg_equal [in orderings]
seg_segs [in orderings]
seg_equiv [in cum]
sep_rep [in sets]
sep_subc [in sets]
sep_incl' [in sets]
sep_incl [in sets]
sep_realizes [in sets]
set_partition [in instances]
shift [in cum]
sigma_pow [in instances]
sigma_WF [in instances]
sigma_trans [in instances]
sigma_cumulative [in instances]
sigma_increasing [in instances]
similarity_res' [in orderings]
similarity_res [in orderings]
simi_trans [in orderings]
simi_equiv [in orderings]
simi_sub [in orderings]
simi_lin [in orderings]
simi_domain_sub [in orderings]
simi_agree [in orderings]
simi_wfounded [in orderings]
simi_res' [in orderings]
simi_res [in orderings]
simi_dom2 [in orderings]
simi_dom1 [in orderings]
simi_rewrite [in orderings]
simi_neq2 [in orderings]
simi_neq1 [in orderings]
simi_eq2 [in orderings]
simi_eq1 [in orderings]
simi_com [in orderings]
simi_simu2 [in orderings]
simi_simu1 [in orderings]
simi_inv [in orderings]
simi_realizable_iff [in cum]
simulation_dom [in orderings]
sing_el [in cum]
sing_injective [in sets]
step [in cum]
sub_trans2 [in orderings]
sub_trans1 [in orderings]
sub_el [in cum]
sub_sing [in sets]
sub_anti [in sets]
sub_trans [in sets]
sub_refl [in sets]

## T

tower_representation [in cum]
tower_worder [in cum]
tower_norealizable [in cum]
tower_unrealizable [in cum]
tower_cumulative [in cum]
tower_sandwich [in cum]
tower_linear [in cum]
tower_SegB [in cum]
tower_WF [in cum]
tower_trans [in cum]
tower_reach [in linearity]
trans_union [in cum]
trans_power [in instances]

## U

union_power_eq [in sets]
union_eset_eq [in sets]
union_monotone [in sets]
union_sing_eq [in sets]
union_lub [in sets]
union_incl [in sets]
union_el_incl [in sets]
unrealizable_red [in sets]
unrealizable_new_el [in sets]
upair_sing [in sets]
upair_injective [in sets]
upair_inr [in sets]
upair_inl [in sets]

## W

WF_no_loop [in cum]
WF_union [in cum]
WF_pow_sub [in instances]
WF_cum_least [in instances]
WF_cum [in instances]
worder_wfounded [in orderings]
worder_equiv [in orderings]
worder_sub [in orderings]
worder_Segs [in orderings]
worder_linear [in orderings]

Tower [in cum]

# Constructor Index

SBB [in cum]
SFB [in cum]
SLB [in cum]

## T

TS [in cum]
TS [in linearity]
TU [in cum]
TU [in linearity]

## W

WFI [in cum]
WI [in orderings]

# Notation Index

## other

_ o=o _ [in orderings]
_ o= _ [in orderings]
_ === _ [in orderings]
_ <<= _ [in orderings]
_ << _ [in sets]
_ <<= _ [in sets]
_ <<= _ [in sets]
_ <<= _ [in sets]
_ <<= _ [in sets]
_ el _ [in sets]

# Inductive Index

SegB [in cum]

## T

Tower [in cum]
Tower [in linearity]

W [in orderings]
WF [in cum]

# Definition Index

## A

antisym [in orderings]

bounded [in cum]
bun [in sets]

## C

Canon [in orderings]
ccum [in cum]
class [in sets]
clinear [in cum]
complete [in cum]
ctrans [in cum]
cum [in instances]
Cum [in instances]
cumulative [in cum]
cWF [in cum]

## D

des [in linearity]
desc [in sets]
dom [in orderings]

## E

eset [in sets]
expansion [in orderings]
expower [in instances]

## F

F [in instances]
fpart [in sets]
frep [in sets]
func [in sets]
functional [in orderings]

## G

greatest [in sets]

## I

Inc [in cum]
increasing [in cum]
increasing [in linearity]
inhab [in sets]
inv [in orderings]
isomorphism [in orderings]

## J

join [in linearity]

## L

Least [in orderings]
least [in sets]
least_inhab [in orderings]
linear [in orderings]

## M

maxisim [in orderings]

## O

Ord [in instances]
orealizable [in cum]

## P

porder [in orderings]

## R

realizable [in sets]
realizes [in sets]
reflexive [in orderings]
Rep1 [in sets]
Rep2 [in sets]
res [in orderings]
res_seg [in orderings]

## S

Seg [in orderings]
Segs [in orderings]
sets [in linearity]
sigma [in instances]
simi [in orderings]
similarity [in orderings]
simulation [in orderings]
simulative [in orderings]
sing [in sets]
sub [in sets]
subcc [in sets]
subcs [in sets]
subsc [in sets]
sur [in cum]

## T

trans [in cum]
transitive [in orderings]
trans_pres [in cum]

## W

wfounded [in orderings]
WF_pres [in cum]
worder [in orderings]
wordered [in cum]

# Axiom Index

## E

elem [in sets]
Empty [in linearity]
empty [in linearity]
Ext [in sets]

pow [in sets]
Power [in sets]

Rep [in sets]
rep [in sets]

Sep [in sets]
sep [in sets]
set [in sets]

Union [in sets]
union [in sets]
Upair [in sets]
upair [in sets]

# Variable Index

## F

f [in linearity]
FI [in linearity]

Tower.f [in cum]

# Library Index

cum

instances

linearity

orderings

## S

sets

 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 (309 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 (193 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 (1 entry) 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 (9 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) 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 (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 (68 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 (15 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 (3 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 (5 entries)