| 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]
Section Index
T
Tower [in cum]Constructor Index
S
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
S
SegB [in cum]T
Tower [in cum]Tower [in linearity]
W
W [in orderings]WF [in cum]
Definition Index
A
antisym [in orderings]B
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]
P
pow [in sets]Power [in sets]
R
Rep [in sets]rep [in sets]
S
Sep [in sets]sep [in sets]
set [in sets]
U
Union [in sets]union [in sets]
Upair [in sets]
upair [in sets]
Variable Index
F
f [in linearity]FI [in linearity]
T
Tower.f [in cum]Library Index
C
cumI
instancesL
linearityO
orderingsS
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) |
This page has been generated by coqdoc