Global Index

H

J

K

V

_

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

_

(27 entries)

Variable Index

A

B

E

G

H

J

K

N

O

P

R

S

T

U

V

X

Y

_

other

(76 entries)

Library Index

A

B

G

H

J

K

L

M

N

S

T

U

V

X

Y

_

other

(23 entries)

Lemma Index

A

G

H

J

K

V

X

Y

_

other

(147 entries)

Constructor Index

D

H

J

K

M

P

Q

R

T

U

V

W

X

Y

Z

_

other

(33 entries)

Inductive Index

A

B

D

G

H

J

K

M

N

P

Q

R

U

V

W

Z

_

other

(21 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

Q

R

S

T

U

V

X

Y

Z

_

other

(14 entries)

Section Index

A

B

E

G

H

J

K

N

O

P

R

S

T

U

V

X

Y

_

other

(21 entries)

Definition Index

H

J

K

U

V

Z

_

other

(60 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

Q

R

S

T

U

V

X

Y

Z

_

other

(5 entries)

Global Index

A

add_finite [constructor, in ZornsLemma.FiniteTypes]
aleph0 [definition, in ZornsLemma.Cardinals]

B

bijective [definition, in ZornsLemma.FunctionProperties]
bijective_impl_invertible [lemma, in ZornsLemma.FunctionProperties]
bij_finite [constructor, in ZornsLemma.FiniteTypes]
bij_eq_cardinal [constructor, in ZornsLemma.Cardinals]

C

cantor_diag2 [lemma, in ZornsLemma.Cardinals]
cantor_diag [lemma, in ZornsLemma.Cardinals]
Cardinal [inductive, in ZornsLemma.Cardinals]
cardinality [constructor, in ZornsLemma.Cardinals]
Cardinals [library]
cardinals_unbounded [lemma, in ZornsLemma.Cardinals]
chain [definition, in ZornsLemma.ZornsLemma]
chains [definition, in ZornsLemma.ZornsLemma]
chains_sup [definition, in ZornsLemma.ZornsLemma]
chains_sup_correct [lemma, in ZornsLemma.ZornsLemma]
chains_sup_def [definition, in ZornsLemma.ZornsLemma]
chains_order [lemma, in ZornsLemma.ZornsLemma]
chains_ord [definition, in ZornsLemma.ZornsLemma]
characteristic_function_to_ensemble_is_identity [lemma, in ZornsLemma.EnsemblesSpec]
characteristic_function_to_ensemble [definition, in ZornsLemma.EnsemblesSpec]
characteristic_function_abstraction [inductive, in ZornsLemma.EnsemblesSpec]
choice_on_dependent_type [lemma, in ZornsLemma.DependentTypeChoice]
Classical_Wf [library]
classic_dec [lemma, in ZornsLemma.DecidableDec]
Countable [definition, in ZornsLemma.CountableTypes]
CountableT [inductive, in ZornsLemma.CountableTypes]
CountableTypes [library]
CountableT_is_FiniteT_or_countably_infinite [lemma, in ZornsLemma.CountableTypes]
countable_union [lemma, in ZornsLemma.CountableTypes]
countable_type_ensemble [lemma, in ZornsLemma.CountableTypes]
countable_img [lemma, in ZornsLemma.CountableTypes]
countable_downward_closed [lemma, in ZornsLemma.CountableTypes]
countable_exp [lemma, in ZornsLemma.CountableTypes]
countable_product [lemma, in ZornsLemma.CountableTypes]
countable_sum [lemma, in ZornsLemma.CountableTypes]
countable_nat_product [lemma, in ZornsLemma.CountableTypes]
CSB [lemma, in ZornsLemma.CSB]
CSB [section, in ZornsLemma.CSB]
CSB [library]
CSB_comp2 [lemma, in ZornsLemma.CSB]
CSB_comp1 [lemma, in ZornsLemma.CSB]
CSB_bijection2 [definition, in ZornsLemma.CSB]
CSB_bijection [definition, in ZornsLemma.CSB]
CSB.f [variable, in ZornsLemma.CSB]
CSB.f_inj [variable, in ZornsLemma.CSB]
CSB.g [variable, in ZornsLemma.CSB]
CSB.g_inj [variable, in ZornsLemma.CSB]
CSB.X [variable, in ZornsLemma.CSB]
CSB.Y [variable, in ZornsLemma.CSB]

D

DecidableDec [library]
decidable_dec [lemma, in ZornsLemma.DecidableDec]
DecreasingSequences [section, in ZornsLemma.Classical_Wf]
DecreasingSequences.R [variable, in ZornsLemma.Classical_Wf]
DecreasingSequences.T [variable, in ZornsLemma.Classical_Wf]
decreasing_sequence_property [definition, in ZornsLemma.Classical_Wf]
DependentTypeChoice [library]
description_of_fbar [lemma, in ZornsLemma.Quotients]
DSP_implies_WF [lemma, in ZornsLemma.Classical_Wf]

E

empty_indexed_union [lemma, in ZornsLemma.IndexedFamilies]
empty_indexed_intersection [lemma, in ZornsLemma.IndexedFamilies]
empty_finite [constructor, in ZornsLemma.FiniteTypes]
empty_family_intersection [lemma, in ZornsLemma.Families]
empty_family_union [lemma, in ZornsLemma.Families]
EnsemblesImplicit [library]
EnsemblesSpec [library]
EnsemblesUtf8 [library]
equality_of_equiv_class_impl_R [lemma, in ZornsLemma.Quotients]
equiv_class_in_quotient [lemma, in ZornsLemma.Quotients]
equiv_classes [definition, in ZornsLemma.Quotients]
equiv_class [definition, in ZornsLemma.Quotients]
eq_cardinal_impl_le_cardinal [lemma, in ZornsLemma.Cardinals]
eq_cardinal_equiv [lemma, in ZornsLemma.Cardinals]
eq_cardinal [inductive, in ZornsLemma.Cardinals]
eq_fn_equiv [lemma, in ZornsLemma.Quotients]
eq_fn [definition, in ZornsLemma.Quotients]
eval [definition, in ZornsLemma.Quotients]
even_odd_excl2 [lemma, in ZornsLemma.CSB]
even_odd_excl [lemma, in ZornsLemma.CSB]
exclusive_dec [lemma, in ZornsLemma.DecidableDec]
extend_strictly_partial_WO_correct [lemma, in ZornsLemma.WellOrders]
extend_strictly_partial_WO [definition, in ZornsLemma.WellOrders]

F

Families [section, in ZornsLemma.Families]
Families [library]
Families.F [variable, in ZornsLemma.Families]
Families.T [variable, in ZornsLemma.Families]
Family [definition, in ZornsLemma.Families]
FamilyFacts [section, in ZornsLemma.Families]
FamilyFacts.T [variable, in ZornsLemma.Families]
FamilyIntersection [inductive, in ZornsLemma.Families]
FamilyUnion [inductive, in ZornsLemma.Families]
family_intersection_intro [constructor, in ZornsLemma.Families]
family_union_intro [constructor, in ZornsLemma.Families]
FiniteIntersections [library]
FiniteT [inductive, in ZornsLemma.FiniteTypes]
FiniteTypes [library]
FiniteT_impl_CountableT [lemma, in ZornsLemma.CountableTypes]
FiniteT_nat_cardinal_bijection [lemma, in ZornsLemma.FiniteTypes]
FiniteT_nat_cardinal_option [lemma, in ZornsLemma.FiniteTypes]
FiniteT_nat_cardinal_False [lemma, in ZornsLemma.FiniteTypes]
FiniteT_nat_cardinal_cond [lemma, in ZornsLemma.FiniteTypes]
FiniteT_nat_cardinal_def [lemma, in ZornsLemma.FiniteTypes]
FiniteT_nat_cardinal [definition, in ZornsLemma.FiniteTypes]
FiniteT_has_nat_cardinal [lemma, in ZornsLemma.FiniteTypes]
FiniteT_img [lemma, in ZornsLemma.FiniteTypes]
Finite_impl_Countable [lemma, in ZornsLemma.CountableTypes]
finite_exp [lemma, in ZornsLemma.FiniteTypes]
finite_prod [lemma, in ZornsLemma.FiniteTypes]
finite_sum [lemma, in ZornsLemma.FiniteTypes]
finite_surj_inj [lemma, in ZornsLemma.FiniteTypes]
finite_inj_surj [lemma, in ZornsLemma.FiniteTypes]
finite_subtype [lemma, in ZornsLemma.FiniteTypes]
Finite_ens_type [lemma, in ZornsLemma.FiniteTypes]
finite_choice [lemma, in ZornsLemma.FiniteTypes]
finite_dep_choice [lemma, in ZornsLemma.FiniteTypes]
finite_eq_dec [lemma, in ZornsLemma.FiniteTypes]
finite_dec_forall [lemma, in ZornsLemma.FiniteTypes]
finite_dec_exists [lemma, in ZornsLemma.FiniteTypes]
finite_nat_initial_segment [lemma, in ZornsLemma.InfiniteTypes]
finite_indexed_intersection_is_finite_intersection [lemma, in ZornsLemma.FiniteIntersections]
finite_intersection_is_finite_indexed_intersection [lemma, in ZornsLemma.FiniteIntersections]
finite_intersections [inductive, in ZornsLemma.FiniteIntersections]
finv [definition, in ZornsLemma.CSB]
finv_noteven [definition, in ZornsLemma.CSB]
FunctionProperties [library]
function_inverse [definition, in ZornsLemma.FunctionProperties]
f_X_odd [constructor, in ZornsLemma.CSB]
f_X_even [constructor, in ZornsLemma.CSB]

G

ge_cardinal [definition, in ZornsLemma.Cardinals]
ginv [definition, in ZornsLemma.CSB]
ginv_odd [definition, in ZornsLemma.CSB]
gt_cardinal [definition, in ZornsLemma.Cardinals]
g_Y_even [constructor, in ZornsLemma.CSB]
g_Y_odd [constructor, in ZornsLemma.CSB]

I

ImageFamily [definition, in ZornsLemma.IndexedFamilies]
ImageImplicit [library]
IndexedFamilies [section, in ZornsLemma.IndexedFamilies]
IndexedFamilies [library]
IndexedFamilies.A [variable, in ZornsLemma.IndexedFamilies]
IndexedFamilies.F [variable, in ZornsLemma.IndexedFamilies]
IndexedFamilies.T [variable, in ZornsLemma.IndexedFamilies]
IndexedFamily [definition, in ZornsLemma.IndexedFamilies]
IndexedFamilyFacts [section, in ZornsLemma.IndexedFamilies]
IndexedFamilyToFamily [section, in ZornsLemma.IndexedFamilies]
IndexedFamilyToFamily.A [variable, in ZornsLemma.IndexedFamilies]
IndexedFamilyToFamily.F [variable, in ZornsLemma.IndexedFamilies]
IndexedFamilyToFamily.T [variable, in ZornsLemma.IndexedFamilies]
IndexedIntersection [inductive, in ZornsLemma.IndexedFamilies]
IndexedUnion [inductive, in ZornsLemma.IndexedFamilies]
indexed_to_family_intersection [lemma, in ZornsLemma.IndexedFamilies]
indexed_to_family_union [lemma, in ZornsLemma.IndexedFamilies]
indexed_intersection_intro [constructor, in ZornsLemma.IndexedFamilies]
indexed_union_intro [constructor, in ZornsLemma.IndexedFamilies]
InducedFunction [section, in ZornsLemma.Quotients]
InducedFunction.A [variable, in ZornsLemma.Quotients]
InducedFunction.B [variable, in ZornsLemma.Quotients]
InducedFunction.equiv [variable, in ZornsLemma.Quotients]
InducedFunction.f [variable, in ZornsLemma.Quotients]
InducedFunction.R [variable, in ZornsLemma.Quotients]
InducedFunction.well_defined [variable, in ZornsLemma.Quotients]
InducedFunction2 [section, in ZornsLemma.Quotients]
InducedFunction2arg [section, in ZornsLemma.Quotients]
InducedFunction2arg.A [variable, in ZornsLemma.Quotients]
InducedFunction2arg.B [variable, in ZornsLemma.Quotients]
InducedFunction2arg.C [variable, in ZornsLemma.Quotients]
InducedFunction2arg.equivR [variable, in ZornsLemma.Quotients]
InducedFunction2arg.equivS [variable, in ZornsLemma.Quotients]
InducedFunction2arg.f [variable, in ZornsLemma.Quotients]
InducedFunction2arg.R [variable, in ZornsLemma.Quotients]
InducedFunction2arg.S [variable, in ZornsLemma.Quotients]
InducedFunction2arg.well_defined_2arg [variable, in ZornsLemma.Quotients]
InducedFunction2.A [variable, in ZornsLemma.Quotients]
InducedFunction2.B [variable, in ZornsLemma.Quotients]
InducedFunction2.equivR [variable, in ZornsLemma.Quotients]
InducedFunction2.equivS [variable, in ZornsLemma.Quotients]
InducedFunction2.f [variable, in ZornsLemma.Quotients]
InducedFunction2.R [variable, in ZornsLemma.Quotients]
InducedFunction2.S [variable, in ZornsLemma.Quotients]
InducedFunction2.well_defined2 [variable, in ZornsLemma.Quotients]
InducedFunction3 [section, in ZornsLemma.Quotients]
InducedFunction3.A [variable, in ZornsLemma.Quotients]
InducedFunction3.B [variable, in ZornsLemma.Quotients]
InducedFunction3.C [variable, in ZornsLemma.Quotients]
InducedFunction3.equivR [variable, in ZornsLemma.Quotients]
InducedFunction3.equivS [variable, in ZornsLemma.Quotients]
InducedFunction3.equivT [variable, in ZornsLemma.Quotients]
InducedFunction3.f [variable, in ZornsLemma.Quotients]
InducedFunction3.R [variable, in ZornsLemma.Quotients]
InducedFunction3.S [variable, in ZornsLemma.Quotients]
InducedFunction3.T [variable, in ZornsLemma.Quotients]
InducedFunction3.well_defined3 [variable, in ZornsLemma.Quotients]
induced_function3_correct [lemma, in ZornsLemma.Quotients]
induced_function3 [definition, in ZornsLemma.Quotients]
induced_function2arg_correct [lemma, in ZornsLemma.Quotients]
induced_function2arg [definition, in ZornsLemma.Quotients]
induced_eval [definition, in ZornsLemma.Quotients]
induced_function2_correct [lemma, in ZornsLemma.Quotients]
induced_function2 [definition, in ZornsLemma.Quotients]
induced_function_unique [lemma, in ZornsLemma.Quotients]
induced_function_correct [lemma, in ZornsLemma.Quotients]
induced_function [definition, in ZornsLemma.Quotients]
induced1 [definition, in ZornsLemma.Quotients]
induced2 [definition, in ZornsLemma.Quotients]
InfiniteTypes [library]
infinite_nat_inj [lemma, in ZornsLemma.InfiniteTypes]
inflation_intro [constructor, in ZornsLemma.ZornsLemma]
injection_preserves_cardinal [lemma, in ZornsLemma.FiniteTypes]
injective [definition, in ZornsLemma.FunctionProperties]
inj_countable [lemma, in ZornsLemma.CountableTypes]
inj_finite [lemma, in ZornsLemma.FiniteTypes]
inj_le_cardinal [constructor, in ZornsLemma.Cardinals]
intro_invertible [constructor, in ZornsLemma.FunctionProperties]
intro_nat_injection [constructor, in ZornsLemma.CountableTypes]
intro_intersection [constructor, in ZornsLemma.FiniteIntersections]
intro_S [constructor, in ZornsLemma.FiniteIntersections]
intro_full [constructor, in ZornsLemma.FiniteIntersections]
intro_characteristic_sat [constructor, in ZornsLemma.EnsemblesSpec]
intro_limit_ord [constructor, in ZornsLemma.Ordinals]
intro_succ_ord [constructor, in ZornsLemma.Ordinals]
InverseImage [library]
inverse_image_composition [lemma, in ZornsLemma.InverseImage]
inverse_image_complement [lemma, in ZornsLemma.InverseImage]
inverse_image_union [lemma, in ZornsLemma.InverseImage]
inverse_image_intersection [lemma, in ZornsLemma.InverseImage]
inverse_image_full [lemma, in ZornsLemma.InverseImage]
inverse_image_empty [lemma, in ZornsLemma.InverseImage]
inverse_image_increasing [lemma, in ZornsLemma.InverseImage]
inverse_image [definition, in ZornsLemma.InverseImage]
invertible [inductive, in ZornsLemma.FunctionProperties]
invertible_impl_bijective [lemma, in ZornsLemma.FunctionProperties]

L

le_cardinal_total [lemma, in ZornsLemma.Cardinals]
le_cardinal_total.Y [variable, in ZornsLemma.Cardinals]
le_cardinal_total.X [variable, in ZornsLemma.Cardinals]
le_cardinal_total [section, in ZornsLemma.Cardinals]
le_cardinal_antisym [lemma, in ZornsLemma.Cardinals]
le_cardinal_preorder [lemma, in ZornsLemma.Cardinals]
le_cardinal [inductive, in ZornsLemma.Cardinals]
limit_ord_wd [constructor, in ZornsLemma.Ordinals]
limit_ordinal [inductive, in ZornsLemma.Ordinals]
lt_cardinal [definition, in ZornsLemma.Cardinals]

M

maximal [definition, in ZornsLemma.ZornsLemma]
MEP_implies_WF [lemma, in ZornsLemma.Classical_Wf]
MinimalElements [section, in ZornsLemma.Classical_Wf]
MinimalElements.R [variable, in ZornsLemma.Classical_Wf]
MinimalElements.T [variable, in ZornsLemma.Classical_Wf]
minimal_element_property [definition, in ZornsLemma.Classical_Wf]

N

nat_infinite [lemma, in ZornsLemma.InfiniteTypes]
nat_to_cardinal [definition, in ZornsLemma.Cardinals]
not_f_img [constructor, in ZornsLemma.CSB]
not_g_img [constructor, in ZornsLemma.CSB]
n_element_set [definition, in ZornsLemma.Cardinals]

O

Ordinal [inductive, in ZornsLemma.Ordinals]
Ordinals [library]
ordinals_well_founded [lemma, in ZornsLemma.Ordinals]
ordS [constructor, in ZornsLemma.Ordinals]
ord_successor_or_limit [lemma, in ZornsLemma.Ordinals]
ord_lt_irrefl [lemma, in ZornsLemma.Ordinals]
ord_total_order [lemma, in ZornsLemma.Ordinals]
ord_lt_respects_succ [lemma, in ZornsLemma.Ordinals]
ord_lt_trans [lemma, in ZornsLemma.Ordinals]
ord_le_lt_trans [lemma, in ZornsLemma.Ordinals]
ord_lt_le_trans [lemma, in ZornsLemma.Ordinals]
ord_lt_le [lemma, in ZornsLemma.Ordinals]
ord_le_S [lemma, in ZornsLemma.Ordinals]
ord_le_refl [lemma, in ZornsLemma.Ordinals]
ord_le_sup [lemma, in ZornsLemma.Ordinals]
ord_le_trans [lemma, in ZornsLemma.Ordinals]
ord_sup_minimal_converse [lemma, in ZornsLemma.Ordinals]
ord_le_S_sup_converse [lemma, in ZornsLemma.Ordinals]
ord_le_respects_succ_converse [lemma, in ZornsLemma.Ordinals]
ord_gt [definition, in ZornsLemma.Ordinals]
ord_ge [definition, in ZornsLemma.Ordinals]
ord_eq [definition, in ZornsLemma.Ordinals]
ord_lt [definition, in ZornsLemma.Ordinals]
ord_sup_minimal [constructor, in ZornsLemma.Ordinals]
ord_le_S_sup [constructor, in ZornsLemma.Ordinals]
ord_le_respects_succ [constructor, in ZornsLemma.Ordinals]
ord_le [inductive, in ZornsLemma.Ordinals]
ord_sup [constructor, in ZornsLemma.Ordinals]

P

partial_WO_chain_ub_correct [lemma, in ZornsLemma.WellOrders]
partial_WO_chain_ub [definition, in ZornsLemma.WellOrders]
partial_WO_preord [lemma, in ZornsLemma.WellOrders]
partial_WO_ord [record, in ZornsLemma.WellOrders]
partial_WO [record, in ZornsLemma.WellOrders]
partial_injection_chain_ub [lemma, in ZornsLemma.Cardinals]
partial_injection_preord [lemma, in ZornsLemma.Cardinals]
partial_injection_ord [record, in ZornsLemma.Cardinals]
partial_injection [record, in ZornsLemma.Cardinals]
pi_func_ext [projection, in ZornsLemma.Cardinals]
pi_dom_inc [projection, in ZornsLemma.Cardinals]
pi_inj [projection, in ZornsLemma.Cardinals]
pi_func [projection, in ZornsLemma.Cardinals]
pi_dom [projection, in ZornsLemma.Cardinals]
positive_countable [lemma, in ZornsLemma.CountableTypes]
premaximal [definition, in ZornsLemma.ZornsLemma]
premaximal_partial_WO_is_full [lemma, in ZornsLemma.WellOrders]
premaximal_pi_is_full_or_surj [lemma, in ZornsLemma.Cardinals]
premaximal_partial_injection [lemma, in ZornsLemma.Cardinals]
projf [definition, in ZornsLemma.Quotients]
projf_well_defined [lemma, in ZornsLemma.Quotients]
projf2 [definition, in ZornsLemma.Quotients]
projf2_well_defined [lemma, in ZornsLemma.Quotients]
Proj1SigInjective [library]
proj1_sig_injective [lemma, in ZornsLemma.Proj1SigInjective]
pwo_downward_closed [projection, in ZornsLemma.WellOrders]
pwo_restriction [projection, in ZornsLemma.WellOrders]
pwo_S_incl [projection, in ZornsLemma.WellOrders]
pwo_wo [projection, in ZornsLemma.WellOrders]
pwo_R_lives_on_S [projection, in ZornsLemma.WellOrders]
pwo_R [projection, in ZornsLemma.WellOrders]
pwo_S [projection, in ZornsLemma.WellOrders]
P_neq_not_P [lemma, in ZornsLemma.Cardinals]

Q

quotient [definition, in ZornsLemma.Quotients]
Quotient [section, in ZornsLemma.Quotients]
Quotients [library]
quotient_projection_minimally_collapses_R [lemma, in ZornsLemma.Quotients]
quotient_projection_collapses_R [lemma, in ZornsLemma.Quotients]
quotient_projection_surjective [lemma, in ZornsLemma.Quotients]
quotient_projection_correct [lemma, in ZornsLemma.Quotients]
quotient_projection [definition, in ZornsLemma.Quotients]
Quotient.A [variable, in ZornsLemma.Quotients]
Quotient.equivR [variable, in ZornsLemma.Quotients]
Quotient.R [variable, in ZornsLemma.Quotients]
Q_countable [lemma, in ZornsLemma.CountableTypes]

R

Relation_Definitions_Implicit [library]
restriction_relation [definition, in ZornsLemma.WellOrders]
R_impl_equality_of_equiv_class [lemma, in ZornsLemma.Quotients]

S

slices_well_defined [lemma, in ZornsLemma.Quotients]
subfamily_intersection [lemma, in ZornsLemma.Families]
subfamily_union [lemma, in ZornsLemma.Families]
subset_eq_compatT [lemma, in ZornsLemma.Proj1SigInjective]
sub_indexed_intersection [lemma, in ZornsLemma.IndexedFamilies]
sub_indexed_union [lemma, in ZornsLemma.IndexedFamilies]
successor_ordinal_not_limit [lemma, in ZornsLemma.Ordinals]
successor_ordinal [inductive, in ZornsLemma.Ordinals]
succ_ord_wd [constructor, in ZornsLemma.Ordinals]
sup_intro [constructor, in ZornsLemma.ZornsLemma]
surjective [definition, in ZornsLemma.FunctionProperties]
surj_countable [lemma, in ZornsLemma.CountableTypes]
surj_finite [lemma, in ZornsLemma.FiniteTypes]
surj_le_cardinal [lemma, in ZornsLemma.Cardinals]

T

total_strict_order [definition, in ZornsLemma.WellOrders]
tower [inductive, in ZornsLemma.ZornsLemma]
tower_is_chain [lemma, in ZornsLemma.ZornsLemma]
True_finite [lemma, in ZornsLemma.FiniteTypes]
types_comparable [lemma, in ZornsLemma.Cardinals]

U

unique_inverse [lemma, in ZornsLemma.FunctionProperties]
unique_FiniteT_nat_cardinal [lemma, in ZornsLemma.FiniteTypes]

W

WellOrder [section, in ZornsLemma.WellOrders]
WellOrderConstruction [section, in ZornsLemma.WellOrders]
WellOrderConstruction.T [variable, in ZornsLemma.WellOrders]
WellOrderMinimum [section, in ZornsLemma.WellOrders]
WellOrderMinimum.R [variable, in ZornsLemma.WellOrders]
WellOrderMinimum.T [variable, in ZornsLemma.WellOrders]
WellOrderMinimum.well_ord [variable, in ZornsLemma.WellOrders]
WellOrders [library]
WellOrder.T [variable, in ZornsLemma.WellOrders]
well_orderable [lemma, in ZornsLemma.WellOrders]
well_order [record, in ZornsLemma.WellOrders]
well_defined_eval [lemma, in ZornsLemma.Quotients]
well_defined_induced1 [lemma, in ZornsLemma.Quotients]
WF_implies_DSP [lemma, in ZornsLemma.Classical_Wf]
WF_implies_MEP [lemma, in ZornsLemma.Classical_Wf]
WO_implies_AC [lemma, in ZornsLemma.WellOrders]
WO_implies_AC [section, in ZornsLemma.WellOrders]
WO_minimum [definition, in ZornsLemma.WellOrders]
wo_transitive [lemma, in ZornsLemma.WellOrders]
wo_antisym [lemma, in ZornsLemma.WellOrders]
wo_irrefl [lemma, in ZornsLemma.WellOrders]
wo_total_strict_order [projection, in ZornsLemma.WellOrders]
wo_well_founded [projection, in ZornsLemma.WellOrders]

X

X_odd_coind [definition, in ZornsLemma.CSB]
X_even_coind [definition, in ZornsLemma.CSB]
X_odd [inductive, in ZornsLemma.CSB]
X_even [inductive, in ZornsLemma.CSB]

Y

Y_even_coind [definition, in ZornsLemma.CSB]
Y_odd_coind [definition, in ZornsLemma.CSB]
Y_even [inductive, in ZornsLemma.CSB]
Y_odd [inductive, in ZornsLemma.CSB]

Z

ZL [section, in ZornsLemma.ZornsLemma]
ZL_preorder.ub_of_chain [variable, in ZornsLemma.ZornsLemma]
ZL_preorder.Rpreord [variable, in ZornsLemma.ZornsLemma]
ZL_preorder.R [variable, in ZornsLemma.ZornsLemma]
ZL_preorder.T [variable, in ZornsLemma.ZornsLemma]
ZL_preorder [section, in ZornsLemma.ZornsLemma]
ZL' [lemma, in ZornsLemma.ZornsLemma]
ZL' [section, in ZornsLemma.ZornsLemma]
ZL'.chain_sup [variable, in ZornsLemma.ZornsLemma]
ZL'.inflation [variable, in ZornsLemma.ZornsLemma]
ZL'.ord [variable, in ZornsLemma.ZornsLemma]
ZL'.R [variable, in ZornsLemma.ZornsLemma]
ZL'.T [variable, in ZornsLemma.ZornsLemma]
ZL.ord [variable, in ZornsLemma.ZornsLemma]
ZL.R [variable, in ZornsLemma.ZornsLemma]
ZL.T [variable, in ZornsLemma.ZornsLemma]
ZL.ub_of_chain [variable, in ZornsLemma.ZornsLemma]
ZornsLemma [lemma, in ZornsLemma.ZornsLemma]
ZornsLemma [library]
ZornsLemmaForPreorders [lemma, in ZornsLemma.ZornsLemma]
Z_countable [lemma, in ZornsLemma.CountableTypes]

other

_ >= _ (ordinal_scope) [notation, in ZornsLemma.Ordinals]
_ > _ (ordinal_scope) [notation, in ZornsLemma.Ordinals]
_ == _ (ordinal_scope) [notation, in ZornsLemma.Ordinals]
_ <= _ (ordinal_scope) [notation, in ZornsLemma.Ordinals]
_ < _ (ordinal_scope) [notation, in ZornsLemma.Ordinals]
_ < _ [notation, in ZornsLemma.EnsemblesUtf8]
_ ⊊ _ [notation, in ZornsLemma.EnsemblesUtf8]
_ <= _ [notation, in ZornsLemma.EnsemblesUtf8]
_ ⊆ _ [notation, in ZornsLemma.EnsemblesUtf8]
_ \ _ [notation, in ZornsLemma.EnsemblesUtf8]
_ ∖ _ [notation, in ZornsLemma.EnsemblesUtf8]
_ \\// _ [notation, in ZornsLemma.EnsemblesUtf8]
_ ∪ _ [notation, in ZornsLemma.EnsemblesUtf8]
_ //\\ _ [notation, in ZornsLemma.EnsemblesUtf8]
_ ∩ _ [notation, in ZornsLemma.EnsemblesUtf8]
_ ∈ _ [notation, in ZornsLemma.EnsemblesUtf8]
//\\ [ _ : _ ] _ [notation, in ZornsLemma.EnsemblesUtf8]
[ _ : _ | _ ] [notation, in ZornsLemma.EnsemblesSpec]
[[ _ , _ , _ ]] [notation, in ZornsLemma.EnsemblesUtf8]
[[ _ , _ ]] [notation, in ZornsLemma.EnsemblesUtf8]
[[ _ ]] [notation, in ZornsLemma.EnsemblesUtf8]
\\// [ _ : _ ] _ [notation, in ZornsLemma.EnsemblesUtf8]
∅ [notation, in ZornsLemma.EnsemblesUtf8]
⋂ [ _ : _ ] _ [notation, in ZornsLemma.EnsemblesUtf8]
⋂ _ [notation, in ZornsLemma.EnsemblesUtf8]
⋃ [ _ : _ ] _ [notation, in ZornsLemma.EnsemblesUtf8]
⋃ _ [notation, in ZornsLemma.EnsemblesUtf8]

Notation Index

other

_ >= _ (ordinal_scope) [in ZornsLemma.Ordinals]
_ > _ (ordinal_scope) [in ZornsLemma.Ordinals]
_ == _ (ordinal_scope) [in ZornsLemma.Ordinals]
_ <= _ (ordinal_scope) [in ZornsLemma.Ordinals]
_ < _ (ordinal_scope) [in ZornsLemma.Ordinals]
_ < _ [in ZornsLemma.EnsemblesUtf8]
_ ⊊ _ [in ZornsLemma.EnsemblesUtf8]
_ <= _ [in ZornsLemma.EnsemblesUtf8]
_ ⊆ _ [in ZornsLemma.EnsemblesUtf8]
_ \ _ [in ZornsLemma.EnsemblesUtf8]
_ ∖ _ [in ZornsLemma.EnsemblesUtf8]
_ \\// _ [in ZornsLemma.EnsemblesUtf8]
_ ∪ _ [in ZornsLemma.EnsemblesUtf8]
_ //\\ _ [in ZornsLemma.EnsemblesUtf8]
_ ∩ _ [in ZornsLemma.EnsemblesUtf8]
_ ∈ _ [in ZornsLemma.EnsemblesUtf8]
//\\ [ _ : _ ] _ [in ZornsLemma.EnsemblesUtf8]
[ _ : _ | _ ] [in ZornsLemma.EnsemblesSpec]
[[ _ , _ , _ ]] [in ZornsLemma.EnsemblesUtf8]
[[ _ , _ ]] [in ZornsLemma.EnsemblesUtf8]
[[ _ ]] [in ZornsLemma.EnsemblesUtf8]
\\// [ _ : _ ] _ [in ZornsLemma.EnsemblesUtf8]
∅ [in ZornsLemma.EnsemblesUtf8]
⋂ [ _ : _ ] _ [in ZornsLemma.EnsemblesUtf8]
⋂ _ [in ZornsLemma.EnsemblesUtf8]
⋃ [ _ : _ ] _ [in ZornsLemma.EnsemblesUtf8]
⋃ _ [in ZornsLemma.EnsemblesUtf8]

Variable Index

C

CSB.f [in ZornsLemma.CSB]
CSB.f_inj [in ZornsLemma.CSB]
CSB.g [in ZornsLemma.CSB]
CSB.g_inj [in ZornsLemma.CSB]
CSB.X [in ZornsLemma.CSB]
CSB.Y [in ZornsLemma.CSB]

D

DecreasingSequences.R [in ZornsLemma.Classical_Wf]
DecreasingSequences.T [in ZornsLemma.Classical_Wf]

F

Families.F [in ZornsLemma.Families]
Families.T [in ZornsLemma.Families]
FamilyFacts.T [in ZornsLemma.Families]

I

IndexedFamilies.A [in ZornsLemma.IndexedFamilies]
IndexedFamilies.F [in ZornsLemma.IndexedFamilies]
IndexedFamilies.T [in ZornsLemma.IndexedFamilies]
IndexedFamilyToFamily.A [in ZornsLemma.IndexedFamilies]
IndexedFamilyToFamily.F [in ZornsLemma.IndexedFamilies]
IndexedFamilyToFamily.T [in ZornsLemma.IndexedFamilies]
InducedFunction.A [in ZornsLemma.Quotients]
InducedFunction.B [in ZornsLemma.Quotients]
InducedFunction.equiv [in ZornsLemma.Quotients]
InducedFunction.f [in ZornsLemma.Quotients]
InducedFunction.R [in ZornsLemma.Quotients]
InducedFunction.well_defined [in ZornsLemma.Quotients]
InducedFunction2arg.A [in ZornsLemma.Quotients]
InducedFunction2arg.B [in ZornsLemma.Quotients]
InducedFunction2arg.C [in ZornsLemma.Quotients]
InducedFunction2arg.equivR [in ZornsLemma.Quotients]
InducedFunction2arg.equivS [in ZornsLemma.Quotients]
InducedFunction2arg.f [in ZornsLemma.Quotients]
InducedFunction2arg.R [in ZornsLemma.Quotients]
InducedFunction2arg.S [in ZornsLemma.Quotients]
InducedFunction2arg.well_defined_2arg [in ZornsLemma.Quotients]
InducedFunction2.A [in ZornsLemma.Quotients]
InducedFunction2.B [in ZornsLemma.Quotients]
InducedFunction2.equivR [in ZornsLemma.Quotients]
InducedFunction2.equivS [in ZornsLemma.Quotients]
InducedFunction2.f [in ZornsLemma.Quotients]
InducedFunction2.R [in ZornsLemma.Quotients]
InducedFunction2.S [in ZornsLemma.Quotients]
InducedFunction2.well_defined2 [in ZornsLemma.Quotients]
InducedFunction3.A [in ZornsLemma.Quotients]
InducedFunction3.B [in ZornsLemma.Quotients]
InducedFunction3.C [in ZornsLemma.Quotients]
InducedFunction3.equivR [in ZornsLemma.Quotients]
InducedFunction3.equivS [in ZornsLemma.Quotients]
InducedFunction3.equivT [in ZornsLemma.Quotients]
InducedFunction3.f [in ZornsLemma.Quotients]
InducedFunction3.R [in ZornsLemma.Quotients]
InducedFunction3.S [in ZornsLemma.Quotients]
InducedFunction3.T [in ZornsLemma.Quotients]
InducedFunction3.well_defined3 [in ZornsLemma.Quotients]

L

le_cardinal_total.Y [in ZornsLemma.Cardinals]
le_cardinal_total.X [in ZornsLemma.Cardinals]

M

MinimalElements.R [in ZornsLemma.Classical_Wf]
MinimalElements.T [in ZornsLemma.Classical_Wf]

Q

Quotient.A [in ZornsLemma.Quotients]
Quotient.equivR [in ZornsLemma.Quotients]
Quotient.R [in ZornsLemma.Quotients]

W

WellOrderConstruction.T [in ZornsLemma.WellOrders]
WellOrderMinimum.R [in ZornsLemma.WellOrders]
WellOrderMinimum.T [in ZornsLemma.WellOrders]
WellOrderMinimum.well_ord [in ZornsLemma.WellOrders]
WellOrder.T [in ZornsLemma.WellOrders]

Z

ZL_preorder.ub_of_chain [in ZornsLemma.ZornsLemma]
ZL_preorder.Rpreord [in ZornsLemma.ZornsLemma]
ZL_preorder.R [in ZornsLemma.ZornsLemma]
ZL_preorder.T [in ZornsLemma.ZornsLemma]
ZL'.chain_sup [in ZornsLemma.ZornsLemma]
ZL'.inflation [in ZornsLemma.ZornsLemma]
ZL'.ord [in ZornsLemma.ZornsLemma]
ZL'.R [in ZornsLemma.ZornsLemma]
ZL'.T [in ZornsLemma.ZornsLemma]
ZL.ord [in ZornsLemma.ZornsLemma]
ZL.R [in ZornsLemma.ZornsLemma]
ZL.T [in ZornsLemma.ZornsLemma]
ZL.ub_of_chain [in ZornsLemma.ZornsLemma]

Library Index

C

Cardinals
Classical_Wf
CountableTypes
CSB

D

DecidableDec
DependentTypeChoice

E

EnsemblesImplicit
EnsemblesSpec
EnsemblesUtf8

F

Families
FiniteIntersections
FiniteTypes
FunctionProperties

I

ImageImplicit
IndexedFamilies
InfiniteTypes
InverseImage

O

P

Proj1SigInjective

Q

R

Relation_Definitions_Implicit

W

Z

Lemma Index

B

bijective_impl_invertible [in ZornsLemma.FunctionProperties]

C

cantor_diag2 [in ZornsLemma.Cardinals]
cantor_diag [in ZornsLemma.Cardinals]
cardinals_unbounded [in ZornsLemma.Cardinals]
chains_sup_correct [in ZornsLemma.ZornsLemma]
chains_order [in ZornsLemma.ZornsLemma]
characteristic_function_to_ensemble_is_identity [in ZornsLemma.EnsemblesSpec]
choice_on_dependent_type [in ZornsLemma.DependentTypeChoice]
classic_dec [in ZornsLemma.DecidableDec]
CountableT_is_FiniteT_or_countably_infinite [in ZornsLemma.CountableTypes]
countable_union [in ZornsLemma.CountableTypes]
countable_type_ensemble [in ZornsLemma.CountableTypes]
countable_img [in ZornsLemma.CountableTypes]
countable_downward_closed [in ZornsLemma.CountableTypes]
countable_exp [in ZornsLemma.CountableTypes]
countable_product [in ZornsLemma.CountableTypes]
countable_sum [in ZornsLemma.CountableTypes]
countable_nat_product [in ZornsLemma.CountableTypes]
CSB [in ZornsLemma.CSB]
CSB_comp2 [in ZornsLemma.CSB]
CSB_comp1 [in ZornsLemma.CSB]

D

decidable_dec [in ZornsLemma.DecidableDec]
description_of_fbar [in ZornsLemma.Quotients]
DSP_implies_WF [in ZornsLemma.Classical_Wf]

E

empty_indexed_union [in ZornsLemma.IndexedFamilies]
empty_indexed_intersection [in ZornsLemma.IndexedFamilies]
empty_family_intersection [in ZornsLemma.Families]
empty_family_union [in ZornsLemma.Families]
equality_of_equiv_class_impl_R [in ZornsLemma.Quotients]
equiv_class_in_quotient [in ZornsLemma.Quotients]
eq_cardinal_impl_le_cardinal [in ZornsLemma.Cardinals]
eq_cardinal_equiv [in ZornsLemma.Cardinals]
eq_fn_equiv [in ZornsLemma.Quotients]
even_odd_excl2 [in ZornsLemma.CSB]
even_odd_excl [in ZornsLemma.CSB]
exclusive_dec [in ZornsLemma.DecidableDec]
extend_strictly_partial_WO_correct [in ZornsLemma.WellOrders]

F

FiniteT_impl_CountableT [in ZornsLemma.CountableTypes]
FiniteT_nat_cardinal_bijection [in ZornsLemma.FiniteTypes]
FiniteT_nat_cardinal_option [in ZornsLemma.FiniteTypes]
FiniteT_nat_cardinal_False [in ZornsLemma.FiniteTypes]
FiniteT_nat_cardinal_cond [in ZornsLemma.FiniteTypes]
FiniteT_nat_cardinal_def [in ZornsLemma.FiniteTypes]
FiniteT_has_nat_cardinal [in ZornsLemma.FiniteTypes]
FiniteT_img [in ZornsLemma.FiniteTypes]
Finite_impl_Countable [in ZornsLemma.CountableTypes]
finite_exp [in ZornsLemma.FiniteTypes]
finite_prod [in ZornsLemma.FiniteTypes]
finite_sum [in ZornsLemma.FiniteTypes]
finite_surj_inj [in ZornsLemma.FiniteTypes]
finite_inj_surj [in ZornsLemma.FiniteTypes]
finite_subtype [in ZornsLemma.FiniteTypes]
Finite_ens_type [in ZornsLemma.FiniteTypes]
finite_choice [in ZornsLemma.FiniteTypes]
finite_dep_choice [in ZornsLemma.FiniteTypes]
finite_eq_dec [in ZornsLemma.FiniteTypes]
finite_dec_forall [in ZornsLemma.FiniteTypes]
finite_dec_exists [in ZornsLemma.FiniteTypes]
finite_nat_initial_segment [in ZornsLemma.InfiniteTypes]
finite_indexed_intersection_is_finite_intersection [in ZornsLemma.FiniteIntersections]
finite_intersection_is_finite_indexed_intersection [in ZornsLemma.FiniteIntersections]

I

indexed_to_family_intersection [in ZornsLemma.IndexedFamilies]
indexed_to_family_union [in ZornsLemma.IndexedFamilies]
induced_function3_correct [in ZornsLemma.Quotients]
induced_function2arg_correct [in ZornsLemma.Quotients]
induced_function2_correct [in ZornsLemma.Quotients]
induced_function_unique [in ZornsLemma.Quotients]
induced_function_correct [in ZornsLemma.Quotients]
infinite_nat_inj [in ZornsLemma.InfiniteTypes]
injection_preserves_cardinal [in ZornsLemma.FiniteTypes]
inj_countable [in ZornsLemma.CountableTypes]
inj_finite [in ZornsLemma.FiniteTypes]
inverse_image_composition [in ZornsLemma.InverseImage]
inverse_image_complement [in ZornsLemma.InverseImage]
inverse_image_union [in ZornsLemma.InverseImage]
inverse_image_intersection [in ZornsLemma.InverseImage]
inverse_image_full [in ZornsLemma.InverseImage]
inverse_image_empty [in ZornsLemma.InverseImage]
inverse_image_increasing [in ZornsLemma.InverseImage]
invertible_impl_bijective [in ZornsLemma.FunctionProperties]

L

le_cardinal_total [in ZornsLemma.Cardinals]
le_cardinal_antisym [in ZornsLemma.Cardinals]
le_cardinal_preorder [in ZornsLemma.Cardinals]

M

MEP_implies_WF [in ZornsLemma.Classical_Wf]

N

nat_infinite [in ZornsLemma.InfiniteTypes]

O

ordinals_well_founded [in ZornsLemma.Ordinals]
ord_successor_or_limit [in ZornsLemma.Ordinals]
ord_lt_irrefl [in ZornsLemma.Ordinals]
ord_total_order [in ZornsLemma.Ordinals]
ord_lt_respects_succ [in ZornsLemma.Ordinals]
ord_lt_trans [in ZornsLemma.Ordinals]
ord_le_lt_trans [in ZornsLemma.Ordinals]
ord_lt_le_trans [in ZornsLemma.Ordinals]
ord_lt_le [in ZornsLemma.Ordinals]
ord_le_S [in ZornsLemma.Ordinals]
ord_le_refl [in ZornsLemma.Ordinals]
ord_le_sup [in ZornsLemma.Ordinals]
ord_le_trans [in ZornsLemma.Ordinals]
ord_sup_minimal_converse [in ZornsLemma.Ordinals]
ord_le_S_sup_converse [in ZornsLemma.Ordinals]
ord_le_respects_succ_converse [in ZornsLemma.Ordinals]

P

partial_WO_chain_ub_correct [in ZornsLemma.WellOrders]
partial_WO_preord [in ZornsLemma.WellOrders]
partial_injection_chain_ub [in ZornsLemma.Cardinals]
partial_injection_preord [in ZornsLemma.Cardinals]
positive_countable [in ZornsLemma.CountableTypes]
premaximal_partial_WO_is_full [in ZornsLemma.WellOrders]
premaximal_pi_is_full_or_surj [in ZornsLemma.Cardinals]
premaximal_partial_injection [in ZornsLemma.Cardinals]
projf_well_defined [in ZornsLemma.Quotients]
projf2_well_defined [in ZornsLemma.Quotients]
proj1_sig_injective [in ZornsLemma.Proj1SigInjective]
P_neq_not_P [in ZornsLemma.Cardinals]

Q

quotient_projection_minimally_collapses_R [in ZornsLemma.Quotients]
quotient_projection_collapses_R [in ZornsLemma.Quotients]
quotient_projection_surjective [in ZornsLemma.Quotients]
quotient_projection_correct [in ZornsLemma.Quotients]
Q_countable [in ZornsLemma.CountableTypes]

R

R_impl_equality_of_equiv_class [in ZornsLemma.Quotients]

S

slices_well_defined [in ZornsLemma.Quotients]
subfamily_intersection [in ZornsLemma.Families]
subfamily_union [in ZornsLemma.Families]
subset_eq_compatT [in ZornsLemma.Proj1SigInjective]
sub_indexed_intersection [in ZornsLemma.IndexedFamilies]
sub_indexed_union [in ZornsLemma.IndexedFamilies]
successor_ordinal_not_limit [in ZornsLemma.Ordinals]
surj_countable [in ZornsLemma.CountableTypes]
surj_finite [in ZornsLemma.FiniteTypes]
surj_le_cardinal [in ZornsLemma.Cardinals]

T

tower_is_chain [in ZornsLemma.ZornsLemma]
True_finite [in ZornsLemma.FiniteTypes]
types_comparable [in ZornsLemma.Cardinals]

U

unique_inverse [in ZornsLemma.FunctionProperties]
unique_FiniteT_nat_cardinal [in ZornsLemma.FiniteTypes]

W

well_orderable [in ZornsLemma.WellOrders]
well_defined_eval [in ZornsLemma.Quotients]
well_defined_induced1 [in ZornsLemma.Quotients]
WF_implies_DSP [in ZornsLemma.Classical_Wf]
WF_implies_MEP [in ZornsLemma.Classical_Wf]
WO_implies_AC [in ZornsLemma.WellOrders]
wo_transitive [in ZornsLemma.WellOrders]
wo_antisym [in ZornsLemma.WellOrders]
wo_irrefl [in ZornsLemma.WellOrders]

Z

ZL' [in ZornsLemma.ZornsLemma]
ZornsLemma [in ZornsLemma.ZornsLemma]
ZornsLemmaForPreorders [in ZornsLemma.ZornsLemma]
Z_countable [in ZornsLemma.CountableTypes]

Constructor Index

A

add_finite [in ZornsLemma.FiniteTypes]

B

bij_finite [in ZornsLemma.FiniteTypes]
bij_eq_cardinal [in ZornsLemma.Cardinals]

C

cardinality [in ZornsLemma.Cardinals]

E

empty_finite [in ZornsLemma.FiniteTypes]

F

family_intersection_intro [in ZornsLemma.Families]
family_union_intro [in ZornsLemma.Families]
f_X_odd [in ZornsLemma.CSB]
f_X_even [in ZornsLemma.CSB]

G

g_Y_even [in ZornsLemma.CSB]
g_Y_odd [in ZornsLemma.CSB]

I

indexed_intersection_intro [in ZornsLemma.IndexedFamilies]
indexed_union_intro [in ZornsLemma.IndexedFamilies]
inflation_intro [in ZornsLemma.ZornsLemma]
inj_le_cardinal [in ZornsLemma.Cardinals]
intro_invertible [in ZornsLemma.FunctionProperties]
intro_nat_injection [in ZornsLemma.CountableTypes]
intro_intersection [in ZornsLemma.FiniteIntersections]
intro_S [in ZornsLemma.FiniteIntersections]
intro_full [in ZornsLemma.FiniteIntersections]
intro_characteristic_sat [in ZornsLemma.EnsemblesSpec]
intro_limit_ord [in ZornsLemma.Ordinals]
intro_succ_ord [in ZornsLemma.Ordinals]

L

limit_ord_wd [in ZornsLemma.Ordinals]

N

not_f_img [in ZornsLemma.CSB]
not_g_img [in ZornsLemma.CSB]

O

ordS [in ZornsLemma.Ordinals]
ord_sup_minimal [in ZornsLemma.Ordinals]
ord_le_S_sup [in ZornsLemma.Ordinals]
ord_le_respects_succ [in ZornsLemma.Ordinals]
ord_sup [in ZornsLemma.Ordinals]

S

succ_ord_wd [in ZornsLemma.Ordinals]
sup_intro [in ZornsLemma.ZornsLemma]

Inductive Index

C

Cardinal [in ZornsLemma.Cardinals]
characteristic_function_abstraction [in ZornsLemma.EnsemblesSpec]
CountableT [in ZornsLemma.CountableTypes]

E

eq_cardinal [in ZornsLemma.Cardinals]

F

FamilyIntersection [in ZornsLemma.Families]
FamilyUnion [in ZornsLemma.Families]
FiniteT [in ZornsLemma.FiniteTypes]
finite_intersections [in ZornsLemma.FiniteIntersections]

I

IndexedIntersection [in ZornsLemma.IndexedFamilies]
IndexedUnion [in ZornsLemma.IndexedFamilies]
invertible [in ZornsLemma.FunctionProperties]

L

le_cardinal [in ZornsLemma.Cardinals]
limit_ordinal [in ZornsLemma.Ordinals]

O

Ordinal [in ZornsLemma.Ordinals]
ord_le [in ZornsLemma.Ordinals]

S

successor_ordinal [in ZornsLemma.Ordinals]

T

tower [in ZornsLemma.ZornsLemma]

X

X_odd [in ZornsLemma.CSB]
X_even [in ZornsLemma.CSB]

Y

Y_even [in ZornsLemma.CSB]
Y_odd [in ZornsLemma.CSB]

Projection Index

P

pi_func_ext [in ZornsLemma.Cardinals]
pi_dom_inc [in ZornsLemma.Cardinals]
pi_inj [in ZornsLemma.Cardinals]
pi_func [in ZornsLemma.Cardinals]
pi_dom [in ZornsLemma.Cardinals]
pwo_downward_closed [in ZornsLemma.WellOrders]
pwo_restriction [in ZornsLemma.WellOrders]
pwo_S_incl [in ZornsLemma.WellOrders]
pwo_wo [in ZornsLemma.WellOrders]
pwo_R_lives_on_S [in ZornsLemma.WellOrders]
pwo_R [in ZornsLemma.WellOrders]
pwo_S [in ZornsLemma.WellOrders]

W

wo_total_strict_order [in ZornsLemma.WellOrders]
wo_well_founded [in ZornsLemma.WellOrders]

Section Index

C

CSB [in ZornsLemma.CSB]

D

DecreasingSequences [in ZornsLemma.Classical_Wf]

F

Families [in ZornsLemma.Families]
FamilyFacts [in ZornsLemma.Families]

I

IndexedFamilies [in ZornsLemma.IndexedFamilies]
IndexedFamilyFacts [in ZornsLemma.IndexedFamilies]
IndexedFamilyToFamily [in ZornsLemma.IndexedFamilies]
InducedFunction [in ZornsLemma.Quotients]
InducedFunction2 [in ZornsLemma.Quotients]
InducedFunction2arg [in ZornsLemma.Quotients]
InducedFunction3 [in ZornsLemma.Quotients]

L

le_cardinal_total [in ZornsLemma.Cardinals]

M

MinimalElements [in ZornsLemma.Classical_Wf]

Q

Quotient [in ZornsLemma.Quotients]

W

WellOrder [in ZornsLemma.WellOrders]
WellOrderConstruction [in ZornsLemma.WellOrders]
WellOrderMinimum [in ZornsLemma.WellOrders]
WO_implies_AC [in ZornsLemma.WellOrders]

Z

ZL [in ZornsLemma.ZornsLemma]
ZL_preorder [in ZornsLemma.ZornsLemma]
ZL' [in ZornsLemma.ZornsLemma]

Definition Index

A

aleph0 [in ZornsLemma.Cardinals]

B

bijective [in ZornsLemma.FunctionProperties]

C

chain [in ZornsLemma.ZornsLemma]
chains [in ZornsLemma.ZornsLemma]
chains_sup [in ZornsLemma.ZornsLemma]
chains_sup_def [in ZornsLemma.ZornsLemma]
chains_ord [in ZornsLemma.ZornsLemma]
characteristic_function_to_ensemble [in ZornsLemma.EnsemblesSpec]
Countable [in ZornsLemma.CountableTypes]
CSB_bijection2 [in ZornsLemma.CSB]
CSB_bijection [in ZornsLemma.CSB]

D

decreasing_sequence_property [in ZornsLemma.Classical_Wf]

E

equiv_classes [in ZornsLemma.Quotients]
equiv_class [in ZornsLemma.Quotients]
eq_fn [in ZornsLemma.Quotients]
eval [in ZornsLemma.Quotients]
extend_strictly_partial_WO [in ZornsLemma.WellOrders]

F

Family [in ZornsLemma.Families]
FiniteT_nat_cardinal [in ZornsLemma.FiniteTypes]
finv [in ZornsLemma.CSB]
finv_noteven [in ZornsLemma.CSB]
function_inverse [in ZornsLemma.FunctionProperties]

G

ge_cardinal [in ZornsLemma.Cardinals]
ginv [in ZornsLemma.CSB]
ginv_odd [in ZornsLemma.CSB]
gt_cardinal [in ZornsLemma.Cardinals]

I

ImageFamily [in ZornsLemma.IndexedFamilies]
IndexedFamily [in ZornsLemma.IndexedFamilies]
induced_function3 [in ZornsLemma.Quotients]
induced_function2arg [in ZornsLemma.Quotients]
induced_eval [in ZornsLemma.Quotients]
induced_function2 [in ZornsLemma.Quotients]
induced_function [in ZornsLemma.Quotients]
induced1 [in ZornsLemma.Quotients]
induced2 [in ZornsLemma.Quotients]
injective [in ZornsLemma.FunctionProperties]
inverse_image [in ZornsLemma.InverseImage]

L

lt_cardinal [in ZornsLemma.Cardinals]

M

maximal [in ZornsLemma.ZornsLemma]
minimal_element_property [in ZornsLemma.Classical_Wf]

N

nat_to_cardinal [in ZornsLemma.Cardinals]
n_element_set [in ZornsLemma.Cardinals]

O

ord_gt [in ZornsLemma.Ordinals]
ord_ge [in ZornsLemma.Ordinals]
ord_eq [in ZornsLemma.Ordinals]
ord_lt [in ZornsLemma.Ordinals]

P

partial_WO_chain_ub [in ZornsLemma.WellOrders]
premaximal [in ZornsLemma.ZornsLemma]
projf [in ZornsLemma.Quotients]
projf2 [in ZornsLemma.Quotients]

Q

quotient [in ZornsLemma.Quotients]
quotient_projection [in ZornsLemma.Quotients]

R

restriction_relation [in ZornsLemma.WellOrders]

S

surjective [in ZornsLemma.FunctionProperties]

T

total_strict_order [in ZornsLemma.WellOrders]

W

WO_minimum [in ZornsLemma.WellOrders]

X

X_odd_coind [in ZornsLemma.CSB]
X_even_coind [in ZornsLemma.CSB]

Y

Y_even_coind [in ZornsLemma.CSB]
Y_odd_coind [in ZornsLemma.CSB]

Record Index

P

partial_WO_ord [in ZornsLemma.WellOrders]
partial_WO [in ZornsLemma.WellOrders]
partial_injection_ord [in ZornsLemma.Cardinals]
partial_injection [in ZornsLemma.Cardinals]

W

well_order [in ZornsLemma.WellOrders]

Global Index

H

J

K

V

_

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

_

(27 entries)

Variable Index

A

B

E

G

H

J

K

N

O

P

R

S

T

U

V

X

Y

_

other

(76 entries)

Library Index

A

B

G

H

J

K

L

M

N

S

T

U

V

X

Y

_

other

(23 entries)

Lemma Index

A

G

H

J

K

V

X

Y

_

other

(147 entries)

Constructor Index

D

H

J

K

M

P

Q

R

T

U

V

W

X

Y

Z

_

other

(33 entries)

Inductive Index

A

B

D

G

H

J

K

M

N

P

Q

R

U

V

W

Z

_

other

(21 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

Q

R

S

T

U

V

X

Y

Z

_

other

(14 entries)

Section Index

A

B

E

G

H

J

K

N

O

P

R

S

T

U

V

X

Y

_

other

(21 entries)

Definition Index

H

J

K

U

V

Z

_

other

(60 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

Q

R

S

T

U

V

X

Y

Z

_

other

(5 entries)