| 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 | (395 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 | (21 entries) |
| Module 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 | (2 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 | (60 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 | (4 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 | (208 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 | (5 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 | (12 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) |
| 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 | (1 entry) |
| 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 | (18 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 | (7 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 | (53 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 | (1 entry) |
Global Index
A
allU [lemma, in libs.fset]all_inP [lemma, in libs.base]
all_subP [lemma, in libs.fset]
all_fset0 [lemma, in libs.fset]
all_fset1 [lemma, in libs.fset]
AutoLemmas [section, in libs.fset]
AutoLemmas.T [variable, in libs.fset]
AutoLemmas.T' [variable, in libs.fset]
B
base [library]bcase [library]
bigU1 [lemma, in libs.fset]
big_sep [lemma, in libs.fset]
bounded [definition, in libs.fset]
C
cardSmC [lemma, in libs.base]classic_orb [lemma, in libs.base]
connect_inP [lemma, in libs.fset]
connect_in_trans [lemma, in libs.fset]
connect_in1 [lemma, in libs.fset]
connect_in0 [lemma, in libs.fset]
connect_in [definition, in libs.fset]
const [definition, in libs.fset]
contraN [lemma, in libs.base]
contraP [lemma, in libs.base]
cupP [lemma, in libs.fset]
curry [definition, in libs.base]
curryE [lemma, in libs.base]
D
del [definition, in libs.base]dist [definition, in libs.base]
Dist [section, in libs.base]
distP [lemma, in libs.base]
distS [lemma, in libs.base]
dist_ltn [lemma, in libs.base]
Dist.T [variable, in libs.base]
Dist.Tgt0 [variable, in libs.base]
dist0 [lemma, in libs.base]
E
edone [library]elements [projection, in libs.fset]
emptyPn [lemma, in libs.fset]
eqEsub [lemma, in libs.fset]
eqF [lemma, in libs.base]
Extensionality [section, in libs.fset]
Extensionality.T [variable, in libs.fset]
ex_dist [lemma, in libs.base]
ex_max [lemma, in libs.fset]
F
fdisj [definition, in libs.fset]feqEsub [definition, in libs.fset]
filter_subset [lemma, in libs.base]
fimsetP [lemma, in libs.fset]
fimsetS [lemma, in libs.fset]
fimsetU [lemma, in libs.fset]
fimsetU1 [lemma, in libs.fset]
fImset_spec [constructor, in libs.fset]
fimset_def [abbreviation, in libs.fset]
fimset0 [lemma, in libs.fset]
fimset1 [lemma, in libs.fset]
fimset2P [lemma, in libs.fset]
fimset2_spec [inductive, in libs.fset]
fimset2_def [abbreviation, in libs.fset]
Fimset3 [section, in libs.fset]
fimset3 [definition, in libs.fset]
fimset3P [lemma, in libs.fset]
fImset3_spec [constructor, in libs.fset]
fimset3_spec [inductive, in libs.fset]
Fimset3.A [variable, in libs.fset]
Fimset3.aT1 [variable, in libs.fset]
Fimset3.aT2 [variable, in libs.fset]
Fimset3.aT3 [variable, in libs.fset]
Fimset3.B [variable, in libs.fset]
Fimset3.C [variable, in libs.fset]
Fimset3.f [variable, in libs.fset]
Fimset3.rT [variable, in libs.fset]
FinSets [section, in libs.fset]
FinSets.T [variable, in libs.fset]
fin_choices [lemma, in libs.base]
fin_choice [lemma, in libs.base]
fin_choice_aux [lemma, in libs.base]
Fixpoints [section, in libs.fset]
Fixpoints.F [variable, in libs.fset]
Fixpoints.F_bound [variable, in libs.fset]
Fixpoints.F_mono [variable, in libs.fset]
Fixpoints.T [variable, in libs.fset]
Fixpoints.U [variable, in libs.fset]
flattenP [lemma, in libs.base]
fNopick [constructor, in libs.fset]
fPick [constructor, in libs.fset]
fpick [definition, in libs.fset]
fpickP [lemma, in libs.fset]
fpick_spec [inductive, in libs.fset]
fproperU [lemma, in libs.fset]
fproper1 [lemma, in libs.fset]
fseq [definition, in libs.fset]
fseq_axiom [lemma, in libs.fset]
fseq_uniq [lemma, in libs.fset]
fseq_perm_eq [lemma, in libs.fset]
fset [definition, in libs.fset]
Fset [module, in libs.fset]
Fset [constructor, in libs.fset]
fset [library]
fsetCK [definition, in libs.fset]
FsetConnect [section, in libs.fset]
FsetConnect.e [variable, in libs.fset]
FsetConnect.S [variable, in libs.fset]
FsetConnect.T [variable, in libs.fset]
fsetD [definition, in libs.fset]
fsetDS [lemma, in libs.fset]
fsetDSS [lemma, in libs.fset]
fsetD0 [lemma, in libs.fset]
fsetE [lemma, in libs.fset]
fsetI [definition, in libs.fset]
fsetIA [lemma, in libs.fset]
fsetIC [lemma, in libs.fset]
fsetIUl [lemma, in libs.fset]
fsetIUr [lemma, in libs.fset]
fsetI0 [lemma, in libs.fset]
fsetSU [lemma, in libs.fset]
fsetT [definition, in libs.fset]
FsetType [module, in libs.fset]
FsetType.fimset [axiom, in libs.fset]
FsetType.fimsetE [axiom, in libs.fset]
FsetType.fimset2 [axiom, in libs.fset]
FsetType.fimset2E [axiom, in libs.fset]
FsetType.fsetU [axiom, in libs.fset]
FsetType.fsetUE [axiom, in libs.fset]
FsetType.fset0E [axiom, in libs.fset]
FsetType.fset0_ [axiom, in libs.fset]
FsetType.fset1 [axiom, in libs.fset]
FsetType.fset1E [axiom, in libs.fset]
FsetType.sep [axiom, in libs.fset]
FsetType.sepE [axiom, in libs.fset]
fsetUA [lemma, in libs.fset]
fsetUC [lemma, in libs.fset]
fsetUCA [lemma, in libs.fset]
fsetUD [lemma, in libs.fset]
fsetUD1 [lemma, in libs.fset]
fsetUIl [lemma, in libs.fset]
fsetUIr [lemma, in libs.fset]
fsetUP [lemma, in libs.fset]
fsetUS [lemma, in libs.fset]
fsetUSU [lemma, in libs.fset]
fsetU_auto4 [lemma, in libs.fset]
fsetU_auto3 [lemma, in libs.fset]
fsetU_auto2 [lemma, in libs.fset]
fsetU_auto1 [lemma, in libs.fset]
fsetU_comlaw [definition, in libs.fset]
fsetU_law [definition, in libs.fset]
fsetU_def [abbreviation, in libs.fset]
fsetU0 [lemma, in libs.fset]
fsetU1P [lemma, in libs.fset]
fsetX [definition, in libs.fset]
fsetXP [lemma, in libs.fset]
fset_ext [lemma, in libs.fset]
fset_eq [lemma, in libs.fset]
fset_subCountType [definition, in libs.fset]
fset_countType [definition, in libs.fset]
fset_choiceType [definition, in libs.fset]
fset_predType [definition, in libs.fset]
fset_eqType [definition, in libs.fset]
fset_subType [definition, in libs.fset]
fset_of [definition, in libs.fset]
fset_type [record, in libs.fset]
fset_axiom [definition, in libs.fset]
Fset.fimset [definition, in libs.fset]
Fset.fimsetE [lemma, in libs.fset]
Fset.fimset2 [definition, in libs.fset]
Fset.fimset2E [lemma, in libs.fset]
Fset.fsetU [definition, in libs.fset]
Fset.fsetUE [lemma, in libs.fset]
Fset.fset0E [lemma, in libs.fset]
Fset.fset0_ [definition, in libs.fset]
Fset.fset1 [definition, in libs.fset]
Fset.fset1E [lemma, in libs.fset]
Fset.sep [definition, in libs.fset]
Fset.sepE [lemma, in libs.fset]
fset0 [abbreviation, in libs.fset]
fset0Es [lemma, in libs.fset]
fset0F [lemma, in libs.fset]
fset0I [lemma, in libs.fset]
fset0U [lemma, in libs.fset]
fset0Vmem [lemma, in libs.fset]
fset0_def [abbreviation, in libs.fset]
fset1Es [lemma, in libs.fset]
fset1F [lemma, in libs.fset]
fset1U [lemma, in libs.fset]
fset1U1 [lemma, in libs.fset]
fset1_def [abbreviation, in libs.fset]
fset11 [lemma, in libs.fset]
fsizeU [lemma, in libs.fset]
fsizeU1 [lemma, in libs.fset]
fsubDl [lemma, in libs.fset]
fsubIl [lemma, in libs.fset]
fsubIr [lemma, in libs.fset]
fsubsetU [lemma, in libs.fset]
fsubUl [lemma, in libs.fset]
fsubUr [lemma, in libs.fset]
fsubUset [lemma, in libs.fset]
fsubUsetP [lemma, in libs.fset]
fsubU_auto [lemma, in libs.fset]
fsub1 [lemma, in libs.fset]
fsub1_auto [lemma, in libs.fset]
fsum [definition, in libs.fset]
FSum [section, in libs.fset]
fsumD [lemma, in libs.fset]
fsumDsub [lemma, in libs.fset]
fsumI [lemma, in libs.fset]
fsumID [lemma, in libs.fset]
fsumS [lemma, in libs.fset]
fsumU [lemma, in libs.fset]
fsum_const1 [lemma, in libs.fset]
fsum_replace [lemma, in libs.fset]
fsum_sub [lemma, in libs.fset]
fsum_eq0 [lemma, in libs.fset]
fsum_const [lemma, in libs.fset]
FSum.T [variable, in libs.fset]
FSum.w [variable, in libs.fset]
fsum0 [lemma, in libs.fset]
fsum1 [lemma, in libs.fset]
funiq [lemma, in libs.fset]
G
gfp [definition, in libs.base]gfp [definition, in libs.fset]
gfpE [lemma, in libs.base]
gfpE [lemma, in libs.fset]
gfp_ind2 [lemma, in libs.base]
gfp_ind [lemma, in libs.base]
gfp_ind [lemma, in libs.fset]
gfp_ind_aux [lemma, in libs.fset]
GreatestFixPoint [section, in libs.base]
GreatestFixpoint [section, in libs.fset]
GreatestFixpoint.bounded_F' [variable, in libs.fset]
GreatestFixPoint.F [variable, in libs.base]
GreatestFixpoint.F [variable, in libs.fset]
GreatestFixPoint.F_mono [variable, in libs.base]
GreatestFixpoint.F_bound [variable, in libs.fset]
GreatestFixpoint.F_mono [variable, in libs.fset]
GreatestFixPoint.F' [variable, in libs.base]
GreatestFixpoint.F' [variable, in libs.fset]
GreatestFixpoint.mono_F' [variable, in libs.fset]
GreatestFixPoint.T [variable, in libs.base]
GreatestFixpoint.T [variable, in libs.fset]
GreatestFixpoint.U [variable, in libs.fset]
~` _ [notation, in libs.fset]
H
hasS [lemma, in libs.base]has_fset0 [lemma, in libs.fset]
has_fset1 [lemma, in libs.fset]
I
inE [definition, in libs.fset]injective2 [definition, in libs.fset]
in_sub_all [lemma, in libs.base]
in_sub_has [lemma, in libs.base]
in_fsetT [lemma, in libs.fset]
in_fsetX [lemma, in libs.fset]
in_fimset2F [lemma, in libs.fset]
in_fimset2 [lemma, in libs.fset]
in_fimset [lemma, in libs.fset]
in_fset [definition, in libs.fset]
in_fset1 [lemma, in libs.fset]
in_fset0 [lemma, in libs.fset]
in_fsetI [lemma, in libs.fset]
in_fsetD [lemma, in libs.fset]
in_fsetU [lemma, in libs.fset]
in_sep [lemma, in libs.fset]
iterFbound [lemma, in libs.fset]
iterFsub [lemma, in libs.base]
iterFsub [lemma, in libs.fset]
iterFsubn [lemma, in libs.base]
iterFsub1 [lemma, in libs.fset]
iter_fix [lemma, in libs.base]
iter_fix [lemma, in libs.fset]
L
LeastFixPoint [section, in libs.base]LeastFixPoint.F [variable, in libs.base]
LeastFixPoint.monoF [variable, in libs.base]
LeastFixPoint.T [variable, in libs.base]
level_max [lemma, in libs.fset]
level1 [lemma, in libs.fset]
level2 [lemma, in libs.fset]
levl [definition, in libs.fset]
lfp [definition, in libs.base]
lfp [definition, in libs.fset]
lfpE [lemma, in libs.base]
lfpE [lemma, in libs.fset]
lfp_ind [lemma, in libs.base]
lfp_level_aux [lemma, in libs.fset]
lfp_ind [lemma, in libs.fset]
lfp_ind_aux [lemma, in libs.fset]
M
mask_inj [lemma, in libs.base]maximal [definition, in libs.fset]
Maximal [section, in libs.fset]
maximalb [definition, in libs.fset]
maximalP [lemma, in libs.fset]
Maximal.P [variable, in libs.fset]
Maximal.T [variable, in libs.fset]
Maximal.U [variable, in libs.fset]
mem_fimset3 [lemma, in libs.fset]
mem_fimset2 [lemma, in libs.fset]
mono [definition, in libs.base]
monotone [definition, in libs.fset]
mono_F' [lemma, in libs.base]
N
nat_size_ind [lemma, in libs.fset]next [definition, in libs.base]
next_subproof [lemma, in libs.base]
nilp_map [lemma, in libs.base]
O
OperationsTheory [section, in libs.fset]OperationsTheory.A [variable, in libs.fset]
OperationsTheory.aT1 [variable, in libs.fset]
OperationsTheory.aT2 [variable, in libs.fset]
OperationsTheory.aT3 [variable, in libs.fset]
OperationsTheory.B [variable, in libs.fset]
OperationsTheory.C [variable, in libs.fset]
OperationsTheory.Laws [section, in libs.fset]
OperationsTheory.Laws.X [variable, in libs.fset]
OperationsTheory.Laws.Y [variable, in libs.fset]
OperationsTheory.Laws.Z [variable, in libs.fset]
OperationsTheory.T [variable, in libs.fset]
OperationsTheory.T' [variable, in libs.fset]
orS [lemma, in libs.base]
P
Pick [section, in libs.fset]Pick.p [variable, in libs.fset]
Pick.T [variable, in libs.fset]
Pick.X [variable, in libs.fset]
powerset [definition, in libs.fset]
powersetE [lemma, in libs.fset]
powersetP [lemma, in libs.fset]
powersetU [lemma, in libs.fset]
powerset_size [lemma, in libs.fset]
power_mon [lemma, in libs.fset]
power_sub [lemma, in libs.fset]
proper [definition, in libs.fset]
properD1 [lemma, in libs.fset]
properE [lemma, in libs.fset]
properEneq [lemma, in libs.fset]
properW [lemma, in libs.fset]
proper_size [lemma, in libs.fset]
pruneE [lemma, in libs.fset]
prune_sub [lemma, in libs.fset]
prune_ind [lemma, in libs.fset]
Pruning [section, in libs.fset]
Pruning.p [variable, in libs.fset]
Pruning.T [variable, in libs.fset]
R
restrict [definition, in libs.fset]S
sepS [lemma, in libs.fset]sepU [lemma, in libs.fset]
sep_sep [lemma, in libs.fset]
sep_sub [lemma, in libs.fset]
sep_def [abbreviation, in libs.fset]
sep0 [lemma, in libs.fset]
sep1 [lemma, in libs.fset]
SetOfSeq [section, in libs.fset]
SetOfSeq.T [variable, in libs.fset]
set_op [definition, in libs.base]
set_of_nilp [lemma, in libs.fset]
set_of_uniq [lemma, in libs.fset]
set_ofE [lemma, in libs.fset]
set_of [definition, in libs.fset]
Size [section, in libs.fset]
sizes_eq0 [lemma, in libs.fset]
sizes0 [lemma, in libs.fset]
size_del [lemma, in libs.base]
size_of_uniq [lemma, in libs.fset]
size_sep [lemma, in libs.fset]
size_gt0P [lemma, in libs.fset]
Size.T [variable, in libs.fset]
slack_ind [lemma, in libs.fset]
subP [lemma, in libs.fset]
subPn [lemma, in libs.fset]
subsep [lemma, in libs.fset]
subset [definition, in libs.fset]
subset_size [lemma, in libs.fset]
subsize_eq [lemma, in libs.fset]
subxx [lemma, in libs.fset]
subx0 [lemma, in libs.fset]
sub_all_dom [lemma, in libs.base]
sub_power [lemma, in libs.fset]
sub_trans [lemma, in libs.fset]
sub0x [lemma, in libs.fset]
sumn_bound [lemma, in libs.base]
U
unique_dist [lemma, in libs.base]W
wf_leq [lemma, in libs.fset]other
{ fset _ } (type_scope) [notation, in libs.fset]_ `x` _ [notation, in libs.fset]
_ |` _ [notation, in libs.fset]
_ `@` _ [notation, in libs.fset]
_ `<` _ [notation, in libs.fset]
_ `<=` _ [notation, in libs.fset]
_ `\` _ [notation, in libs.fset]
_ `&` _ [notation, in libs.fset]
_ `|` _ [notation, in libs.fset]
[ fset _ | _ <- _ , _ <- _ , _ <- _ ] [notation, in libs.fset]
[ fset _ | _ <- _ , _ <- _ ] [notation, in libs.fset]
[ fset _ | _ <- _ ] [notation, in libs.fset]
[ some _ in _ , _ ] [notation, in libs.fset]
[ all _ in _ , _ ] [notation, in libs.fset]
[ fset _ , _ , .. , _ & _ ] [notation, in libs.fset]
[ fset _ ; _ ; .. ; _ ] [notation, in libs.fset]
[ fset _ ] [notation, in libs.fset]
[ fset _ in _ | _ ] [notation, in libs.fset]
\bigcup_( _ in _ ) _ [notation, in libs.fset]
\bigcup_( _ in _ | _ ) _ [notation, in libs.fset]
Notation Index
G
~` _ [in libs.fset]other
{ fset _ } (type_scope) [in libs.fset]_ `x` _ [in libs.fset]
_ |` _ [in libs.fset]
_ `@` _ [in libs.fset]
_ `<` _ [in libs.fset]
_ `<=` _ [in libs.fset]
_ `\` _ [in libs.fset]
_ `&` _ [in libs.fset]
_ `|` _ [in libs.fset]
[ fset _ | _ <- _ , _ <- _ , _ <- _ ] [in libs.fset]
[ fset _ | _ <- _ , _ <- _ ] [in libs.fset]
[ fset _ | _ <- _ ] [in libs.fset]
[ some _ in _ , _ ] [in libs.fset]
[ all _ in _ , _ ] [in libs.fset]
[ fset _ , _ , .. , _ & _ ] [in libs.fset]
[ fset _ ; _ ; .. ; _ ] [in libs.fset]
[ fset _ ] [in libs.fset]
[ fset _ in _ | _ ] [in libs.fset]
\bigcup_( _ in _ ) _ [in libs.fset]
\bigcup_( _ in _ | _ ) _ [in libs.fset]
Module Index
F
Fset [in libs.fset]FsetType [in libs.fset]
Variable Index
A
AutoLemmas.T [in libs.fset]AutoLemmas.T' [in libs.fset]
D
Dist.T [in libs.base]Dist.Tgt0 [in libs.base]
E
Extensionality.T [in libs.fset]F
Fimset3.A [in libs.fset]Fimset3.aT1 [in libs.fset]
Fimset3.aT2 [in libs.fset]
Fimset3.aT3 [in libs.fset]
Fimset3.B [in libs.fset]
Fimset3.C [in libs.fset]
Fimset3.f [in libs.fset]
Fimset3.rT [in libs.fset]
FinSets.T [in libs.fset]
Fixpoints.F [in libs.fset]
Fixpoints.F_bound [in libs.fset]
Fixpoints.F_mono [in libs.fset]
Fixpoints.T [in libs.fset]
Fixpoints.U [in libs.fset]
FsetConnect.e [in libs.fset]
FsetConnect.S [in libs.fset]
FsetConnect.T [in libs.fset]
FSum.T [in libs.fset]
FSum.w [in libs.fset]
G
GreatestFixpoint.bounded_F' [in libs.fset]GreatestFixPoint.F [in libs.base]
GreatestFixpoint.F [in libs.fset]
GreatestFixPoint.F_mono [in libs.base]
GreatestFixpoint.F_bound [in libs.fset]
GreatestFixpoint.F_mono [in libs.fset]
GreatestFixPoint.F' [in libs.base]
GreatestFixpoint.F' [in libs.fset]
GreatestFixpoint.mono_F' [in libs.fset]
GreatestFixPoint.T [in libs.base]
GreatestFixpoint.T [in libs.fset]
GreatestFixpoint.U [in libs.fset]
L
LeastFixPoint.F [in libs.base]LeastFixPoint.monoF [in libs.base]
LeastFixPoint.T [in libs.base]
M
Maximal.P [in libs.fset]Maximal.T [in libs.fset]
Maximal.U [in libs.fset]
O
OperationsTheory.A [in libs.fset]OperationsTheory.aT1 [in libs.fset]
OperationsTheory.aT2 [in libs.fset]
OperationsTheory.aT3 [in libs.fset]
OperationsTheory.B [in libs.fset]
OperationsTheory.C [in libs.fset]
OperationsTheory.Laws.X [in libs.fset]
OperationsTheory.Laws.Y [in libs.fset]
OperationsTheory.Laws.Z [in libs.fset]
OperationsTheory.T [in libs.fset]
OperationsTheory.T' [in libs.fset]
P
Pick.p [in libs.fset]Pick.T [in libs.fset]
Pick.X [in libs.fset]
Pruning.p [in libs.fset]
Pruning.T [in libs.fset]
S
SetOfSeq.T [in libs.fset]Size.T [in libs.fset]
Library Index
B
basebcase
E
edoneF
fsetLemma Index
A
allU [in libs.fset]all_inP [in libs.base]
all_subP [in libs.fset]
all_fset0 [in libs.fset]
all_fset1 [in libs.fset]
B
bigU1 [in libs.fset]big_sep [in libs.fset]
C
cardSmC [in libs.base]classic_orb [in libs.base]
connect_inP [in libs.fset]
connect_in_trans [in libs.fset]
connect_in1 [in libs.fset]
connect_in0 [in libs.fset]
contraN [in libs.base]
contraP [in libs.base]
cupP [in libs.fset]
curryE [in libs.base]
D
distP [in libs.base]distS [in libs.base]
dist_ltn [in libs.base]
dist0 [in libs.base]
E
emptyPn [in libs.fset]eqEsub [in libs.fset]
eqF [in libs.base]
ex_dist [in libs.base]
ex_max [in libs.fset]
F
filter_subset [in libs.base]fimsetP [in libs.fset]
fimsetS [in libs.fset]
fimsetU [in libs.fset]
fimsetU1 [in libs.fset]
fimset0 [in libs.fset]
fimset1 [in libs.fset]
fimset2P [in libs.fset]
fimset3P [in libs.fset]
fin_choices [in libs.base]
fin_choice [in libs.base]
fin_choice_aux [in libs.base]
flattenP [in libs.base]
fpickP [in libs.fset]
fproperU [in libs.fset]
fproper1 [in libs.fset]
fseq_axiom [in libs.fset]
fseq_uniq [in libs.fset]
fseq_perm_eq [in libs.fset]
fsetDS [in libs.fset]
fsetDSS [in libs.fset]
fsetD0 [in libs.fset]
fsetE [in libs.fset]
fsetIA [in libs.fset]
fsetIC [in libs.fset]
fsetIUl [in libs.fset]
fsetIUr [in libs.fset]
fsetI0 [in libs.fset]
fsetSU [in libs.fset]
fsetUA [in libs.fset]
fsetUC [in libs.fset]
fsetUCA [in libs.fset]
fsetUD [in libs.fset]
fsetUD1 [in libs.fset]
fsetUIl [in libs.fset]
fsetUIr [in libs.fset]
fsetUP [in libs.fset]
fsetUS [in libs.fset]
fsetUSU [in libs.fset]
fsetU_auto4 [in libs.fset]
fsetU_auto3 [in libs.fset]
fsetU_auto2 [in libs.fset]
fsetU_auto1 [in libs.fset]
fsetU0 [in libs.fset]
fsetU1P [in libs.fset]
fsetXP [in libs.fset]
fset_ext [in libs.fset]
fset_eq [in libs.fset]
Fset.fimsetE [in libs.fset]
Fset.fimset2E [in libs.fset]
Fset.fsetUE [in libs.fset]
Fset.fset0E [in libs.fset]
Fset.fset1E [in libs.fset]
Fset.sepE [in libs.fset]
fset0Es [in libs.fset]
fset0F [in libs.fset]
fset0I [in libs.fset]
fset0U [in libs.fset]
fset0Vmem [in libs.fset]
fset1Es [in libs.fset]
fset1F [in libs.fset]
fset1U [in libs.fset]
fset1U1 [in libs.fset]
fset11 [in libs.fset]
fsizeU [in libs.fset]
fsizeU1 [in libs.fset]
fsubDl [in libs.fset]
fsubIl [in libs.fset]
fsubIr [in libs.fset]
fsubsetU [in libs.fset]
fsubUl [in libs.fset]
fsubUr [in libs.fset]
fsubUset [in libs.fset]
fsubUsetP [in libs.fset]
fsubU_auto [in libs.fset]
fsub1 [in libs.fset]
fsub1_auto [in libs.fset]
fsumD [in libs.fset]
fsumDsub [in libs.fset]
fsumI [in libs.fset]
fsumID [in libs.fset]
fsumS [in libs.fset]
fsumU [in libs.fset]
fsum_const1 [in libs.fset]
fsum_replace [in libs.fset]
fsum_sub [in libs.fset]
fsum_eq0 [in libs.fset]
fsum_const [in libs.fset]
fsum0 [in libs.fset]
fsum1 [in libs.fset]
funiq [in libs.fset]
G
gfpE [in libs.base]gfpE [in libs.fset]
gfp_ind2 [in libs.base]
gfp_ind [in libs.base]
gfp_ind [in libs.fset]
gfp_ind_aux [in libs.fset]
H
hasS [in libs.base]has_fset0 [in libs.fset]
has_fset1 [in libs.fset]
I
in_sub_all [in libs.base]in_sub_has [in libs.base]
in_fsetT [in libs.fset]
in_fsetX [in libs.fset]
in_fimset2F [in libs.fset]
in_fimset2 [in libs.fset]
in_fimset [in libs.fset]
in_fset1 [in libs.fset]
in_fset0 [in libs.fset]
in_fsetI [in libs.fset]
in_fsetD [in libs.fset]
in_fsetU [in libs.fset]
in_sep [in libs.fset]
iterFbound [in libs.fset]
iterFsub [in libs.base]
iterFsub [in libs.fset]
iterFsubn [in libs.base]
iterFsub1 [in libs.fset]
iter_fix [in libs.base]
iter_fix [in libs.fset]
L
level_max [in libs.fset]level1 [in libs.fset]
level2 [in libs.fset]
lfpE [in libs.base]
lfpE [in libs.fset]
lfp_ind [in libs.base]
lfp_level_aux [in libs.fset]
lfp_ind [in libs.fset]
lfp_ind_aux [in libs.fset]
M
mask_inj [in libs.base]maximalP [in libs.fset]
mem_fimset3 [in libs.fset]
mem_fimset2 [in libs.fset]
mono_F' [in libs.base]
N
nat_size_ind [in libs.fset]next_subproof [in libs.base]
nilp_map [in libs.base]
O
orS [in libs.base]P
powersetE [in libs.fset]powersetP [in libs.fset]
powersetU [in libs.fset]
powerset_size [in libs.fset]
power_mon [in libs.fset]
power_sub [in libs.fset]
properD1 [in libs.fset]
properE [in libs.fset]
properEneq [in libs.fset]
properW [in libs.fset]
proper_size [in libs.fset]
pruneE [in libs.fset]
prune_sub [in libs.fset]
prune_ind [in libs.fset]
S
sepS [in libs.fset]sepU [in libs.fset]
sep_sep [in libs.fset]
sep_sub [in libs.fset]
sep0 [in libs.fset]
sep1 [in libs.fset]
set_of_nilp [in libs.fset]
set_of_uniq [in libs.fset]
set_ofE [in libs.fset]
sizes_eq0 [in libs.fset]
sizes0 [in libs.fset]
size_del [in libs.base]
size_of_uniq [in libs.fset]
size_sep [in libs.fset]
size_gt0P [in libs.fset]
slack_ind [in libs.fset]
subP [in libs.fset]
subPn [in libs.fset]
subsep [in libs.fset]
subset_size [in libs.fset]
subsize_eq [in libs.fset]
subxx [in libs.fset]
subx0 [in libs.fset]
sub_all_dom [in libs.base]
sub_power [in libs.fset]
sub_trans [in libs.fset]
sub0x [in libs.fset]
sumn_bound [in libs.base]
U
unique_dist [in libs.base]W
wf_leq [in libs.fset]Constructor Index
F
fImset_spec [in libs.fset]fImset3_spec [in libs.fset]
fNopick [in libs.fset]
fPick [in libs.fset]
Fset [in libs.fset]
Axiom Index
F
FsetType.fimset [in libs.fset]FsetType.fimsetE [in libs.fset]
FsetType.fimset2 [in libs.fset]
FsetType.fimset2E [in libs.fset]
FsetType.fsetU [in libs.fset]
FsetType.fsetUE [in libs.fset]
FsetType.fset0E [in libs.fset]
FsetType.fset0_ [in libs.fset]
FsetType.fset1 [in libs.fset]
FsetType.fset1E [in libs.fset]
FsetType.sep [in libs.fset]
FsetType.sepE [in libs.fset]
Inductive Index
F
fimset2_spec [in libs.fset]fimset3_spec [in libs.fset]
fpick_spec [in libs.fset]
Projection Index
E
elements [in libs.fset]Section Index
A
AutoLemmas [in libs.fset]D
Dist [in libs.base]E
Extensionality [in libs.fset]F
Fimset3 [in libs.fset]FinSets [in libs.fset]
Fixpoints [in libs.fset]
FsetConnect [in libs.fset]
FSum [in libs.fset]
G
GreatestFixPoint [in libs.base]GreatestFixpoint [in libs.fset]
L
LeastFixPoint [in libs.base]M
Maximal [in libs.fset]O
OperationsTheory [in libs.fset]OperationsTheory.Laws [in libs.fset]
P
Pick [in libs.fset]Pruning [in libs.fset]
S
SetOfSeq [in libs.fset]Size [in libs.fset]
Abbreviation Index
F
fimset_def [in libs.fset]fimset2_def [in libs.fset]
fsetU_def [in libs.fset]
fset0 [in libs.fset]
fset0_def [in libs.fset]
fset1_def [in libs.fset]
S
sep_def [in libs.fset]Definition Index
B
bounded [in libs.fset]C
connect_in [in libs.fset]const [in libs.fset]
curry [in libs.base]
D
del [in libs.base]dist [in libs.base]
F
fdisj [in libs.fset]feqEsub [in libs.fset]
fimset3 [in libs.fset]
fpick [in libs.fset]
fseq [in libs.fset]
fset [in libs.fset]
fsetCK [in libs.fset]
fsetD [in libs.fset]
fsetI [in libs.fset]
fsetT [in libs.fset]
fsetU_comlaw [in libs.fset]
fsetU_law [in libs.fset]
fsetX [in libs.fset]
fset_subCountType [in libs.fset]
fset_countType [in libs.fset]
fset_choiceType [in libs.fset]
fset_predType [in libs.fset]
fset_eqType [in libs.fset]
fset_subType [in libs.fset]
fset_of [in libs.fset]
fset_axiom [in libs.fset]
Fset.fimset [in libs.fset]
Fset.fimset2 [in libs.fset]
Fset.fsetU [in libs.fset]
Fset.fset0_ [in libs.fset]
Fset.fset1 [in libs.fset]
Fset.sep [in libs.fset]
fsum [in libs.fset]
G
gfp [in libs.base]gfp [in libs.fset]
I
inE [in libs.fset]injective2 [in libs.fset]
in_fset [in libs.fset]
L
levl [in libs.fset]lfp [in libs.base]
lfp [in libs.fset]
M
maximal [in libs.fset]maximalb [in libs.fset]
mono [in libs.base]
monotone [in libs.fset]
N
next [in libs.base]P
powerset [in libs.fset]proper [in libs.fset]
R
restrict [in libs.fset]S
set_op [in libs.base]set_of [in libs.fset]
subset [in libs.fset]
Record Index
F
fset_type [in libs.fset]| 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 | (395 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 | (21 entries) |
| Module 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 | (2 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 | (60 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 | (4 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 | (208 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 | (5 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 | (12 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) |
| 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 | (1 entry) |
| 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 | (18 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 | (7 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 | (53 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 | (1 entry) |
This page has been generated by coqdoc