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

(951 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

(20 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

(3 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

(135 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

(28 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

(170 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

(36 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

(19 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

(54 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

(28 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

(91 entries)

Instance 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

(129 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

(206 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

(32 entries)

---

Global Index

A

absorb [projection, in interfaces.lattice_interface]
absorb [constructor, in interfaces.lattice_interface]
Absorption [record, in interfaces.lattice_interface]
Absorption [inductive, in interfaces.lattice_interface]
absorption_andb_orb [instance, in interfaces.lattice_examples]
absorption_orb_andb [instance, in interfaces.lattice_examples]
absorption_max_min [projection, in interfaces.lattice_interface]
absorption_min_max [projection, in interfaces.lattice_interface]
add_top.A [variable, in misc.ordered]
add_top [section, in misc.ordered]
all [definition, in misc.dec_fset]
all_decidable [instance, in misc.dec_fset]
all_elim [lemma, in misc.dec_fset]
all_intro [lemma, in misc.dec_fset]
alternative_definition [section, in subobjects.k_finite]
and_false [definition, in interfaces.lattice_examples]
and_true [definition, in interfaces.lattice_examples]
Antisymmetric [record, in misc.ordered]
Antisymmetric [inductive, in misc.ordered]
antisymmetry [projection, in misc.ordered]
antisymmetry [constructor, in misc.ordered]
AP [definition, in interfaces.lattice_examples]
append_comm [lemma, in list_representation.properties]
append_singleton [lemma, in list_representation.properties]
append_assoc [lemma, in list_representation.properties]
append_nr [lemma, in list_representation.properties]
append_nl [definition, in list_representation.properties]
append_union [lemma, in implementations.lists]
append_union [lemma, in list_representation.isomorphism]
ap_equiv [lemma, in prelude]
ap_inl_path_sum_inl [lemma, in prelude]
Associative [record, in interfaces.lattice_interface]
Associative [inductive, in interfaces.lattice_interface]
associative_max [projection, in interfaces.lattice_interface]
associative_min [projection, in interfaces.lattice_interface]
associative_max_js [projection, in interfaces.lattice_interface]
associativity [projection, in interfaces.lattice_interface]
associativity [constructor, in interfaces.lattice_interface]

B

bad [library]
Bfin [definition, in subobjects.b_finite]
bfin_union [lemma, in subobjects.b_finite]
bfin_to_kfin_sub [definition, in subobjects.b_finite]
bfin_to_kfin [lemma, in subobjects.b_finite]
bfin_kfin [section, in subobjects.b_finite]
Bfin_no_singletons [section, in subobjects.b_finite]
binary_operation.n [variable, in interfaces.lattice_interface]
binary_operation.g [variable, in interfaces.lattice_interface]
binary_operation.f [variable, in interfaces.lattice_interface]
binary_operation.A [variable, in interfaces.lattice_interface]
binary_operation [section, in interfaces.lattice_interface]
bind [projection, in interfaces.monad_interface]
bind_isIn [lemma, in kuratowski.properties]
bind_neutral_r [projection, in interfaces.monad_interface]
bind_neutral_l [projection, in interfaces.monad_interface]
bind_assoc [projection, in interfaces.monad_interface]
bishop_projective [instance, in misc.projective]
BoolLattice [section, in interfaces.lattice_examples]
botAP [instance, in interfaces.lattice_examples]
bottom [record, in interfaces.lattice_interface]
bottom [inductive, in interfaces.lattice_interface]
bottom_bool [instance, in interfaces.lattice_examples]
bottom_view [instance, in interfaces.set_interface]
bot_fun [instance, in interfaces.lattice_examples]
b_fin_projective [section, in misc.projective]
b_finite [library]

C

closedEmpty [definition, in subobjects.sub]
closedIntersection [definition, in subobjects.sub]
closedSingleton [definition, in subobjects.sub]
closedUnion [definition, in subobjects.sub]
Commutative [record, in interfaces.lattice_interface]
Commutative [inductive, in interfaces.lattice_interface]
commutative_max [projection, in interfaces.lattice_interface]
commutative_min [projection, in interfaces.lattice_interface]
commutative_max_js [projection, in interfaces.lattice_interface]
commutativity [projection, in interfaces.lattice_interface]
commutativity [constructor, in interfaces.lattice_interface]
comm' [definition, in list_representation.isomorphism]
comprehension_all [lemma, in kuratowski.properties]
comprehension_or [lemma, in kuratowski.properties]
comprehension_subset [lemma, in kuratowski.properties]
comprehension_false [lemma, in kuratowski.properties]
comprehension_properties [section, in kuratowski.properties]
comprehension_isIn_d [lemma, in kuratowski.properties]
comprehension_isIn [lemma, in kuratowski.properties]
comprehension_union [lemma, in kuratowski.properties]
concatD [definition, in subobjects.enumerated]
corollary_5_7 [definition, in CPP]
CPP [library]

D

DecidableMembership [instance, in subobjects.b_finite]
DecidableToMerely [instance, in prelude]
decidable_eq_pauli [instance, in misc.dec_fset]
decidable_A_intersect [lemma, in subobjects.sub]
decidable_A_isIn [lemma, in subobjects.sub]
decidable_equality [section, in misc.dec_kuratowski]
decidable_empty_finite [definition, in subobjects.b_finite]
dec_memb_list [instance, in implementations.lists]
dec_memb [instance, in implementations.lists]
dec_eq [section, in kuratowski.properties]
dec_length [lemma, in misc.dec_kuratowski]
dec_decidable_equality [definition, in misc.dec_kuratowski]
dec_subset [definition, in misc.dec_kuratowski]
dec_intersection [lemma, in misc.dec_kuratowski]
dec_membership [definition, in misc.dec_kuratowski]
dec_membership.A [variable, in subobjects.b_finite]
dec_membership [section, in subobjects.b_finite]
dec_kuratowski [library]
dec_fset [library]
dec_lem [library]
definition_5_8 [definition, in CPP]
definition_5_2 [definition, in CPP]
definition_5_1 [definition, in CPP]
definition_4_19 [definition, in CPP]
definition_4_14 [definition, in CPP]
definition_4_13 [definition, in CPP]
definition_4_5 [definition, in CPP]
definition_4_4 [definition, in CPP]
definition_4_3 [definition, in CPP]
definition_4_1 [definition, in CPP]
definition_3_8 [definition, in CPP]
definition_3_7 [definition, in CPP]
definition_3_3 [definition, in CPP]
definition_2_7 [definition, in CPP]
definition_2_4 [definition, in CPP]
definition_2_2 [definition, in CPP]
definition_2_1 [definition, in CPP]
difference [definition, in kuratowski.operations]
difference_isIn_d [lemma, in kuratowski.properties]
disjoint [definition, in kuratowski.length]
disjoint_summants [lemma, in kuratowski.length]
disjoint_sub [lemma, in kuratowski.length]
disjoint_difference [lemma, in kuratowski.length]
disjoint_sum [definition, in kuratowski.operations]
dist₁ [definition, in interfaces.lattice_examples]
dist₂ [definition, in interfaces.lattice_examples]
dupl' [definition, in list_representation.isomorphism]

E

el [definition, in subobjects.b_finite]
empty [projection, in interfaces.lattice_interface]
empty [constructor, in interfaces.lattice_interface]
empty [projection, in interfaces.set_names]
empty [constructor, in interfaces.set_names]
empty [section, in subobjects.b_finite]
empty_min [definition, in misc.ordered]
empty_empty [definition, in implementations.lists]
empty_isIn_d [definition, in kuratowski.properties]
empty_isIn [definition, in kuratowski.properties]
Empty_Projective [instance, in misc.projective]
empty_finite [definition, in subobjects.b_finite]
empty_isIn [definition, in interfaces.set_interface]
empty.A [variable, in subobjects.b_finite]
empty.X [variable, in subobjects.b_finite]
empty.Xequiv [variable, in subobjects.b_finite]
enumerated [definition, in subobjects.enumerated]
enumerated [library]
enumeratedS [definition, in subobjects.enumerated]
enumeratedS_to_FSet [definition, in subobjects.enumerated]
enumeratedS_union [lemma, in subobjects.enumerated]
enumeratedS_singleton [lemma, in subobjects.enumerated]
enumeratedS_empty [lemma, in subobjects.enumerated]
enumerated_Kf [lemma, in subobjects.enumerated]
enumerated_fset.A [variable, in subobjects.enumerated]
enumerated_fset [section, in subobjects.enumerated]
enumerated_prod [lemma, in subobjects.enumerated]
enumerated_sum [lemma, in subobjects.enumerated]
enumerated_surj [lemma, in subobjects.enumerated]
enumerated_comprehension [lemma, in subobjects.enumerated]
equiv_definition [lemma, in subobjects.k_finite]
equiv_pathspace_T [definition, in misc.dec_lem]
equiv_subset1_r [lemma, in kuratowski.extensionality]
equiv_subset1_l [lemma, in kuratowski.extensionality]
eq_subset [lemma, in kuratowski.extensionality]
eq_subset2 [lemma, in kuratowski.extensionality]
eq_subset1 [lemma, in kuratowski.extensionality]
example_4_20 [definition, in CPP]
exist [definition, in misc.dec_fset]
exists_isIn [section, in misc.dec_fset]
exist_elim [lemma, in implementations.lists]
exist_isIn [lemma, in misc.dec_fset]
exist_decidable [instance, in misc.dec_fset]
exist_elim [lemma, in misc.dec_fset]
exist_intro [lemma, in misc.dec_fset]
ext [lemma, in kuratowski.properties]
ext [section, in kuratowski.extensionality]
extensionality [library]

F

f [definition, in misc.bad]
filter [projection, in interfaces.set_names]
filter [constructor, in interfaces.set_names]
filterD [definition, in subobjects.enumerated]
filterD_lookup [lemma, in subobjects.enumerated]
filterD_cons_no [lemma, in subobjects.enumerated]
filterD_cons [lemma, in subobjects.enumerated]
filter_comprehension [lemma, in implementations.lists]
filter_isIn [definition, in interfaces.set_interface]
finite_hott.A [variable, in subobjects.b_finite]
finite_hott [section, in subobjects.b_finite]
fmap_isIn_d_inj [lemma, in kuratowski.properties]
fmap_isIn_inj [lemma, in kuratowski.properties]
fmap_Surjection [instance, in kuratowski.properties]
fmap_isIn [lemma, in kuratowski.properties]
fmap_inr [lemma, in kuratowski.length]
fmap_inl [lemma, in kuratowski.length]
fmap_compose [projection, in interfaces.monad_interface]
from_squash [definition, in prelude]
FSet [module, in misc.bad]
FSet [module, in kuratowski.kuratowski_sets]
FSetC [module, in list_representation.list_representation]
FSetC_to_FSet [definition, in list_representation.isomorphism]
fsetc_singleton [instance, in list_representation.operations]
fsetc_union [instance, in list_representation.operations]
FSetC.Cns [constructor, in list_representation.list_representation]
FSetC.comm_s [axiom, in list_representation.list_representation]
FSetC.dupl [axiom, in list_representation.list_representation]
FSetC.FSetC [inductive, in list_representation.list_representation]
FSetC.FSetC [section, in list_representation.list_representation]
FSetC.FSetC_prim_rec [definition, in list_representation.list_representation]
FSetC.FSetC_prim_recursion.commP [variable, in list_representation.list_representation]
FSetC.FSetC_prim_recursion.duplP [variable, in list_representation.list_representation]
FSetC.FSetC_prim_recursion.cns [variable, in list_representation.list_representation]
FSetC.FSetC_prim_recursion.nil [variable, in list_representation.list_representation]
FSetC.FSetC_prim_recursion.H [variable, in list_representation.list_representation]
FSetC.FSetC_prim_recursion.P [variable, in list_representation.list_representation]
FSetC.FSetC_prim_recursion.A [variable, in list_representation.list_representation]
FSetC.FSetC_prim_recursion [section, in list_representation.list_representation]
FSetC.FSetC_recursion [instance, in list_representation.list_representation]
FSetC.FSetC_rec [definition, in list_representation.list_representation]
FSetC.FSetC_recursion.commP [variable, in list_representation.list_representation]
FSetC.FSetC_recursion.duplP [variable, in list_representation.list_representation]
FSetC.FSetC_recursion.cns [variable, in list_representation.list_representation]
FSetC.FSetC_recursion.nil [variable, in list_representation.list_representation]
FSetC.FSetC_recursion.H [variable, in list_representation.list_representation]
FSetC.FSetC_recursion.P [variable, in list_representation.list_representation]
FSetC.FSetC_recursion.A [variable, in list_representation.list_representation]
FSetC.FSetC_recursion [section, in list_representation.list_representation]
FSetC.FSetC_ind [definition, in list_representation.list_representation]
FSetC.FSetC_induction.commP [variable, in list_representation.list_representation]
FSetC.FSetC_induction.duplP [variable, in list_representation.list_representation]
FSetC.FSetC_induction.cnsP [variable, in list_representation.list_representation]
FSetC.FSetC_induction.eP [variable, in list_representation.list_representation]
FSetC.FSetC_induction.H [variable, in list_representation.list_representation]
FSetC.FSetC_induction.P [variable, in list_representation.list_representation]
FSetC.FSetC_induction.A [variable, in list_representation.list_representation]
FSetC.FSetC_induction [section, in list_representation.list_representation]
FSetC.FSetC.A [variable, in list_representation.list_representation]
_ ;; _ [notation, in list_representation.list_representation]
FSetC.fset_empty [instance, in list_representation.list_representation]
FSetC.Nil [constructor, in list_representation.list_representation]
FSetC.trunc [axiom, in list_representation.list_representation]
_ ;; _ [notation, in list_representation.list_representation]
FSets [library]
fsets_dec_eq [instance, in kuratowski.properties]
fset_to_k_to_fset [lemma, in subobjects.k_finite]
fset_to_k [definition, in subobjects.k_finite]
fset_list_memb [lemma, in implementations.lists]
fset_bot [instance, in kuratowski.properties]
fset_min [instance, in kuratowski.properties]
fset_max [instance, in kuratowski.properties]
fset_join_semilattice [section, in kuratowski.properties]
FSet_sum [lemma, in kuratowski.properties]
FSet_Unit [lemma, in kuratowski.properties]
FSet_Unit_2 [definition, in kuratowski.properties]
fset_monad [instance, in kuratowski.properties]
fset_functor [instance, in kuratowski.properties]
fset_functorish [instance, in kuratowski.properties]
FSet_not_hset [lemma, in misc.bad]
FSet_S_ap [lemma, in misc.bad]
FSet_to_S [definition, in misc.bad]
fset_subset [instance, in kuratowski.kuratowski_sets]
fset_member [instance, in kuratowski.kuratowski_sets]
FSet_to_Bfin [definition, in subobjects.b_finite]
FSet_cons_ind [lemma, in list_representation.isomorphism]
fset_fsetc [lemma, in list_representation.isomorphism]
FSet_to_FSetC [definition, in list_representation.isomorphism]
FSet_to_enumeratedS [definition, in subobjects.enumerated]
fset_dec_enumerated.A [variable, in subobjects.enumerated]
fset_dec_enumerated [section, in subobjects.enumerated]
fset_ext [lemma, in kuratowski.extensionality]
FSet_cons_beta_cons [definition, in kuratowski.operations]
FSet_cons_beta_empty [definition, in kuratowski.operations]
FSet_cons_rec [definition, in kuratowski.operations]
FSet_cons_rec.Pcomm [variable, in kuratowski.operations]
FSet_cons_rec.Pdupl [variable, in kuratowski.operations]
FSet_cons_rec.Pcons [variable, in kuratowski.operations]
FSet_cons_rec.Pe [variable, in kuratowski.operations]
FSet_cons_rec.Pset [variable, in kuratowski.operations]
FSet_cons_rec.P [variable, in kuratowski.operations]
FSet_cons_rec [section, in kuratowski.operations]
fset_intersection [instance, in kuratowski.operations]
fset_subset_bool [instance, in kuratowski.operations]
fset_member_bool [instance, in kuratowski.operations]
fset_comprehension [instance, in kuratowski.operations]
fset_bind [instance, in kuratowski.operations]
fset_pure [instance, in kuratowski.operations]
fset_fmap [definition, in kuratowski.operations]
FSet.assoc [axiom, in misc.bad]
FSet.assoc [axiom, in kuratowski.kuratowski_sets]
FSet.comm [axiom, in misc.bad]
FSet.comm [axiom, in kuratowski.kuratowski_sets]
FSet.E [constructor, in misc.bad]
FSet.E [constructor, in kuratowski.kuratowski_sets]
FSet.FSet [inductive, in misc.bad]
FSet.FSet [section, in misc.bad]
FSet.FSet [inductive, in kuratowski.kuratowski_sets]
FSet.FSet [section, in kuratowski.kuratowski_sets]
FSet.FSet_recursion [instance, in misc.bad]
FSet.FSet_rec_beta_idem [definition, in misc.bad]
FSet.FSet_rec_beta_nr [definition, in misc.bad]
FSet.FSet_rec_beta_nl [definition, in misc.bad]
FSet.FSet_rec_beta_comm [definition, in misc.bad]
FSet.FSet_rec_beta_assoc [definition, in misc.bad]
FSet.FSet_rec [definition, in misc.bad]
FSet.FSet_recursion.idemP [variable, in misc.bad]
FSet.FSet_recursion.nrP [variable, in misc.bad]
FSet.FSet_recursion.nlP [variable, in misc.bad]
FSet.FSet_recursion.commP [variable, in misc.bad]
FSet.FSet_recursion.assocP [variable, in misc.bad]
FSet.FSet_recursion.u [variable, in misc.bad]
FSet.FSet_recursion.l [variable, in misc.bad]
FSet.FSet_recursion.e [variable, in misc.bad]
FSet.FSet_recursion.P [variable, in misc.bad]
FSet.FSet_recursion.A [variable, in misc.bad]
FSet.FSet_recursion [section, in misc.bad]
FSet.FSet_ind_beta_idem [axiom, in misc.bad]
FSet.FSet_ind_beta_nr [axiom, in misc.bad]
FSet.FSet_ind_beta_nl [axiom, in misc.bad]
FSet.FSet_ind_beta_comm [axiom, in misc.bad]
FSet.FSet_ind_beta_assoc [axiom, in misc.bad]
FSet.FSet_ind [definition, in misc.bad]
FSet.FSet_induction.idemP [variable, in misc.bad]
FSet.FSet_induction.nrP [variable, in misc.bad]
FSet.FSet_induction.nlP [variable, in misc.bad]
FSet.FSet_induction.commP [variable, in misc.bad]
FSet.FSet_induction.assocP [variable, in misc.bad]
FSet.FSet_induction.uP [variable, in misc.bad]
FSet.FSet_induction.lP [variable, in misc.bad]
FSet.FSet_induction.eP [variable, in misc.bad]
FSet.FSet_induction.P [variable, in misc.bad]
FSet.FSet_induction.A [variable, in misc.bad]
FSet.FSet_induction [section, in misc.bad]
FSet.fset_union [instance, in misc.bad]
FSet.fset_singleton [instance, in misc.bad]
FSet.fset_empty [instance, in misc.bad]
FSet.FSet_recursion [instance, in kuratowski.kuratowski_sets]
FSet.FSet_rec [definition, in kuratowski.kuratowski_sets]
FSet.FSet_recursion.idemP [variable, in kuratowski.kuratowski_sets]
FSet.FSet_recursion.nrP [variable, in kuratowski.kuratowski_sets]
FSet.FSet_recursion.nlP [variable, in kuratowski.kuratowski_sets]
FSet.FSet_recursion.commP [variable, in kuratowski.kuratowski_sets]
FSet.FSet_recursion.assocP [variable, in kuratowski.kuratowski_sets]
FSet.FSet_recursion.u [variable, in kuratowski.kuratowski_sets]
FSet.FSet_recursion.l [variable, in kuratowski.kuratowski_sets]
FSet.FSet_recursion.e [variable, in kuratowski.kuratowski_sets]
FSet.FSet_recursion.H [variable, in kuratowski.kuratowski_sets]
FSet.FSet_recursion.P [variable, in kuratowski.kuratowski_sets]
FSet.FSet_recursion.A [variable, in kuratowski.kuratowski_sets]
FSet.FSet_recursion [section, in kuratowski.kuratowski_sets]
FSet.FSet_ind [definition, in kuratowski.kuratowski_sets]
FSet.FSet_induction.idemP [variable, in kuratowski.kuratowski_sets]
FSet.FSet_induction.nrP [variable, in kuratowski.kuratowski_sets]
FSet.FSet_induction.nlP [variable, in kuratowski.kuratowski_sets]
FSet.FSet_induction.commP [variable, in kuratowski.kuratowski_sets]
FSet.FSet_induction.assocP [variable, in kuratowski.kuratowski_sets]
FSet.FSet_induction.uP [variable, in kuratowski.kuratowski_sets]
FSet.FSet_induction.lP [variable, in kuratowski.kuratowski_sets]
FSet.FSet_induction.eP [variable, in kuratowski.kuratowski_sets]
FSet.FSet_induction.H [variable, in kuratowski.kuratowski_sets]
FSet.FSet_induction.P [variable, in kuratowski.kuratowski_sets]
FSet.FSet_induction.A [variable, in kuratowski.kuratowski_sets]
FSet.FSet_induction [section, in kuratowski.kuratowski_sets]
FSet.fset_union [instance, in kuratowski.kuratowski_sets]
FSet.fset_singleton [instance, in kuratowski.kuratowski_sets]
FSet.fset_empty [instance, in kuratowski.kuratowski_sets]
FSet.FSet.A [variable, in misc.bad]
FSet.FSet.A [variable, in kuratowski.kuratowski_sets]
FSet.idem [axiom, in misc.bad]
FSet.idem [axiom, in kuratowski.kuratowski_sets]
FSet.L [constructor, in misc.bad]
FSet.L [constructor, in kuratowski.kuratowski_sets]
FSet.nl [axiom, in misc.bad]
FSet.nl [axiom, in kuratowski.kuratowski_sets]
FSet.nr [axiom, in misc.bad]
FSet.nr [axiom, in kuratowski.kuratowski_sets]
FSet.trunc [axiom, in kuratowski.kuratowski_sets]
FSet.U [constructor, in misc.bad]
FSet.U [constructor, in kuratowski.kuratowski_sets]
fsum1 [definition, in kuratowski.properties]
fsum1_inr [lemma, in kuratowski.properties]
fsum1_inl [lemma, in kuratowski.properties]
fsum2 [definition, in kuratowski.properties]
Functor [record, in interfaces.monad_interface]
functor [section, in interfaces.monad_interface]
functor.F [variable, in interfaces.monad_interface]
fun_lattice [section, in interfaces.lattice_examples]
f_eq_ext [lemma, in interfaces.set_interface]
f_is_surjective [instance, in interfaces.set_interface]
f_eq [definition, in interfaces.set_interface]
f_surjective [instance, in interfaces.set_interface]
f_member [projection, in interfaces.set_interface]
f_filter [projection, in interfaces.set_interface]
f_union [projection, in interfaces.set_interface]
f_singleton [projection, in interfaces.set_interface]
f_empty [projection, in interfaces.set_interface]

H

hasBind [record, in interfaces.monad_interface]
hasComprehension [record, in interfaces.set_names]
hasComprehension [inductive, in interfaces.set_names]
hasDecidableEmpty [definition, in subobjects.sub]
hasEmpty [record, in interfaces.set_names]
hasEmpty [inductive, in interfaces.set_names]
hasIntersection [record, in interfaces.set_names]
hasIntersection [inductive, in interfaces.set_names]
hasMembership [record, in interfaces.set_names]
hasMembership [inductive, in interfaces.set_names]
hasMembership_decidable [record, in interfaces.set_names]
hasMembership_decidable [inductive, in interfaces.set_names]
hasPure [record, in interfaces.monad_interface]
hasSingleton [record, in interfaces.set_names]
hasSingleton [inductive, in interfaces.set_names]
hasSubset [record, in interfaces.set_names]
hasSubset [inductive, in interfaces.set_names]
hasSubset_decidable [record, in interfaces.set_names]
hasSubset_decidable [inductive, in interfaces.set_names]
hasUnion [record, in interfaces.set_names]
hasUnion [inductive, in interfaces.set_names]
hPropLattice [section, in interfaces.lattice_examples]
hprop_lem [instance, in prelude]
hprop_sub [instance, in interfaces.lattice_examples]
hprop_sub_fset [instance, in subobjects.enumerated]

I

idempotency [projection, in interfaces.lattice_interface]
idempotency [constructor, in interfaces.lattice_interface]
Idempotent [record, in interfaces.lattice_interface]
Idempotent [inductive, in interfaces.lattice_interface]
idempotent_max [projection, in interfaces.lattice_interface]
idempotent_min [projection, in interfaces.lattice_interface]
idempotent_max_js [projection, in interfaces.lattice_interface]
inclusion_exclusion [lemma, in kuratowski.length]
inl_embedding [instance, in prelude]
inr_embedding [instance, in prelude]
interface [section, in interfaces.set_interface]
interface.f [variable, in interfaces.set_interface]
interface.T [variable, in interfaces.set_interface]
intersect [section, in subobjects.sub]
intersection [projection, in interfaces.set_names]
intersection [constructor, in interfaces.set_names]
intersection [section, in misc.dec_kuratowski]
intersection_isIn [lemma, in kuratowski.properties]
intersection_isIn_d [lemma, in kuratowski.properties]
intersection.int [variable, in misc.dec_kuratowski]
intersection.int_member [variable, in misc.dec_kuratowski]
intersect.A [variable, in subobjects.sub]
intersect.C [variable, in subobjects.sub]
IP [constructor, in misc.dec_fset]
isEmpty [definition, in kuratowski.operations]
isIn [section, in subobjects.sub]
isIn_decidable [instance, in kuratowski.operations]
isIn.A [variable, in subobjects.sub]
isIn.C [variable, in subobjects.sub]
Iso [section, in list_representation.isomorphism]
isomorphism [library]
IsProjective [record, in misc.projective]
IsProjective [inductive, in misc.projective]
IsProjective_IsHProp [instance, in misc.projective]
IsTop [record, in misc.ordered]
IsTop [inductive, in misc.ordered]
I_Kfinite [lemma, in subobjects.k_finite]

J

JoinSemiLattice [record, in interfaces.lattice_interface]
JoinSemiLattice [section, in interfaces.lattice_interface]
joinsemilattice_fset [instance, in kuratowski.properties]
JoinSemiLattice.A [variable, in interfaces.lattice_interface]

K

Kf [definition, in subobjects.k_finite]
kfin_bfin.A [variable, in subobjects.b_finite]
kfin_bfin [section, in subobjects.b_finite]
kf_sub [definition, in subobjects.k_finite]
Kf_prod [lemma, in subobjects.k_finite]
Kf_subterm [lemma, in subobjects.k_finite]
Kf_sum_inv [lemma, in subobjects.k_finite]
Kf_sum [lemma, in subobjects.k_finite]
Kf_surjection [lemma, in subobjects.k_finite]
Kf_Unit [lemma, in subobjects.k_finite]
Kf_Empty [lemma, in subobjects.k_finite]
Kf_unfold [lemma, in subobjects.k_finite]
Kf_sub [definition, in subobjects.k_finite]
Kf_sub_hprop [instance, in subobjects.k_finite]
Kf_sub_intern [definition, in subobjects.k_finite]
Kf_to_Bf [instance, in subobjects.b_finite]
Kf_enumerated [definition, in subobjects.enumerated]
kuratowski_projective [instance, in misc.projective]
kuratowski_projective_oo [instance, in misc.projective]
kuratowski_sets [library]
k_to_fset_to_k [lemma, in subobjects.k_finite]
k_to_fset [definition, in subobjects.k_finite]
k_properties [section, in subobjects.k_finite]
k_finite_hasDecidableEmpty [lemma, in subobjects.k_finite]
k_finite_singleton [lemma, in subobjects.k_finite]
k_finite_empty [lemma, in subobjects.k_finite]
k_finite_union [lemma, in subobjects.k_finite]
k_finite [section, in subobjects.k_finite]
k_fin_projective_lem.P [variable, in misc.projective]
k_fin_projective_lem [section, in misc.projective]
k_fin_lem_projective.X [variable, in misc.projective]
k_fin_lem_projective [section, in misc.projective]
k_fin_lemoo_projective [section, in misc.projective]
k_finite [library]

L

land [instance, in interfaces.lattice_examples]
land_idempotent [instance, in interfaces.lattice_examples]
land_associative [instance, in interfaces.lattice_examples]
land_commutative [instance, in interfaces.lattice_examples]
Lattice [record, in interfaces.lattice_interface]
Lattice [section, in interfaces.lattice_interface]
lattice_hprop [instance, in interfaces.lattice_examples]
lattice_sub [instance, in interfaces.lattice_examples]
lattice_fun [instance, in interfaces.lattice_examples]
lattice_bool [instance, in interfaces.lattice_examples]
lattice_operations.A [variable, in interfaces.lattice_interface]
lattice_operations [section, in interfaces.lattice_interface]
lattice_fset [instance, in kuratowski.properties]
lattice_examples [library]
lattice_interface [library]
Lattice.A [variable, in interfaces.lattice_interface]
LEM [lemma, in misc.projective]
lemma_4_10 [definition, in CPP]
lemma_4_9 [definition, in CPP]
lemma_4_6 [definition, in CPP]
lemma_4_2 [definition, in CPP]
lemma_2_6 [definition, in CPP]
lemma_2_3 [definition, in CPP]
length [definition, in kuratowski.length]
length [section, in kuratowski.length]
length [section, in misc.dec_kuratowski]
length [library]
length_one [lemma, in kuratowski.length]
length_zero [lemma, in kuratowski.length]
length_zero_one [section, in kuratowski.length]
length_disjoint_sum [lemma, in kuratowski.length]
length_fmap_inj [lemma, in kuratowski.length]
length_sum [section, in kuratowski.length]
length_product [lemma, in kuratowski.length]
length_singleproduct [lemma, in kuratowski.length]
length_product [section, in kuratowski.length]
length_union_1 [lemma, in kuratowski.length]
length_single_disjoint [lemma, in kuratowski.length]
length_disjoint [definition, in kuratowski.length]
length_add [definition, in kuratowski.length]
length_compute [lemma, in kuratowski.length]
length_singleton [definition, in kuratowski.length]
length_empty [definition, in kuratowski.length]
length.length [variable, in misc.dec_kuratowski]
length.length_one [variable, in misc.dec_kuratowski]
length.length_singleton [variable, in misc.dec_kuratowski]
leq [projection, in misc.ordered]
leq [constructor, in misc.ordered]
LessThan [record, in misc.ordered]
LessThan [inductive, in misc.ordered]
lfalse [instance, in interfaces.lattice_examples]
listexist_intro [lemma, in implementations.lists]
listExt [definition, in subobjects.enumerated]
listExt_concatD_l [lemma, in subobjects.enumerated]
listExt_concatD_r [lemma, in subobjects.enumerated]
listExt_weaken [lemma, in subobjects.enumerated]
listExt_prod [lemma, in subobjects.enumerated]
listExt_prod_sing [lemma, in subobjects.enumerated]
listExt_app_l [lemma, in subobjects.enumerated]
listExt_app_r [lemma, in subobjects.enumerated]
listProd [definition, in subobjects.enumerated]
listProd_sing [definition, in subobjects.enumerated]
lists [library]
lists_sets [instance, in implementations.lists]
lists_are_sets [section, in implementations.lists]
ListToSet [section, in implementations.lists]
ListToSet.A [variable, in implementations.lists]
list_exist_set [lemma, in implementations.lists]
list_exist [definition, in implementations.lists]
list_all_elim [lemma, in implementations.lists]
list_all_intro [lemma, in implementations.lists]
list_all_set [lemma, in implementations.lists]
list_all [definition, in implementations.lists]
list_to_set [definition, in implementations.lists]
list_comprehension [instance, in implementations.lists]
list_membership [instance, in implementations.lists]
list_union [instance, in implementations.lists]
list_single [instance, in implementations.lists]
list_empty [instance, in implementations.lists]
list_weaken_to_fset_in_sub [lemma, in subobjects.enumerated]
list_weaken_to_fset_ext [lemma, in subobjects.enumerated]
list_weaken_to_fset [definition, in subobjects.enumerated]
list_to_fset_ext [lemma, in subobjects.enumerated]
list_to_fset [definition, in subobjects.enumerated]
list_representation [library]
lor [instance, in interfaces.lattice_examples]
lor_neutralr [instance, in interfaces.lattice_examples]
lor_neutrall [instance, in interfaces.lattice_examples]
lor_idempotent [instance, in interfaces.lattice_examples]
lor_associative [instance, in interfaces.lattice_examples]
lor_commutative [instance, in interfaces.lattice_examples]

M

map [definition, in subobjects.k_finite]
map [definition, in subobjects.enumerated]
map_union [lemma, in subobjects.k_finite]
map_injective [instance, in subobjects.k_finite]
map_listExt [lemma, in subobjects.enumerated]
maxAP [instance, in interfaces.lattice_examples]
maximum [record, in interfaces.lattice_interface]
maximum [inductive, in interfaces.lattice_interface]
maximum_bool [instance, in interfaces.lattice_examples]
max_fun [instance, in interfaces.lattice_examples]
max_min [definition, in interfaces.lattice_examples]
max_L [projection, in interfaces.lattice_interface]
max_L [constructor, in interfaces.lattice_interface]
member [projection, in interfaces.set_names]
member [constructor, in interfaces.set_names]
membership [section, in misc.dec_kuratowski]
member_isIn [lemma, in implementations.lists]
member_dec [projection, in interfaces.set_names]
member_dec [constructor, in interfaces.set_names]
MerelyDecidablePaths [record, in prelude]
MerelyDecidablePaths [inductive, in prelude]
merely_decidable_sum [instance, in prelude]
merely_decidable_paths_prod [instance, in prelude]
merely_decidable_operations.B [variable, in prelude]
merely_decidable_operations.A [variable, in prelude]
merely_decidable_operations [section, in prelude]
merely_choice [lemma, in kuratowski.properties]
merely_dec [lemma, in misc.dec_lem]
merely_enumeration_FSet [definition, in subobjects.enumerated]
mere_choice [section, in kuratowski.properties]
min [definition, in misc.ordered]
minAP [instance, in interfaces.lattice_examples]
minimum [section, in misc.ordered]
minimum [record, in interfaces.lattice_interface]
minimum [inductive, in interfaces.lattice_interface]
minimum_bool [instance, in interfaces.lattice_examples]
minimum.top [variable, in misc.ordered]
min_set_spec [definition, in misc.ordered]
min_set [definition, in misc.ordered]
min_set.A [variable, in misc.ordered]
min_set [section, in misc.ordered]
min_top_r [lemma, in misc.ordered]
min_top_l [lemma, in misc.ordered]
min_nl [lemma, in misc.ordered]
min_nr [lemma, in misc.ordered]
min_assoc [lemma, in misc.ordered]
min_idem [lemma, in misc.ordered]
min_comm [lemma, in misc.ordered]
min_spec2 [lemma, in misc.ordered]
min_spec1 [lemma, in misc.ordered]
min_fun [instance, in interfaces.lattice_examples]
min_L [projection, in interfaces.lattice_interface]
min_L [constructor, in interfaces.lattice_interface]
misc_2 [definition, in CPP]
misc_1 [definition, in CPP]
Monad [record, in interfaces.monad_interface]
monad [section, in interfaces.monad_interface]
monad_fset [section, in kuratowski.properties]
monad_operations.F [variable, in interfaces.monad_interface]
monad_operations [section, in interfaces.monad_interface]
monad_interface [library]
monad.F [variable, in interfaces.monad_interface]
m_dec_path [projection, in prelude]
m_dec_path [constructor, in prelude]

N

neutralityL [projection, in interfaces.lattice_interface]
neutralityL [constructor, in interfaces.lattice_interface]
neutralityR [projection, in interfaces.lattice_interface]
neutralityR [constructor, in interfaces.lattice_interface]
NeutralL [record, in interfaces.lattice_interface]
NeutralL [inductive, in interfaces.lattice_interface]
neutralL_max [projection, in interfaces.lattice_interface]
neutralL_max_js [projection, in interfaces.lattice_interface]
NeutralR [record, in interfaces.lattice_interface]
NeutralR [inductive, in interfaces.lattice_interface]
neutralR_max [projection, in interfaces.lattice_interface]
neutralR_max_js [projection, in interfaces.lattice_interface]
notIn_ext_union_singleton [lemma, in subobjects.b_finite]
not_IP [definition, in misc.dec_fset]
not_ZP [definition, in misc.dec_fset]
not_YP [definition, in misc.dec_fset]
not_XP [definition, in misc.dec_fset]
no_singleton [lemma, in subobjects.b_finite]
no_union [lemma, in subobjects.b_finite]

O

operation [definition, in interfaces.lattice_interface]
Operations [section, in implementations.lists]
operations [section, in list_representation.operations]
operations [section, in kuratowski.operations]
operations [library]
operations [library]
operations_decidable [section, in kuratowski.operations]
ordered [library]

P

P [definition, in misc.dec_fset]
p [definition, in misc.projective]
Pauli [inductive, in misc.dec_fset]
pauli [section, in misc.dec_fset]
Pauli_mult_comm [lemma, in misc.dec_fset]
pauli_comm [definition, in misc.dec_fset]
Pauli_all [lemma, in misc.dec_fset]
Pauli_finite [lemma, in misc.dec_fset]
Pauli_list [definition, in misc.dec_fset]
Pauli_set [instance, in misc.dec_fset]
Pauli_mult [definition, in misc.dec_fset]
plus_assoc [lemma, in kuratowski.length]
prelude [library]
product [definition, in kuratowski.operations]
product_isIn_d [lemma, in kuratowski.properties]
product_membership [section, in kuratowski.properties]
product_isIn [definition, in kuratowski.properties]
projective [projection, in misc.projective]
projective [constructor, in misc.projective]
projective [library]
properties [section, in list_representation.properties]
properties [section, in interfaces.set_interface]
properties [library]
properties [library]
properties_membership_decidable [section, in kuratowski.properties]
properties_membership [section, in kuratowski.properties]
properties.f [variable, in interfaces.set_interface]
properties.T [variable, in interfaces.set_interface]
proposition_5_9 [definition, in CPP]
proposition_5_5 [definition, in CPP]
proposition_5_4 [definition, in CPP]
proposition_5_3 [definition, in CPP]
proposition_4_22 [definition, in CPP]
proposition_4_18 [definition, in CPP]
proposition_4_17 [definition, in CPP]
proposition_4_16 [definition, in CPP]
proposition_4_15 [definition, in CPP]
proposition_4_12 [definition, in CPP]
proposition_4_11 [definition, in CPP]
proposition_4_8 [definition, in CPP]
proposition_4_7 [definition, in CPP]
proposition_3_12 [definition, in CPP]
proposition_3_11 [definition, in CPP]
proposition_3_9 [definition, in CPP]
proposition_3_6 [definition, in CPP]
proposition_3_5 [definition, in CPP]
proposition_3_4 [definition, in CPP]
proposition_3_2 [definition, in CPP]
proposition_2_9 [definition, in CPP]
pure [projection, in interfaces.monad_interface]
p_surj [instance, in misc.projective]

Q

quantifiers [section, in misc.dec_fset]
quantifiers.P [variable, in misc.dec_fset]
quotientB [definition, in interfaces.set_interface]
quotientB_recursion [instance, in misc.dec_lem]
quotientB_surj [instance, in interfaces.set_interface]
quotientB_emb [instance, in interfaces.set_interface]
quotientB_to_B [definition, in interfaces.set_interface]
quotientB_recursion [instance, in interfaces.set_interface]
quotient_properties.f [variable, in interfaces.set_interface]
quotient_properties.T [variable, in interfaces.set_interface]
quotient_properties [section, in interfaces.set_interface]
quotient_iso [definition, in interfaces.set_interface]
quotient_surjection.H [variable, in interfaces.set_interface]
quotient_surjection.f [variable, in interfaces.set_interface]
quotient_surjection.B [variable, in interfaces.set_interface]
quotient_surjection.A [variable, in interfaces.set_interface]
quotient_surjection [section, in interfaces.set_interface]

R

R [definition, in misc.dec_lem]
refinement [definition, in interfaces.set_interface]
refinement [section, in interfaces.set_interface]
refinement_examples [section, in implementations.lists]
refinement.f [variable, in interfaces.set_interface]
refinement.g [variable, in interfaces.set_interface]
refinement.S [variable, in interfaces.set_interface]
refinement.T [variable, in interfaces.set_interface]
reflect_f_eq [definition, in interfaces.set_interface]
reflect_eq [definition, in interfaces.set_interface]
relation [definition, in misc.ordered]
relations [section, in kuratowski.kuratowski_sets]
remove_S [lemma, in kuratowski.length]
repr_iso [lemma, in list_representation.isomorphism]
repr_iso_id_r [lemma, in list_representation.isomorphism]
repr_iso_id_l [lemma, in list_representation.isomorphism]
reverse [definition, in implementations.lists]
reverse_set [lemma, in implementations.lists]
RTop [instance, in misc.ordered]
RTopOrder [instance, in misc.ordered]
rtop_hprop [instance, in misc.ordered]
R_trans [instance, in misc.dec_lem]
R_sym [instance, in misc.dec_lem]
R_refl [instance, in misc.dec_lem]
R_trans [instance, in interfaces.set_interface]
R_sym [instance, in interfaces.set_interface]
R_refl [instance, in interfaces.set_interface]

S

same_class [lemma, in interfaces.set_interface]
separation [definition, in kuratowski.operations]
separation_isIn [lemma, in kuratowski.properties]
sets [record, in interfaces.set_interface]
set_length_cons [definition, in implementations.lists]
set_length_nil [definition, in implementations.lists]
set_length [definition, in implementations.lists]
set_lattice [section, in kuratowski.properties]
set_sphere.A [variable, in misc.bad]
set_sphere [section, in misc.bad]
set_as_difference [lemma, in kuratowski.length]
set_singleton [instance, in subobjects.b_finite]
set_subset [definition, in interfaces.set_interface]
set_eq [definition, in interfaces.set_interface]
set_names [library]
set_interface [library]
simple_example [definition, in misc.dec_fset]
simple_example [section, in misc.dec_fset]
singleproduct_isIn_d_false [lemma, in kuratowski.properties]
singleproduct_isIn_d_aa [lemma, in kuratowski.properties]
singleproduct_isIn [lemma, in kuratowski.properties]
singleton [projection, in interfaces.set_names]
singleton [constructor, in interfaces.set_names]
singleton [definition, in subobjects.b_finite]
singleton_idem [lemma, in list_representation.properties]
singleton_single [definition, in implementations.lists]
singleton_isIn_d [lemma, in kuratowski.properties]
singleton_isIn_d_false [lemma, in kuratowski.properties]
singleton_isIn_d_aa [lemma, in kuratowski.properties]
singleton_isIn_d_true [lemma, in kuratowski.properties]
singleton_isIn [definition, in kuratowski.properties]
singleton_set.HA [variable, in subobjects.b_finite]
singleton_set.A [variable, in subobjects.b_finite]
singleton_set [section, in subobjects.b_finite]
singleton_fin_equiv [instance, in subobjects.b_finite]
singleton_fin_equiv' [definition, in subobjects.b_finite]
singleton_contr [instance, in subobjects.b_finite]
singleton_isIn [definition, in interfaces.set_interface]
single_product_disjoint [lemma, in kuratowski.length]
single_bfin_set [lemma, in subobjects.b_finite]
single_product [definition, in kuratowski.operations]
split [definition, in subobjects.b_finite]
split [section, in subobjects.b_finite]
split.A [variable, in subobjects.b_finite]
split.f [variable, in subobjects.b_finite]
split.n [variable, in subobjects.b_finite]
split.P [variable, in subobjects.b_finite]
squash [definition, in prelude]
structure [section, in interfaces.set_names]
structure_k_finite [section, in subobjects.k_finite]
structure.A [variable, in interfaces.set_names]
structure.T [variable, in interfaces.set_names]
Sub [definition, in subobjects.sub]
sub [library]
subobjects [section, in subobjects.sub]
subobjects [section, in subobjects.enumerated]
subobjects.A [variable, in subobjects.sub]
subobjects.A [variable, in subobjects.enumerated]
subobject_lattice [instance, in subobjects.sub]
subset [projection, in interfaces.set_names]
subset [constructor, in interfaces.set_names]
subset [section, in misc.dec_kuratowski]
subset_dec [projection, in interfaces.set_names]
subset_dec [constructor, in interfaces.set_names]
subset_isIn [lemma, in kuratowski.extensionality]
subset_union_equiv [lemma, in kuratowski.extensionality]
subset_union_l [lemma, in kuratowski.extensionality]
subset_union [lemma, in kuratowski.extensionality]
subset_decidable [instance, in kuratowski.operations]
sub_lattice [section, in interfaces.lattice_examples]
sub_classes.C [variable, in subobjects.sub]
sub_classes [section, in subobjects.sub]
sub_subset [instance, in subobjects.sub]
sub_comprehension [instance, in subobjects.sub]
sub_membership [instance, in subobjects.sub]
sub_singleton [instance, in subobjects.sub]
sub_intersection [instance, in subobjects.sub]
sub_union [instance, in subobjects.sub]
sub_empty [instance, in subobjects.sub]
Sum_Projective [instance, in misc.projective]
S1op [definition, in misc.bad]
S1op_comm [lemma, in misc.bad]
S1op_assoc [lemma, in misc.bad]
S1op_nl [lemma, in misc.bad]
S1op_nr [lemma, in misc.bad]
S1toSig [definition, in subobjects.b_finite]
S1toSig_equiv [instance, in subobjects.b_finite]
S1_Kfinite [lemma, in subobjects.k_finite]
S1_merely_decidable_equality [definition, in prelude]
S1_recursion [instance, in misc.bad]

T

T [definition, in misc.dec_lem]
test [instance, in interfaces.set_interface]
theorem_5_6 [definition, in CPP]
theorem_4_23 [definition, in CPP]
theorem_4_21 [definition, in CPP]
theorem_3_10 [definition, in CPP]
theorem_3_1 [definition, in CPP]
theorem_2_8 [definition, in CPP]
theorem_2_5 [definition, in CPP]
top [definition, in misc.ordered]
Top [definition, in misc.ordered]
top_a_top [instance, in misc.ordered]
top_max [projection, in misc.ordered]
top_max [constructor, in misc.ordered]
total [projection, in misc.ordered]
Total [record, in misc.ordered]
total [constructor, in misc.ordered]
Total [inductive, in misc.ordered]
TotalOrder [record, in misc.ordered]
TotalOrder [section, in misc.ordered]
TotalOrder_Total [projection, in misc.ordered]
TotalOrder_Transitive [projection, in misc.ordered]
TotalOrder_Antisymmetric [projection, in misc.ordered]
TotalOrder_Reflexive [projection, in misc.ordered]
TR [definition, in misc.dec_lem]
TR [section, in misc.dec_lem]
transfer [lemma, in interfaces.set_interface]
TR_one [definition, in misc.dec_lem]
TR_zero [definition, in misc.dec_lem]
TR.A [variable, in misc.dec_lem]
Two_FSet_Unit [definition, in kuratowski.properties]

U

union [projection, in interfaces.set_names]
union [constructor, in interfaces.set_names]
union_isIn_d [lemma, in kuratowski.properties]
union_isIn [definition, in kuratowski.properties]
union_idem [lemma, in kuratowski.kuratowski_sets]
union_to_disjoint [lemma, in kuratowski.length]
union_neutralR [lemma, in interfaces.set_interface]
union_neutralL [lemma, in interfaces.set_interface]
union_idem [lemma, in interfaces.set_interface]
union_assoc [lemma, in interfaces.set_interface]
union_comm [lemma, in interfaces.set_interface]
union_isIn [definition, in interfaces.set_interface]
Unit_Projective [instance, in misc.projective]

V

View [definition, in interfaces.set_interface]
view_lattice [instance, in interfaces.set_interface]
View_max [instance, in interfaces.set_interface]
View_member [instance, in interfaces.set_interface]
View_singleton [instance, in interfaces.set_interface]
View_empty [instance, in interfaces.set_interface]
view_comprehension [instance, in interfaces.set_interface]
view_union [instance, in interfaces.set_interface]

W

weaken_list_r [definition, in subobjects.enumerated]
well_defined_sungleton [definition, in interfaces.set_interface]
well_defined_empty [definition, in interfaces.set_interface]
well_defined_filter [definition, in interfaces.set_interface]
well_defined_union [definition, in interfaces.set_interface]

X

X [definition, in misc.dec_fset]
X [definition, in misc.projective]
XP [constructor, in misc.dec_fset]
X_fin [definition, in misc.projective]
X_set [instance, in misc.projective]
X_empty [lemma, in subobjects.b_finite]

Y

YP [constructor, in misc.dec_fset]

Z

ZP [constructor, in misc.dec_fset]
Z_not_S [lemma, in kuratowski.length]

other

_ ∧ _ (logic_scope) [notation, in interfaces.lattice_examples]
_ ∨ _ (logic_scope) [notation, in interfaces.lattice_examples]
_ ;; _ [notation, in list_representation.list_representation]
_ ⊆_d _ [notation, in interfaces.set_names]
_ ∈_d _ [notation, in interfaces.set_names]
_ ⊆ _ [notation, in interfaces.set_names]
_ ∈ _ [notation, in interfaces.set_names]
_ ∩ _ [notation, in interfaces.set_names]
_ ∪ _ [notation, in interfaces.set_names]
( ∩ _ ) [notation, in interfaces.set_names]
( _ ∩ ) [notation, in interfaces.set_names]
( ∩ ) [notation, in interfaces.set_names]
( ∪ _ ) [notation, in interfaces.set_names]
( _ ∪) [notation, in interfaces.set_names]
(∪) [notation, in interfaces.set_names]
{| _ & _ |} [notation, in interfaces.set_names]
{| _ |} [notation, in interfaces.set_names]
∅ [notation, in interfaces.set_names]

---

Notation Index

F

_ ;; _ [in list_representation.list_representation]
_ ;; _ [in list_representation.list_representation]

other

_ ∧ _ (logic_scope) [in interfaces.lattice_examples]
_ ∨ _ (logic_scope) [in interfaces.lattice_examples]
_ ;; _ [in list_representation.list_representation]
_ ⊆_d _ [in interfaces.set_names]
_ ∈_d _ [in interfaces.set_names]
_ ⊆ _ [in interfaces.set_names]
_ ∈ _ [in interfaces.set_names]
_ ∩ _ [in interfaces.set_names]
_ ∪ _ [in interfaces.set_names]
( ∩ _ ) [in interfaces.set_names]
( _ ∩ ) [in interfaces.set_names]
( ∩ ) [in interfaces.set_names]
( ∪ _ ) [in interfaces.set_names]
( _ ∪) [in interfaces.set_names]
(∪) [in interfaces.set_names]
{| _ & _ |} [in interfaces.set_names]
{| _ |} [in interfaces.set_names]
∅ [in interfaces.set_names]

---

Module Index

F

FSet [in misc.bad]
FSet [in kuratowski.kuratowski_sets]
FSetC [in list_representation.list_representation]

---

Variable Index

A

add_top.A [in misc.ordered]

B

binary_operation.n [in interfaces.lattice_interface]
binary_operation.g [in interfaces.lattice_interface]
binary_operation.f [in interfaces.lattice_interface]
binary_operation.A [in interfaces.lattice_interface]

D

dec_membership.A [in subobjects.b_finite]

E

empty.A [in subobjects.b_finite]
empty.X [in subobjects.b_finite]
empty.Xequiv [in subobjects.b_finite]
enumerated_fset.A [in subobjects.enumerated]

F

finite_hott.A [in subobjects.b_finite]
FSetC.FSetC_prim_recursion.commP [in list_representation.list_representation]
FSetC.FSetC_prim_recursion.duplP [in list_representation.list_representation]
FSetC.FSetC_prim_recursion.cns [in list_representation.list_representation]
FSetC.FSetC_prim_recursion.nil [in list_representation.list_representation]
FSetC.FSetC_prim_recursion.H [in list_representation.list_representation]
FSetC.FSetC_prim_recursion.P [in list_representation.list_representation]
FSetC.FSetC_prim_recursion.A [in list_representation.list_representation]
FSetC.FSetC_recursion.commP [in list_representation.list_representation]
FSetC.FSetC_recursion.duplP [in list_representation.list_representation]
FSetC.FSetC_recursion.cns [in list_representation.list_representation]
FSetC.FSetC_recursion.nil [in list_representation.list_representation]
FSetC.FSetC_recursion.H [in list_representation.list_representation]
FSetC.FSetC_recursion.P [in list_representation.list_representation]
FSetC.FSetC_recursion.A [in list_representation.list_representation]
FSetC.FSetC_induction.commP [in list_representation.list_representation]
FSetC.FSetC_induction.duplP [in list_representation.list_representation]
FSetC.FSetC_induction.cnsP [in list_representation.list_representation]
FSetC.FSetC_induction.eP [in list_representation.list_representation]
FSetC.FSetC_induction.H [in list_representation.list_representation]
FSetC.FSetC_induction.P [in list_representation.list_representation]
FSetC.FSetC_induction.A [in list_representation.list_representation]
FSetC.FSetC.A [in list_representation.list_representation]
fset_dec_enumerated.A [in subobjects.enumerated]
FSet_cons_rec.Pcomm [in kuratowski.operations]
FSet_cons_rec.Pdupl [in kuratowski.operations]
FSet_cons_rec.Pcons [in kuratowski.operations]
FSet_cons_rec.Pe [in kuratowski.operations]
FSet_cons_rec.Pset [in kuratowski.operations]
FSet_cons_rec.P [in kuratowski.operations]
FSet.FSet_recursion.idemP [in misc.bad]
FSet.FSet_recursion.nrP [in misc.bad]
FSet.FSet_recursion.nlP [in misc.bad]
FSet.FSet_recursion.commP [in misc.bad]
FSet.FSet_recursion.assocP [in misc.bad]
FSet.FSet_recursion.u [in misc.bad]
FSet.FSet_recursion.l [in misc.bad]
FSet.FSet_recursion.e [in misc.bad]
FSet.FSet_recursion.P [in misc.bad]
FSet.FSet_recursion.A [in misc.bad]
FSet.FSet_induction.idemP [in misc.bad]
FSet.FSet_induction.nrP [in misc.bad]
FSet.FSet_induction.nlP [in misc.bad]
FSet.FSet_induction.commP [in misc.bad]
FSet.FSet_induction.assocP [in misc.bad]
FSet.FSet_induction.uP [in misc.bad]
FSet.FSet_induction.lP [in misc.bad]
FSet.FSet_induction.eP [in misc.bad]
FSet.FSet_induction.P [in misc.bad]
FSet.FSet_induction.A [in misc.bad]
FSet.FSet_recursion.idemP [in kuratowski.kuratowski_sets]
FSet.FSet_recursion.nrP [in kuratowski.kuratowski_sets]
FSet.FSet_recursion.nlP [in kuratowski.kuratowski_sets]
FSet.FSet_recursion.commP [in kuratowski.kuratowski_sets]
FSet.FSet_recursion.assocP [in kuratowski.kuratowski_sets]
FSet.FSet_recursion.u [in kuratowski.kuratowski_sets]
FSet.FSet_recursion.l [in kuratowski.kuratowski_sets]
FSet.FSet_recursion.e [in kuratowski.kuratowski_sets]
FSet.FSet_recursion.H [in kuratowski.kuratowski_sets]
FSet.FSet_recursion.P [in kuratowski.kuratowski_sets]
FSet.FSet_recursion.A [in kuratowski.kuratowski_sets]
FSet.FSet_induction.idemP [in kuratowski.kuratowski_sets]
FSet.FSet_induction.nrP [in kuratowski.kuratowski_sets]
FSet.FSet_induction.nlP [in kuratowski.kuratowski_sets]
FSet.FSet_induction.commP [in kuratowski.kuratowski_sets]
FSet.FSet_induction.assocP [in kuratowski.kuratowski_sets]
FSet.FSet_induction.uP [in kuratowski.kuratowski_sets]
FSet.FSet_induction.lP [in kuratowski.kuratowski_sets]
FSet.FSet_induction.eP [in kuratowski.kuratowski_sets]
FSet.FSet_induction.H [in kuratowski.kuratowski_sets]
FSet.FSet_induction.P [in kuratowski.kuratowski_sets]
FSet.FSet_induction.A [in kuratowski.kuratowski_sets]
FSet.FSet.A [in misc.bad]
FSet.FSet.A [in kuratowski.kuratowski_sets]
functor.F [in interfaces.monad_interface]

I

interface.f [in interfaces.set_interface]
interface.T [in interfaces.set_interface]
intersection.int [in misc.dec_kuratowski]
intersection.int_member [in misc.dec_kuratowski]
intersect.A [in subobjects.sub]
intersect.C [in subobjects.sub]
isIn.A [in subobjects.sub]
isIn.C [in subobjects.sub]

J

JoinSemiLattice.A [in interfaces.lattice_interface]

K

kfin_bfin.A [in subobjects.b_finite]
k_fin_projective_lem.P [in misc.projective]
k_fin_lem_projective.X [in misc.projective]

L

lattice_operations.A [in interfaces.lattice_interface]
Lattice.A [in interfaces.lattice_interface]
length.length [in misc.dec_kuratowski]
length.length_one [in misc.dec_kuratowski]
length.length_singleton [in misc.dec_kuratowski]
ListToSet.A [in implementations.lists]

M

merely_decidable_operations.B [in prelude]
merely_decidable_operations.A [in prelude]
minimum.top [in misc.ordered]
min_set.A [in misc.ordered]
monad_operations.F [in interfaces.monad_interface]
monad.F [in interfaces.monad_interface]

P

properties.f [in interfaces.set_interface]
properties.T [in interfaces.set_interface]

Q

quantifiers.P [in misc.dec_fset]
quotient_properties.f [in interfaces.set_interface]
quotient_properties.T [in interfaces.set_interface]
quotient_surjection.H [in interfaces.set_interface]
quotient_surjection.f [in interfaces.set_interface]
quotient_surjection.B [in interfaces.set_interface]
quotient_surjection.A [in interfaces.set_interface]

R

refinement.f [in interfaces.set_interface]
refinement.g [in interfaces.set_interface]
refinement.S [in interfaces.set_interface]
refinement.T [in interfaces.set_interface]

S

set_sphere.A [in misc.bad]
singleton_set.HA [in subobjects.b_finite]
singleton_set.A [in subobjects.b_finite]
split.A [in subobjects.b_finite]
split.f [in subobjects.b_finite]
split.n [in subobjects.b_finite]
split.P [in subobjects.b_finite]
structure.A [in interfaces.set_names]
structure.T [in interfaces.set_names]
subobjects.A [in subobjects.sub]
subobjects.A [in subobjects.enumerated]
sub_classes.C [in subobjects.sub]

T

TR.A [in misc.dec_lem]

---

Library Index

B

bad
b_finite

C

CPP

D

dec_kuratowski
dec_fset
dec_lem

E

enumerated
extensionality

F

FSets

I

isomorphism

K

kuratowski_sets
k_finite

L

lattice_examples
lattice_interface
length
lists
list_representation

M

monad_interface

O

operations
operations
ordered

P

prelude
projective
properties
properties

S

set_names
set_interface
sub

---

Lemma Index

A

all_elim [in misc.dec_fset]
all_intro [in misc.dec_fset]
append_comm [in list_representation.properties]
append_singleton [in list_representation.properties]
append_assoc [in list_representation.properties]
append_nr [in list_representation.properties]
append_union [in implementations.lists]
append_union [in list_representation.isomorphism]
ap_equiv [in prelude]
ap_inl_path_sum_inl [in prelude]

B

bfin_union [in subobjects.b_finite]
bfin_to_kfin [in subobjects.b_finite]
bind_isIn [in kuratowski.properties]

C

comprehension_all [in kuratowski.properties]
comprehension_or [in kuratowski.properties]
comprehension_subset [in kuratowski.properties]
comprehension_false [in kuratowski.properties]
comprehension_isIn_d [in kuratowski.properties]
comprehension_isIn [in kuratowski.properties]
comprehension_union [in kuratowski.properties]

D

decidable_A_intersect [in subobjects.sub]
decidable_A_isIn [in subobjects.sub]
dec_length [in misc.dec_kuratowski]
dec_intersection [in misc.dec_kuratowski]
difference_isIn_d [in kuratowski.properties]
disjoint_summants [in kuratowski.length]
disjoint_sub [in kuratowski.length]
disjoint_difference [in kuratowski.length]

E

enumeratedS_union [in subobjects.enumerated]
enumeratedS_singleton [in subobjects.enumerated]
enumeratedS_empty [in subobjects.enumerated]
enumerated_Kf [in subobjects.enumerated]
enumerated_prod [in subobjects.enumerated]
enumerated_sum [in subobjects.enumerated]
enumerated_surj [in subobjects.enumerated]
enumerated_comprehension [in subobjects.enumerated]
equiv_definition [in subobjects.k_finite]
equiv_subset1_r [in kuratowski.extensionality]
equiv_subset1_l [in kuratowski.extensionality]
eq_subset [in kuratowski.extensionality]
eq_subset2 [in kuratowski.extensionality]
eq_subset1 [in kuratowski.extensionality]
exist_elim [in implementations.lists]
exist_isIn [in misc.dec_fset]
exist_elim [in misc.dec_fset]
exist_intro [in misc.dec_fset]
ext [in kuratowski.properties]

F

filterD_lookup [in subobjects.enumerated]
filterD_cons_no [in subobjects.enumerated]
filterD_cons [in subobjects.enumerated]
filter_comprehension [in implementations.lists]
fmap_isIn_d_inj [in kuratowski.properties]
fmap_isIn_inj [in kuratowski.properties]
fmap_isIn [in kuratowski.properties]
fmap_inr [in kuratowski.length]
fmap_inl [in kuratowski.length]
fset_to_k_to_fset [in subobjects.k_finite]
fset_list_memb [in implementations.lists]
FSet_sum [in kuratowski.properties]
FSet_Unit [in kuratowski.properties]
FSet_not_hset [in misc.bad]
FSet_S_ap [in misc.bad]
FSet_cons_ind [in list_representation.isomorphism]
fset_fsetc [in list_representation.isomorphism]
fset_ext [in kuratowski.extensionality]
fsum1_inr [in kuratowski.properties]
fsum1_inl [in kuratowski.properties]
f_eq_ext [in interfaces.set_interface]

I

inclusion_exclusion [in kuratowski.length]
intersection_isIn [in kuratowski.properties]
intersection_isIn_d [in kuratowski.properties]
I_Kfinite [in subobjects.k_finite]

K

Kf_prod [in subobjects.k_finite]
Kf_subterm [in subobjects.k_finite]
Kf_sum_inv [in subobjects.k_finite]
Kf_sum [in subobjects.k_finite]
Kf_surjection [in subobjects.k_finite]
Kf_Unit [in subobjects.k_finite]
Kf_Empty [in subobjects.k_finite]
Kf_unfold [in subobjects.k_finite]
k_to_fset_to_k [in subobjects.k_finite]
k_finite_hasDecidableEmpty [in subobjects.k_finite]
k_finite_singleton [in subobjects.k_finite]
k_finite_empty [in subobjects.k_finite]
k_finite_union [in subobjects.k_finite]

L

LEM [in misc.projective]
length_one [in kuratowski.length]
length_zero [in kuratowski.length]
length_disjoint_sum [in kuratowski.length]
length_fmap_inj [in kuratowski.length]
length_product [in kuratowski.length]
length_singleproduct [in kuratowski.length]
length_union_1 [in kuratowski.length]
length_single_disjoint [in kuratowski.length]
length_compute [in kuratowski.length]
listexist_intro [in implementations.lists]
listExt_concatD_l [in subobjects.enumerated]
listExt_concatD_r [in subobjects.enumerated]
listExt_weaken [in subobjects.enumerated]
listExt_prod [in subobjects.enumerated]
listExt_prod_sing [in subobjects.enumerated]
listExt_app_l [in subobjects.enumerated]
listExt_app_r [in subobjects.enumerated]
list_exist_set [in implementations.lists]
list_all_elim [in implementations.lists]
list_all_intro [in implementations.lists]
list_all_set [in implementations.lists]
list_weaken_to_fset_in_sub [in subobjects.enumerated]
list_weaken_to_fset_ext [in subobjects.enumerated]
list_to_fset_ext [in subobjects.enumerated]

M

map_union [in subobjects.k_finite]
map_listExt [in subobjects.enumerated]
member_isIn [in implementations.lists]
merely_choice [in kuratowski.properties]
merely_dec [in misc.dec_lem]
min_top_r [in misc.ordered]
min_top_l [in misc.ordered]
min_nl [in misc.ordered]
min_nr [in misc.ordered]
min_assoc [in misc.ordered]
min_idem [in misc.ordered]
min_comm [in misc.ordered]
min_spec2 [in misc.ordered]
min_spec1 [in misc.ordered]

N

notIn_ext_union_singleton [in subobjects.b_finite]
no_singleton [in subobjects.b_finite]
no_union [in subobjects.b_finite]

P

Pauli_mult_comm [in misc.dec_fset]
Pauli_all [in misc.dec_fset]
Pauli_finite [in misc.dec_fset]
plus_assoc [in kuratowski.length]
product_isIn_d [in kuratowski.properties]

R

remove_S [in kuratowski.length]
repr_iso [in list_representation.isomorphism]
repr_iso_id_r [in list_representation.isomorphism]
repr_iso_id_l [in list_representation.isomorphism]
reverse_set [in implementations.lists]

S

same_class [in interfaces.set_interface]
separation_isIn [in kuratowski.properties]
set_as_difference [in kuratowski.length]
singleproduct_isIn_d_false [in kuratowski.properties]
singleproduct_isIn_d_aa [in kuratowski.properties]
singleproduct_isIn [in kuratowski.properties]
singleton_idem [in list_representation.properties]
singleton_isIn_d [in kuratowski.properties]
singleton_isIn_d_false [in kuratowski.properties]
singleton_isIn_d_aa [in kuratowski.properties]
singleton_isIn_d_true [in kuratowski.properties]
single_product_disjoint [in kuratowski.length]
single_bfin_set [in subobjects.b_finite]
subset_isIn [in kuratowski.extensionality]
subset_union_equiv [in kuratowski.extensionality]
subset_union_l [in kuratowski.extensionality]
subset_union [in kuratowski.extensionality]
S1op_comm [in misc.bad]
S1op_assoc [in misc.bad]
S1op_nl [in misc.bad]
S1op_nr [in misc.bad]
S1_Kfinite [in subobjects.k_finite]

T

transfer [in interfaces.set_interface]

U

union_isIn_d [in kuratowski.properties]
union_idem [in kuratowski.kuratowski_sets]
union_to_disjoint [in kuratowski.length]
union_neutralR [in interfaces.set_interface]
union_neutralL [in interfaces.set_interface]
union_idem [in interfaces.set_interface]
union_assoc [in interfaces.set_interface]
union_comm [in interfaces.set_interface]

X

X_empty [in subobjects.b_finite]

Z

Z_not_S [in kuratowski.length]

---

Constructor Index

A

absorb [in interfaces.lattice_interface]
antisymmetry [in misc.ordered]
associativity [in interfaces.lattice_interface]

C

commutativity [in interfaces.lattice_interface]

E

empty [in interfaces.lattice_interface]
empty [in interfaces.set_names]

F

filter [in interfaces.set_names]
FSetC.Cns [in list_representation.list_representation]
FSetC.Nil [in list_representation.list_representation]
FSet.E [in misc.bad]
FSet.E [in kuratowski.kuratowski_sets]
FSet.L [in misc.bad]
FSet.L [in kuratowski.kuratowski_sets]
FSet.U [in misc.bad]
FSet.U [in kuratowski.kuratowski_sets]

I

idempotency [in interfaces.lattice_interface]
intersection [in interfaces.set_names]
IP [in misc.dec_fset]

L

leq [in misc.ordered]

M

max_L [in interfaces.lattice_interface]
member [in interfaces.set_names]
member_dec [in interfaces.set_names]
min_L [in interfaces.lattice_interface]
m_dec_path [in prelude]

N

neutralityL [in interfaces.lattice_interface]
neutralityR [in interfaces.lattice_interface]

P

projective [in misc.projective]

S

singleton [in interfaces.set_names]
subset [in interfaces.set_names]
subset_dec [in interfaces.set_names]

T

top_max [in misc.ordered]
total [in misc.ordered]

U

union [in interfaces.set_names]

X

XP [in misc.dec_fset]

Y

YP [in misc.dec_fset]

Z

ZP [in misc.dec_fset]

---

Axiom Index

F

FSetC.comm_s [in list_representation.list_representation]
FSetC.dupl [in list_representation.list_representation]
FSetC.trunc [in list_representation.list_representation]
FSet.assoc [in misc.bad]
FSet.assoc [in kuratowski.kuratowski_sets]
FSet.comm [in misc.bad]
FSet.comm [in kuratowski.kuratowski_sets]
FSet.FSet_ind_beta_idem [in misc.bad]
FSet.FSet_ind_beta_nr [in misc.bad]
FSet.FSet_ind_beta_nl [in misc.bad]
FSet.FSet_ind_beta_comm [in misc.bad]
FSet.FSet_ind_beta_assoc [in misc.bad]
FSet.idem [in misc.bad]
FSet.idem [in kuratowski.kuratowski_sets]
FSet.nl [in misc.bad]
FSet.nl [in kuratowski.kuratowski_sets]
FSet.nr [in misc.bad]
FSet.nr [in kuratowski.kuratowski_sets]
FSet.trunc [in kuratowski.kuratowski_sets]

---

Projection Index

A

absorb [in interfaces.lattice_interface]
absorption_max_min [in interfaces.lattice_interface]
absorption_min_max [in interfaces.lattice_interface]
antisymmetry [in misc.ordered]
associative_max [in interfaces.lattice_interface]
associative_min [in interfaces.lattice_interface]
associative_max_js [in interfaces.lattice_interface]
associativity [in interfaces.lattice_interface]

B

bind [in interfaces.monad_interface]
bind_neutral_r [in interfaces.monad_interface]
bind_neutral_l [in interfaces.monad_interface]
bind_assoc [in interfaces.monad_interface]

C

commutative_max [in interfaces.lattice_interface]
commutative_min [in interfaces.lattice_interface]
commutative_max_js [in interfaces.lattice_interface]
commutativity [in interfaces.lattice_interface]

E

empty [in interfaces.lattice_interface]
empty [in interfaces.set_names]

F

filter [in interfaces.set_names]
fmap_compose [in interfaces.monad_interface]
f_member [in interfaces.set_interface]
f_filter [in interfaces.set_interface]
f_union [in interfaces.set_interface]
f_singleton [in interfaces.set_interface]
f_empty [in interfaces.set_interface]

I

idempotency [in interfaces.lattice_interface]
idempotent_max [in interfaces.lattice_interface]
idempotent_min [in interfaces.lattice_interface]
idempotent_max_js [in interfaces.lattice_interface]
intersection [in interfaces.set_names]

L

leq [in misc.ordered]

M

max_L [in interfaces.lattice_interface]
member [in interfaces.set_names]
member_dec [in interfaces.set_names]
min_L [in interfaces.lattice_interface]
m_dec_path [in prelude]

N

neutralityL [in interfaces.lattice_interface]
neutralityR [in interfaces.lattice_interface]
neutralL_max [in interfaces.lattice_interface]
neutralL_max_js [in interfaces.lattice_interface]
neutralR_max [in interfaces.lattice_interface]
neutralR_max_js [in interfaces.lattice_interface]

P

projective [in misc.projective]
pure [in interfaces.monad_interface]

S

singleton [in interfaces.set_names]
subset [in interfaces.set_names]
subset_dec [in interfaces.set_names]

T

top_max [in misc.ordered]
total [in misc.ordered]
TotalOrder_Total [in misc.ordered]
TotalOrder_Transitive [in misc.ordered]
TotalOrder_Antisymmetric [in misc.ordered]
TotalOrder_Reflexive [in misc.ordered]

U

union [in interfaces.set_names]

---

Inductive Index

A

Absorption [in interfaces.lattice_interface]
Antisymmetric [in misc.ordered]
Associative [in interfaces.lattice_interface]

B

bottom [in interfaces.lattice_interface]

C

Commutative [in interfaces.lattice_interface]

F

FSetC.FSetC [in list_representation.list_representation]
FSet.FSet [in misc.bad]
FSet.FSet [in kuratowski.kuratowski_sets]

H

hasComprehension [in interfaces.set_names]
hasEmpty [in interfaces.set_names]
hasIntersection [in interfaces.set_names]
hasMembership [in interfaces.set_names]
hasMembership_decidable [in interfaces.set_names]
hasSingleton [in interfaces.set_names]
hasSubset [in interfaces.set_names]
hasSubset_decidable [in interfaces.set_names]
hasUnion [in interfaces.set_names]

I

Idempotent [in interfaces.lattice_interface]
IsProjective [in misc.projective]
IsTop [in misc.ordered]

L

LessThan [in misc.ordered]

M

maximum [in interfaces.lattice_interface]
MerelyDecidablePaths [in prelude]
minimum [in interfaces.lattice_interface]

N

NeutralL [in interfaces.lattice_interface]
NeutralR [in interfaces.lattice_interface]

P

Pauli [in misc.dec_fset]

T

Total [in misc.ordered]

---

Section Index

A

add_top [in misc.ordered]
alternative_definition [in subobjects.k_finite]

B

bfin_kfin [in subobjects.b_finite]
Bfin_no_singletons [in subobjects.b_finite]
binary_operation [in interfaces.lattice_interface]
BoolLattice [in interfaces.lattice_examples]
b_fin_projective [in misc.projective]

C

comprehension_properties [in kuratowski.properties]

D

decidable_equality [in misc.dec_kuratowski]
dec_eq [in kuratowski.properties]
dec_membership [in subobjects.b_finite]

E

empty [in subobjects.b_finite]
enumerated_fset [in subobjects.enumerated]
exists_isIn [in misc.dec_fset]
ext [in kuratowski.extensionality]

F

finite_hott [in subobjects.b_finite]
FSetC.FSetC [in list_representation.list_representation]
FSetC.FSetC_prim_recursion [in list_representation.list_representation]
FSetC.FSetC_recursion [in list_representation.list_representation]
FSetC.FSetC_induction [in list_representation.list_representation]
fset_join_semilattice [in kuratowski.properties]
fset_dec_enumerated [in subobjects.enumerated]
FSet_cons_rec [in kuratowski.operations]
FSet.FSet [in misc.bad]
FSet.FSet [in kuratowski.kuratowski_sets]
FSet.FSet_recursion [in misc.bad]
FSet.FSet_induction [in misc.bad]
FSet.FSet_recursion [in kuratowski.kuratowski_sets]
FSet.FSet_induction [in kuratowski.kuratowski_sets]
functor [in interfaces.monad_interface]
fun_lattice [in interfaces.lattice_examples]

H

hPropLattice [in interfaces.lattice_examples]

I

interface [in interfaces.set_interface]
intersect [in subobjects.sub]
intersection [in misc.dec_kuratowski]
isIn [in subobjects.sub]
Iso [in list_representation.isomorphism]

J

JoinSemiLattice [in interfaces.lattice_interface]

K

kfin_bfin [in subobjects.b_finite]
k_properties [in subobjects.k_finite]
k_finite [in subobjects.k_finite]
k_fin_projective_lem [in misc.projective]
k_fin_lem_projective [in misc.projective]
k_fin_lemoo_projective [in misc.projective]

L

Lattice [in interfaces.lattice_interface]
lattice_operations [in interfaces.lattice_interface]
length [in kuratowski.length]
length [in misc.dec_kuratowski]
length_zero_one [in kuratowski.length]
length_sum [in kuratowski.length]
length_product [in kuratowski.length]
lists_are_sets [in implementations.lists]
ListToSet [in implementations.lists]

M

membership [in misc.dec_kuratowski]
merely_decidable_operations [in prelude]
mere_choice [in kuratowski.properties]
minimum [in misc.ordered]
min_set [in misc.ordered]
monad [in interfaces.monad_interface]
monad_fset [in kuratowski.properties]
monad_operations [in interfaces.monad_interface]

O

Operations [in implementations.lists]
operations [in list_representation.operations]
operations [in kuratowski.operations]
operations_decidable [in kuratowski.operations]

P

pauli [in misc.dec_fset]
product_membership [in kuratowski.properties]
properties [in list_representation.properties]
properties [in interfaces.set_interface]
properties_membership_decidable [in kuratowski.properties]
properties_membership [in kuratowski.properties]

Q

quantifiers [in misc.dec_fset]
quotient_properties [in interfaces.set_interface]
quotient_surjection [in interfaces.set_interface]

R

refinement [in interfaces.set_interface]
refinement_examples [in implementations.lists]
relations [in kuratowski.kuratowski_sets]

S

set_lattice [in kuratowski.properties]
set_sphere [in misc.bad]
simple_example [in misc.dec_fset]
singleton_set [in subobjects.b_finite]
split [in subobjects.b_finite]
structure [in interfaces.set_names]
structure_k_finite [in subobjects.k_finite]
subobjects [in subobjects.sub]
subobjects [in subobjects.enumerated]
subset [in misc.dec_kuratowski]
sub_lattice [in interfaces.lattice_examples]
sub_classes [in subobjects.sub]

T

TotalOrder [in misc.ordered]
TR [in misc.dec_lem]

---

Instance Index

A

absorption_andb_orb [in interfaces.lattice_examples]
absorption_orb_andb [in interfaces.lattice_examples]
all_decidable [in misc.dec_fset]

B

bishop_projective [in misc.projective]
botAP [in interfaces.lattice_examples]
bottom_bool [in interfaces.lattice_examples]
bottom_view [in interfaces.set_interface]
bot_fun [in interfaces.lattice_examples]

D

DecidableMembership [in subobjects.b_finite]
DecidableToMerely [in prelude]
decidable_eq_pauli [in misc.dec_fset]
dec_memb_list [in implementations.lists]
dec_memb [in implementations.lists]

E

Empty_Projective [in misc.projective]
exist_decidable [in misc.dec_fset]

F

fmap_Surjection [in kuratowski.properties]
fsetc_singleton [in list_representation.operations]
fsetc_union [in list_representation.operations]
FSetC.FSetC_recursion [in list_representation.list_representation]
FSetC.fset_empty [in list_representation.list_representation]
fsets_dec_eq [in kuratowski.properties]
fset_bot [in kuratowski.properties]
fset_min [in kuratowski.properties]
fset_max [in kuratowski.properties]
fset_monad [in kuratowski.properties]
fset_functor [in kuratowski.properties]
fset_functorish [in kuratowski.properties]
fset_subset [in kuratowski.kuratowski_sets]
fset_member [in kuratowski.kuratowski_sets]
fset_intersection [in kuratowski.operations]
fset_subset_bool [in kuratowski.operations]
fset_member_bool [in kuratowski.operations]
fset_comprehension [in kuratowski.operations]
fset_bind [in kuratowski.operations]
fset_pure [in kuratowski.operations]
FSet.FSet_recursion [in misc.bad]
FSet.fset_union [in misc.bad]
FSet.fset_singleton [in misc.bad]
FSet.fset_empty [in misc.bad]
FSet.FSet_recursion [in kuratowski.kuratowski_sets]
FSet.fset_union [in kuratowski.kuratowski_sets]
FSet.fset_singleton [in kuratowski.kuratowski_sets]
FSet.fset_empty [in kuratowski.kuratowski_sets]
f_is_surjective [in interfaces.set_interface]
f_surjective [in interfaces.set_interface]

H

hprop_lem [in prelude]
hprop_sub [in interfaces.lattice_examples]
hprop_sub_fset [in subobjects.enumerated]

I

inl_embedding [in prelude]
inr_embedding [in prelude]
isIn_decidable [in kuratowski.operations]
IsProjective_IsHProp [in misc.projective]

J

joinsemilattice_fset [in kuratowski.properties]

K

Kf_sub_hprop [in subobjects.k_finite]
Kf_to_Bf [in subobjects.b_finite]
kuratowski_projective [in misc.projective]
kuratowski_projective_oo [in misc.projective]

L

land [in interfaces.lattice_examples]
land_idempotent [in interfaces.lattice_examples]
land_associative [in interfaces.lattice_examples]
land_commutative [in interfaces.lattice_examples]
lattice_hprop [in interfaces.lattice_examples]
lattice_sub [in interfaces.lattice_examples]
lattice_fun [in interfaces.lattice_examples]
lattice_bool [in interfaces.lattice_examples]
lattice_fset [in kuratowski.properties]
lfalse [in interfaces.lattice_examples]
lists_sets [in implementations.lists]
list_comprehension [in implementations.lists]
list_membership [in implementations.lists]
list_union [in implementations.lists]
list_single [in implementations.lists]
list_empty [in implementations.lists]
lor [in interfaces.lattice_examples]
lor_neutralr [in interfaces.lattice_examples]
lor_neutrall [in interfaces.lattice_examples]
lor_idempotent [in interfaces.lattice_examples]
lor_associative [in interfaces.lattice_examples]
lor_commutative [in interfaces.lattice_examples]

M

map_injective [in subobjects.k_finite]
maxAP [in interfaces.lattice_examples]
maximum_bool [in interfaces.lattice_examples]
max_fun [in interfaces.lattice_examples]
merely_decidable_sum [in prelude]
merely_decidable_paths_prod [in prelude]
minAP [in interfaces.lattice_examples]
minimum_bool [in interfaces.lattice_examples]
min_fun [in interfaces.lattice_examples]

P

Pauli_set [in misc.dec_fset]
p_surj [in misc.projective]

Q

quotientB_recursion [in misc.dec_lem]
quotientB_surj [in interfaces.set_interface]
quotientB_emb [in interfaces.set_interface]
quotientB_recursion [in interfaces.set_interface]

R

RTop [in misc.ordered]
RTopOrder [in misc.ordered]
rtop_hprop [in misc.ordered]
R_trans [in misc.dec_lem]
R_sym [in misc.dec_lem]
R_refl [in misc.dec_lem]
R_trans [in interfaces.set_interface]
R_sym [in interfaces.set_interface]
R_refl [in interfaces.set_interface]

S

set_singleton [in subobjects.b_finite]
singleton_fin_equiv [in subobjects.b_finite]
singleton_contr [in subobjects.b_finite]
subobject_lattice [in subobjects.sub]
subset_decidable [in kuratowski.operations]
sub_subset [in subobjects.sub]
sub_comprehension [in subobjects.sub]
sub_membership [in subobjects.sub]
sub_singleton [in subobjects.sub]
sub_intersection [in subobjects.sub]
sub_union [in subobjects.sub]
sub_empty [in subobjects.sub]
Sum_Projective [in misc.projective]
S1toSig_equiv [in subobjects.b_finite]
S1_recursion [in misc.bad]

T

test [in interfaces.set_interface]
top_a_top [in misc.ordered]

U

Unit_Projective [in misc.projective]

V

view_lattice [in interfaces.set_interface]
View_max [in interfaces.set_interface]
View_member [in interfaces.set_interface]
View_singleton [in interfaces.set_interface]
View_empty [in interfaces.set_interface]
view_comprehension [in interfaces.set_interface]
view_union [in interfaces.set_interface]

X

X_set [in misc.projective]

---

Definition Index

A

all [in misc.dec_fset]
and_false [in interfaces.lattice_examples]
and_true [in interfaces.lattice_examples]
AP [in interfaces.lattice_examples]
append_nl [in list_representation.properties]

B

Bfin [in subobjects.b_finite]
bfin_to_kfin_sub [in subobjects.b_finite]

C

closedEmpty [in subobjects.sub]
closedIntersection [in subobjects.sub]
closedSingleton [in subobjects.sub]
closedUnion [in subobjects.sub]
comm' [in list_representation.isomorphism]
concatD [in subobjects.enumerated]
corollary_5_7 [in CPP]

D

decidable_empty_finite [in subobjects.b_finite]
dec_decidable_equality [in misc.dec_kuratowski]
dec_subset [in misc.dec_kuratowski]
dec_membership [in misc.dec_kuratowski]
definition_5_8 [in CPP]
definition_5_2 [in CPP]
definition_5_1 [in CPP]
definition_4_19 [in CPP]
definition_4_14 [in CPP]
definition_4_13 [in CPP]
definition_4_5 [in CPP]
definition_4_4 [in CPP]
definition_4_3 [in CPP]
definition_4_1 [in CPP]
definition_3_8 [in CPP]
definition_3_7 [in CPP]
definition_3_3 [in CPP]
definition_2_7 [in CPP]
definition_2_4 [in CPP]
definition_2_2 [in CPP]
definition_2_1 [in CPP]
difference [in kuratowski.operations]
disjoint [in kuratowski.length]
disjoint_sum [in kuratowski.operations]
dist₁ [in interfaces.lattice_examples]
dist₂ [in interfaces.lattice_examples]
dupl' [in list_representation.isomorphism]

E

el [in subobjects.b_finite]
empty_min [in misc.ordered]
empty_empty [in implementations.lists]
empty_isIn_d [in kuratowski.properties]
empty_isIn [in kuratowski.properties]
empty_finite [in subobjects.b_finite]
empty_isIn [in interfaces.set_interface]
enumerated [in subobjects.enumerated]
enumeratedS [in subobjects.enumerated]
enumeratedS_to_FSet [in subobjects.enumerated]
equiv_pathspace_T [in misc.dec_lem]
example_4_20 [in CPP]
exist [in misc.dec_fset]

F

f [in misc.bad]
filterD [in subobjects.enumerated]
filter_isIn [in interfaces.set_interface]
from_squash [in prelude]
FSetC_to_FSet [in list_representation.isomorphism]
FSetC.FSetC_prim_rec [in list_representation.list_representation]
FSetC.FSetC_rec [in list_representation.list_representation]
FSetC.FSetC_ind [in list_representation.list_representation]
fset_to_k [in subobjects.k_finite]
FSet_Unit_2 [in kuratowski.properties]
FSet_to_S [in misc.bad]
FSet_to_Bfin [in subobjects.b_finite]
FSet_to_FSetC [in list_representation.isomorphism]
FSet_to_enumeratedS [in subobjects.enumerated]
FSet_cons_beta_cons [in kuratowski.operations]
FSet_cons_beta_empty [in kuratowski.operations]
FSet_cons_rec [in kuratowski.operations]
fset_fmap [in kuratowski.operations]
FSet.FSet_rec_beta_idem [in misc.bad]
FSet.FSet_rec_beta_nr [in misc.bad]
FSet.FSet_rec_beta_nl [in misc.bad]
FSet.FSet_rec_beta_comm [in misc.bad]
FSet.FSet_rec_beta_assoc [in misc.bad]
FSet.FSet_rec [in misc.bad]
FSet.FSet_ind [in misc.bad]
FSet.FSet_rec [in kuratowski.kuratowski_sets]
FSet.FSet_ind [in kuratowski.kuratowski_sets]
fsum1 [in kuratowski.properties]
fsum2 [in kuratowski.properties]
f_eq [in interfaces.set_interface]

H

hasDecidableEmpty [in subobjects.sub]

I

isEmpty [in kuratowski.operations]

K

Kf [in subobjects.k_finite]
kf_sub [in subobjects.k_finite]
Kf_sub [in subobjects.k_finite]
Kf_sub_intern [in subobjects.k_finite]
Kf_enumerated [in subobjects.enumerated]
k_to_fset [in subobjects.k_finite]

L

lemma_4_10 [in CPP]
lemma_4_9 [in CPP]
lemma_4_6 [in CPP]
lemma_4_2 [in CPP]
lemma_2_6 [in CPP]
lemma_2_3 [in CPP]
length [in kuratowski.length]
length_disjoint [in kuratowski.length]
length_add [in kuratowski.length]
length_singleton [in kuratowski.length]
length_empty [in kuratowski.length]
listExt [in subobjects.enumerated]
listProd [in subobjects.enumerated]
listProd_sing [in subobjects.enumerated]
list_exist [in implementations.lists]
list_all [in implementations.lists]
list_to_set [in implementations.lists]
list_weaken_to_fset [in subobjects.enumerated]
list_to_fset [in subobjects.enumerated]

M

map [in subobjects.k_finite]
map [in subobjects.enumerated]
max_min [in interfaces.lattice_examples]
merely_enumeration_FSet [in subobjects.enumerated]
min [in misc.ordered]
min_set_spec [in misc.ordered]
min_set [in misc.ordered]
misc_2 [in CPP]
misc_1 [in CPP]

N

not_IP [in misc.dec_fset]
not_ZP [in misc.dec_fset]
not_YP [in misc.dec_fset]
not_XP [in misc.dec_fset]

O

operation [in interfaces.lattice_interface]

P

P [in misc.dec_fset]
p [in misc.projective]
pauli_comm [in misc.dec_fset]
Pauli_list [in misc.dec_fset]
Pauli_mult [in misc.dec_fset]
product [in kuratowski.operations]
product_isIn [in kuratowski.properties]
proposition_5_9 [in CPP]
proposition_5_5 [in CPP]
proposition_5_4 [in CPP]
proposition_5_3 [in CPP]
proposition_4_22 [in CPP]
proposition_4_18 [in CPP]
proposition_4_17 [in CPP]
proposition_4_16 [in CPP]
proposition_4_15 [in CPP]
proposition_4_12 [in CPP]
proposition_4_11 [in CPP]
proposition_4_8 [in CPP]
proposition_4_7 [in CPP]
proposition_3_12 [in CPP]
proposition_3_11 [in CPP]
proposition_3_9 [in CPP]
proposition_3_6 [in CPP]
proposition_3_5 [in CPP]
proposition_3_4 [in CPP]
proposition_3_2 [in CPP]
proposition_2_9 [in CPP]

Q

quotientB [in interfaces.set_interface]
quotientB_to_B [in interfaces.set_interface]
quotient_iso [in interfaces.set_interface]

R

R [in misc.dec_lem]
refinement [in interfaces.set_interface]
reflect_f_eq [in interfaces.set_interface]
reflect_eq [in interfaces.set_interface]
relation [in misc.ordered]
reverse [in implementations.lists]

S

separation [in kuratowski.operations]
set_length_cons [in implementations.lists]
set_length_nil [in implementations.lists]
set_length [in implementations.lists]
set_subset [in interfaces.set_interface]
set_eq [in interfaces.set_interface]
simple_example [in misc.dec_fset]
singleton [in subobjects.b_finite]
singleton_single [in implementations.lists]
singleton_isIn [in kuratowski.properties]
singleton_fin_equiv' [in subobjects.b_finite]
singleton_isIn [in interfaces.set_interface]
single_product [in kuratowski.operations]
split [in subobjects.b_finite]
squash [in prelude]
Sub [in subobjects.sub]
S1op [in misc.bad]
S1toSig [in subobjects.b_finite]
S1_merely_decidable_equality [in prelude]

T

T [in misc.dec_lem]
theorem_5_6 [in CPP]
theorem_4_23 [in CPP]
theorem_4_21 [in CPP]
theorem_3_10 [in CPP]
theorem_3_1 [in CPP]
theorem_2_8 [in CPP]
theorem_2_5 [in CPP]
top [in misc.ordered]
Top [in misc.ordered]
TR [in misc.dec_lem]
TR_one [in misc.dec_lem]
TR_zero [in misc.dec_lem]
Two_FSet_Unit [in kuratowski.properties]

U

union_isIn [in kuratowski.properties]
union_isIn [in interfaces.set_interface]

V

View [in interfaces.set_interface]

W

weaken_list_r [in subobjects.enumerated]
well_defined_sungleton [in interfaces.set_interface]
well_defined_empty [in interfaces.set_interface]
well_defined_filter [in interfaces.set_interface]
well_defined_union [in interfaces.set_interface]

X

X [in misc.dec_fset]
X [in misc.projective]
X_fin [in misc.projective]

---

Record Index

A

Absorption [in interfaces.lattice_interface]
Antisymmetric [in misc.ordered]
Associative [in interfaces.lattice_interface]

B

bottom [in interfaces.lattice_interface]

C

Commutative [in interfaces.lattice_interface]

F

Functor [in interfaces.monad_interface]

H

hasBind [in interfaces.monad_interface]
hasComprehension [in interfaces.set_names]
hasEmpty [in interfaces.set_names]
hasIntersection [in interfaces.set_names]
hasMembership [in interfaces.set_names]
hasMembership_decidable [in interfaces.set_names]
hasPure [in interfaces.monad_interface]
hasSingleton [in interfaces.set_names]
hasSubset [in interfaces.set_names]
hasSubset_decidable [in interfaces.set_names]
hasUnion [in interfaces.set_names]

I

Idempotent [in interfaces.lattice_interface]
IsProjective [in misc.projective]
IsTop [in misc.ordered]

J

JoinSemiLattice [in interfaces.lattice_interface]

L

Lattice [in interfaces.lattice_interface]
LessThan [in misc.ordered]

M

maximum [in interfaces.lattice_interface]
MerelyDecidablePaths [in prelude]
minimum [in interfaces.lattice_interface]
Monad [in interfaces.monad_interface]

N

NeutralL [in interfaces.lattice_interface]
NeutralR [in interfaces.lattice_interface]

S

sets [in interfaces.set_interface]

T

Total [in misc.ordered]
TotalOrder [in misc.ordered]

---

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

(951 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

(20 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

(3 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

(135 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

(28 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

(170 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

(36 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

(19 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

(54 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

(28 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

(91 entries)

Instance 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

(129 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

(206 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

(32 entries)

---

This page has been generated by coqdoc