| 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 | (323 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 | (32 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| 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 | (112 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 | (14 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 | (12 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 | (20 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 | (4 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 | (26 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 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 | (84 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 | (9 entries) |
Global Index
A
adjunction [definition, in Continuum.Basic_Set_Theory]All [definition, in Continuum.Basic_Set_Theory]
Any [definition, in Continuum.Basic_Set_Theory]
Axiom_Of_Choice [definition, in Continuum.Sierpinskis_Theorem]
Axiom_Of_Choice' [definition, in Continuum.Sierpinskis_Theorem]
B
Basic_Set_Theory [library]big_union [axiom, in Continuum.Basic_Set_Theory]
big_union_is_ordinal [constructor, in Continuum.Ordinals]
Bijection [record, in Continuum.Cardinality]
bijection_subrelation_flipped_injection [instance, in Continuum.Cardinality]
bijection_subrelation_injection [instance, in Continuum.Cardinality]
bijection_is_injective [lemma, in Continuum.Cardinality]
bijection_relation_transitivity [lemma, in Continuum.Cardinality]
bijection_relation_symmetry [lemma, in Continuum.Cardinality]
bijection_relation_reflexivity [lemma, in Continuum.Cardinality]
bijection_relation_on_Set [definition, in Continuum.Cardinality]
bijection_relation [definition, in Continuum.Cardinality]
bijection_left_right [projection, in Continuum.Cardinality]
bijection_right_left [projection, in Continuum.Cardinality]
bijection_to_left [projection, in Continuum.Cardinality]
bijection_to_right [projection, in Continuum.Cardinality]
build_is_unique_solution [constructor, in Continuum.Basic_Set_Theory]
build_element [constructor, in Continuum.Basic_Set_Theory]
build_class [constructor, in Continuum.Basic_Set_Theory]
build_surjection [constructor, in Continuum.Cardinality]
build_injection [constructor, in Continuum.Cardinality]
build_bijection [constructor, in Continuum.Cardinality]
build_well_order [constructor, in Continuum.Ordinals]
C
cancel_inverse_left [lemma, in Continuum.Cardinality]cancel_inverse_right [lemma, in Continuum.Cardinality]
cantors_theorem [lemma, in Continuum.Cardinality]
Cardinality [library]
cartesian_product_upper_bound [lemma, in Continuum.Basic_Set_Theory]
cartesian_product_eta [lemma, in Continuum.Basic_Set_Theory]
cartesian_product [definition, in Continuum.Basic_Set_Theory]
Class [record, in Continuum.Basic_Set_Theory]
class_of_all_sets [definition, in Continuum.Basic_Set_Theory]
class_as_set_equiv_set [lemma, in Continuum.Cardinality]
class_as_set [definition, in Continuum.Cardinality]
compose_injections [definition, in Continuum.Cardinality]
compose_bijections [definition, in Continuum.Cardinality]
compose_isos [definition, in Continuum.Ordinals]
comprehension [definition, in Continuum.Basic_Set_Theory]
comprehension_condition [lemma, in Continuum.Basic_Set_Theory]
conditional_fun_replacement [definition, in Continuum.Basic_Set_Theory]
D
decode [definition, in Continuum.Ordinals]decode_encode [lemma, in Continuum.Ordinals]
description [definition, in Continuum.Basic_Set_Theory]
Description [section, in Continuum.Basic_Set_Theory]
description_is_solution [lemma, in Continuum.Basic_Set_Theory]
description_is_unique [instance, in Continuum.Basic_Set_Theory]
difference [definition, in Continuum.Basic_Set_Theory]
Disjoint [definition, in Continuum.Cardinality]
disjoint_union_ind [definition, in Continuum.Basic_Set_Theory]
disjoint_union_iter_reduction_right [lemma, in Continuum.Basic_Set_Theory]
disjoint_union_iter_reduction_left [lemma, in Continuum.Basic_Set_Theory]
disjoint_union_iter_property [lemma, in Continuum.Basic_Set_Theory]
disjoint_union_iter [definition, in Continuum.Basic_Set_Theory]
Disjoint_Union_Iter_Property [definition, in Continuum.Basic_Set_Theory]
disjoint_union [definition, in Continuum.Basic_Set_Theory]
disjoint_union_is_increasing_on_right [lemma, in Continuum.Cardinality]
disjoint_union_is_increasing_on_left [lemma, in Continuum.Cardinality]
disjoint_union_associative [lemma, in Continuum.Cardinality]
double_induction [lemma, in Continuum.Ordinals]
E
element [abbreviation, in Continuum.Basic_Set_Theory]element_of_tail_is_element_of_adjunction [instance, in Continuum.Basic_Set_Theory]
element_stays_element [instance, in Continuum.Basic_Set_Theory]
element_equality [lemma, in Continuum.Basic_Set_Theory]
element_property [projection, in Continuum.Basic_Set_Theory]
element_value [projection, in Continuum.Basic_Set_Theory]
Element_Of [record, in Continuum.Basic_Set_Theory]
element_predicate [projection, in Continuum.Basic_Set_Theory]
element_of_ordinal_is_ordinal [instance, in Continuum.Ordinals]
element_of_ordinal_is_subset [lemma, in Continuum.Ordinals]
empty_set_ind [lemma, in Continuum.Basic_Set_Theory]
empty_set [axiom, in Continuum.Basic_Set_Theory]
encode [definition, in Continuum.Ordinals]
encodings [definition, in Continuum.Ordinals]
exists_element_of_explicit_set_iff [lemma, in Continuum.Basic_Set_Theory]
explicit_set_equals_explicit_set_iff [lemma, in Continuum.Basic_Set_Theory]
explicit_set_is_subset_of_explicit_set_iff [lemma, in Continuum.Basic_Set_Theory]
explicit_set [definition, in Continuum.Basic_Set_Theory]
extensionality [axiom, in Continuum.Basic_Set_Theory]
extract_from_right_is_injective [lemma, in Continuum.Basic_Set_Theory]
extract_from_right [definition, in Continuum.Basic_Set_Theory]
extract_from_left [definition, in Continuum.Basic_Set_Theory]
F
forall_elements_of_explicit_set_iff [lemma, in Continuum.Basic_Set_Theory]from_left_or_right [lemma, in Continuum.Basic_Set_Theory]
Functional [record, in Continuum.Basic_Set_Theory]
Functional [inductive, in Continuum.Basic_Set_Theory]
functionality [projection, in Continuum.Basic_Set_Theory]
functionality [constructor, in Continuum.Basic_Set_Theory]
function_compose_inverse [lemma, in Continuum.Cardinality]
fun_replacement_in_power_set [instance, in Continuum.Basic_Set_Theory]
fun_replacement [definition, in Continuum.Basic_Set_Theory]
G
Generalized_Continuum_Hypothesis [definition, in Continuum.Sierpinskis_Theorem]Greater [definition, in Continuum.Ordinals]
H
hartogs_number_has_upper_bound [lemma, in Continuum.Hartogs_Number]hartogs_number_is_not_smaller [lemma, in Continuum.Hartogs_Number]
hartogs_number [definition, in Continuum.Hartogs_Number]
hartogs_number_as_class_is_a_set [lemma, in Continuum.Hartogs_Number]
hartogs_number_as_class_has_upper_bound [lemma, in Continuum.Hartogs_Number]
hartogs_number_as_class [definition, in Continuum.Hartogs_Number]
Hartogs_Number [library]
head_is_element_of_adjunction [instance, in Continuum.Basic_Set_Theory]
I
id_injection [definition, in Continuum.Cardinality]id_bijection [definition, in Continuum.Cardinality]
image_of [definition, in Continuum.Basic_Set_Theory]
image_under_id [lemma, in Continuum.Basic_Set_Theory]
image_of_image [lemma, in Continuum.Basic_Set_Theory]
image_under [definition, in Continuum.Basic_Set_Theory]
image_of_injection_is_equipotent [lemma, in Continuum.Cardinality]
indexed_intersection [definition, in Continuum.Basic_Set_Theory]
indexed_union [definition, in Continuum.Basic_Set_Theory]
Infinite [definition, in Continuum.Sierpinskis_Theorem]
Injection [record, in Continuum.Cardinality]
injection_relation_transitivity [lemma, in Continuum.Cardinality]
injection_relation_reflexivity [lemma, in Continuum.Cardinality]
injection_relation_on_Set [definition, in Continuum.Cardinality]
injection_relation [definition, in Continuum.Cardinality]
injection_as_bijection_into_image [definition, in Continuum.Cardinality]
injection_property [projection, in Continuum.Cardinality]
injection_fun [projection, in Continuum.Cardinality]
inj1 [definition, in Continuum.Basic_Set_Theory]
inj1_extract_from_left [lemma, in Continuum.Basic_Set_Theory]
inj1_and_inj2_are_disjoint [lemma, in Continuum.Basic_Set_Theory]
inj1_is_injective [lemma, in Continuum.Basic_Set_Theory]
inj2 [definition, in Continuum.Basic_Set_Theory]
inj2_is_injective [lemma, in Continuum.Basic_Set_Theory]
intersection [definition, in Continuum.Basic_Set_Theory]
inverse_compose_function [lemma, in Continuum.Cardinality]
inverse_bijection [definition, in Continuum.Cardinality]
in_Numeral_iff [lemma, in Continuum.Basic_Set_Theory]
in_Numeral_iff' [axiom, in Continuum.Basic_Set_Theory]
in_difference_iff [lemma, in Continuum.Basic_Set_Theory]
in_intersection_iff [lemma, in Continuum.Basic_Set_Theory]
in_indexed_intersection_iff [lemma, in Continuum.Basic_Set_Theory]
in_indexed_union [instance, in Continuum.Basic_Set_Theory]
in_indexed_union_iff [lemma, in Continuum.Basic_Set_Theory]
in_explicit_set_iff [lemma, in Continuum.Basic_Set_Theory]
in_adjunction_iff [lemma, in Continuum.Basic_Set_Theory]
in_union_intro_right [instance, in Continuum.Basic_Set_Theory]
in_union_intro_left [instance, in Continuum.Basic_Set_Theory]
in_union_intro2 [instance, in Continuum.Basic_Set_Theory]
in_union_intro1 [instance, in Continuum.Basic_Set_Theory]
in_union_iff [lemma, in Continuum.Basic_Set_Theory]
in_provisional_singleton [lemma, in Continuum.Basic_Set_Theory]
in_provisional_unordered_pair_iff [lemma, in Continuum.Basic_Set_Theory]
in_comprehension_iff_typed [lemma, in Continuum.Basic_Set_Theory]
in_comprehension_iff [lemma, in Continuum.Basic_Set_Theory]
in_conditional_fun_replacement_iff [lemma, in Continuum.Basic_Set_Theory]
in_image_of [instance, in Continuum.Basic_Set_Theory]
in_image_under [instance, in Continuum.Basic_Set_Theory]
in_image_iff [lemma, in Continuum.Basic_Set_Theory]
in_fun_replacement_iff [lemma, in Continuum.Basic_Set_Theory]
in_replacement_iff [axiom, in Continuum.Basic_Set_Theory]
in_set_if_in_subset [instance, in Continuum.Basic_Set_Theory]
in_power_set_iff [axiom, in Continuum.Basic_Set_Theory]
in_big_union_iff [axiom, in Continuum.Basic_Set_Theory]
in_empty_set_iff [axiom, in Continuum.Basic_Set_Theory]
in_class_of_all_sets [instance, in Continuum.Basic_Set_Theory]
in_class [projection, in Continuum.Basic_Set_Theory]
In_Class [record, in Continuum.Basic_Set_Theory]
in_class [constructor, in Continuum.Basic_Set_Theory]
In_Class [inductive, in Continuum.Basic_Set_Theory]
In_Set [axiom, in Continuum.Basic_Set_Theory]
in_class_as_set_iff [lemma, in Continuum.Cardinality]
in_successor_iff [lemma, in Continuum.Ordinals]
isomorphic_ordinals_are_equal [lemma, in Continuum.Ordinals]
Isomorphism [definition, in Continuum.Ordinals]
isomorphism_from_ordinal_to_element_is_non_decreasing [lemma, in Continuum.Ordinals]
isomorphism_relation_symmetry [lemma, in Continuum.Ordinals]
isomorphism_relation_transitivity [lemma, in Continuum.Ordinals]
isomorphism_relation_reflexivity [lemma, in Continuum.Ordinals]
isomorphism_relation [definition, in Continuum.Ordinals]
isomorphism_inverse [definition, in Continuum.Ordinals]
isomorphism_preserves_relation [lemma, in Continuum.Ordinals]
Is_From_Right [definition, in Continuum.Basic_Set_Theory]
Is_From_Left [definition, in Continuum.Basic_Set_Theory]
Is_Unique_Solution_Of [record, in Continuum.Basic_Set_Theory]
Is_Well_Founded [definition, in Continuum.Basic_Set_Theory]
is_accessible_intro [constructor, in Continuum.Basic_Set_Theory]
Is_Accessible_By [inductive, in Continuum.Basic_Set_Theory]
Is_Subset_Of [definition, in Continuum.Basic_Set_Theory]
Is_A_Set [definition, in Continuum.Cardinality]
Is_Surjective [definition, in Continuum.Cardinality]
Is_Transitive_Set [definition, in Continuum.Ordinals]
Is_Ordinal [inductive, in Continuum.Ordinals]
Is_Linear_Relation [definition, in Continuum.Ordinals]
L
least_element [definition, in Continuum.Ordinals]left_projection_beta [lemma, in Continuum.Basic_Set_Theory]
left_projection [definition, in Continuum.Basic_Set_Theory]
lemma1 [lemma, in Continuum.Sierpinskis_Theorem]
lemma2 [lemma, in Continuum.Sierpinskis_Theorem]
Less [definition, in Continuum.Ordinals]
Less_Or_Equal [definition, in Continuum.Cardinality]
linearity [lemma, in Continuum.Ordinals]
N
nat_to_numeral_is_injective [lemma, in Continuum.Basic_Set_Theory]nat_to_numeral_is_monotone [lemma, in Continuum.Basic_Set_Theory]
nat_to_numeral_is_nat_to_numeral' [lemma, in Continuum.Basic_Set_Theory]
nat_to_numeral [definition, in Continuum.Basic_Set_Theory]
nat_to_numeral' [definition, in Continuum.Basic_Set_Theory]
not_gt_implies_leq [lemma, in Continuum.Ordinals]
no_set_equals_its_power_set [lemma, in Continuum.Basic_Set_Theory]
no_set_contains_itself [lemma, in Continuum.Basic_Set_Theory]
Numeral [axiom, in Continuum.Basic_Set_Theory]
Numeral_iter_reduction_S [lemma, in Continuum.Basic_Set_Theory]
Numeral_iter_reduction_O [lemma, in Continuum.Basic_Set_Theory]
Numeral_iter_property [lemma, in Continuum.Basic_Set_Theory]
Numeral_iter [definition, in Continuum.Basic_Set_Theory]
Numeral_iter_Property [definition, in Continuum.Basic_Set_Theory]
Numeral_ind [definition, in Continuum.Basic_Set_Theory]
numeral_S [definition, in Continuum.Basic_Set_Theory]
numeral_O [definition, in Continuum.Basic_Set_Theory]
Numeral_equipotent_Numeral_plus_one [lemma, in Continuum.Cardinality]
O
one_ind [lemma, in Continuum.Basic_Set_Theory]Ordinal [definition, in Continuum.Ordinals]
Ordinals [library]
ordinal_is_not_isomorphic_to_element [lemma, in Continuum.Ordinals]
ordinal_order [definition, in Continuum.Ordinals]
ordinal_linearity [lemma, in Continuum.Ordinals]
ordinal_order_transitivity [lemma, in Continuum.Ordinals]
ordinal_order_irreflexivity [lemma, in Continuum.Ordinals]
ordinal_order_relation [abbreviation, in Continuum.Ordinals]
ordinal_is_in_Ordinal [instance, in Continuum.Ordinals]
ordinal_is_ordinal [instance, in Continuum.Ordinals]
P
pair [definition, in Continuum.Basic_Set_Theory]pair_is_injective_left [lemma, in Continuum.Basic_Set_Theory]
pair_is_injective_right [lemma, in Continuum.Basic_Set_Theory]
power_set [axiom, in Continuum.Basic_Set_Theory]
power_set_equiv_power_set_plus_power_set [lemma, in Continuum.Cardinality]
power_set_of_disjoint_union [lemma, in Continuum.Cardinality]
power_set_is_increasing [lemma, in Continuum.Cardinality]
Preserves_Relation [definition, in Continuum.Ordinals]
provisional_singleton [definition, in Continuum.Basic_Set_Theory]
provisional_unordered_pair [definition, in Continuum.Basic_Set_Theory]
R
reflexive_closure_is_partial_order [instance, in Continuum.Ordinals]reflexive_closure_is_pre_order [instance, in Continuum.Ordinals]
reflexive_closure [definition, in Continuum.Ordinals]
replacement [axiom, in Continuum.Basic_Set_Theory]
restrict_well_order [definition, in Continuum.Ordinals]
right_projection_beta [lemma, in Continuum.Basic_Set_Theory]
right_projection [definition, in Continuum.Basic_Set_Theory]
S
S [abbreviation, in Continuum.Basic_Set_Theory]sets_are_well_founded [axiom, in Continuum.Basic_Set_Theory]
set_in_power_set [instance, in Continuum.Basic_Set_Theory]
Set_ [axiom, in Continuum.Basic_Set_Theory]
set_equipotent_set_plus_one [lemma, in Continuum.Cardinality]
set_equipotent_subset_plus_difference [lemma, in Continuum.Cardinality]
set_equals_subset_union_difference [lemma, in Continuum.Cardinality]
sierpinskis_theorem [lemma, in Continuum.Sierpinskis_Theorem]
Sierpinskis_Theorem [library]
small_class_is_a_set [lemma, in Continuum.Cardinality]
solutions [definition, in Continuum.Basic_Set_Theory]
strip_element [lemma, in Continuum.Basic_Set_Theory]
subset_extensionality [lemma, in Continuum.Basic_Set_Theory]
subset_relation_transitivity [instance, in Continuum.Basic_Set_Theory]
subset_relation_reflexivity [instance, in Continuum.Basic_Set_Theory]
subset_subrelation_injection [instance, in Continuum.Cardinality]
successor_linearity [lemma, in Continuum.Ordinals]
successor_is_ordinal [constructor, in Continuum.Ordinals]
Surjection [record, in Continuum.Cardinality]
surjection_is_surjective [projection, in Continuum.Cardinality]
surjection_fun [projection, in Continuum.Cardinality]
symmetric_cartesian_product_is_increasing [lemma, in Continuum.Cardinality]
T
transitive_set_of_ordinals_is_ordinal [lemma, in Continuum.Ordinals]transported_relation_is_isomorphic [lemma, in Continuum.Ordinals]
transport_well_order [definition, in Continuum.Ordinals]
transport_relation [definition, in Continuum.Ordinals]
two_times_set_is_disjoin_union [lemma, in Continuum.Basic_Set_Theory]
two_is_power_set_of_one [lemma, in Continuum.Cardinality]
U
union [definition, in Continuum.Basic_Set_Theory]union_of_disjoints_equipotent_disjoint_union [lemma, in Continuum.Cardinality]
unique_solution_is_unique [projection, in Continuum.Basic_Set_Theory]
unique_solution_is_solution [projection, in Continuum.Basic_Set_Theory]
unordered_pair_equals_unordered_pair_iff [lemma, in Continuum.Basic_Set_Theory]
untyped_pair_is_injective_right [lemma, in Continuum.Basic_Set_Theory]
untyped_pair_is_injective_left [lemma, in Continuum.Basic_Set_Theory]
untyped_pair [definition, in Continuum.Basic_Set_Theory]
W
well_founded_induction [lemma, in Continuum.Basic_Set_Theory]well_order_has_least_elements [lemma, in Continuum.Ordinals]
well_order_is_strict_order [instance, in Continuum.Ordinals]
well_order_is_well_founded [projection, in Continuum.Ordinals]
well_order_is_linear [projection, in Continuum.Ordinals]
well_order_is_irreflexive [projection, in Continuum.Ordinals]
well_order_is_transitive [projection, in Continuum.Ordinals]
well_order_relation [projection, in Continuum.Ordinals]
Well_Order_On [record, in Continuum.Ordinals]
Well_Ordering_to_Choice [lemma, in Continuum.Sierpinskis_Theorem]
Well_Ordering_Theorem [definition, in Continuum.Sierpinskis_Theorem]
other
_ ⊔ _ [notation, in Continuum.Basic_Set_Theory]_ × _ [notation, in Continuum.Basic_Set_Theory]
_ \ _ [notation, in Continuum.Basic_Set_Theory]
_ ∩ _ [notation, in Continuum.Basic_Set_Theory]
_ @ _ [notation, in Continuum.Basic_Set_Theory]
_ ∪ _ [notation, in Continuum.Basic_Set_Theory]
_ '' _ [notation, in Continuum.Basic_Set_Theory]
_ ⊆ _ [notation, in Continuum.Basic_Set_Theory]
_ ∉ _ [notation, in Continuum.Basic_Set_Theory]
_ ∈ _ [notation, in Continuum.Basic_Set_Theory]
_ ↠ _ [notation, in Continuum.Cardinality]
_ ↪ _ [notation, in Continuum.Cardinality]
_ ∼ _ [notation, in Continuum.Cardinality]
_ ⁻¹ [notation, in Continuum.Cardinality]
_ <= _ <= _ [notation, in Continuum.Cardinality]
_ <= _ [notation, in Continuum.Cardinality]
_ ≃ _ [notation, in Continuum.Ordinals]
_ > _ [notation, in Continuum.Ordinals]
_ < _ [notation, in Continuum.Ordinals]
`( _ , _ ) [notation, in Continuum.Basic_Set_Theory]
`{ _ , .. , _ } [notation, in Continuum.Basic_Set_Theory]
`{ } [notation, in Continuum.Basic_Set_Theory]
`{ _ in _ | _ } [notation, in Continuum.Basic_Set_Theory]
`{ _ | _ in _ , _ } [notation, in Continuum.Basic_Set_Theory]
`{ _ | _ in _ } [notation, in Continuum.Basic_Set_Theory]
∅ [notation, in Continuum.Basic_Set_Theory]
⋂ _ ∈ _ , _ [notation, in Continuum.Basic_Set_Theory]
⋃ _ ∈ _ , _ [notation, in Continuum.Basic_Set_Theory]
δ _ : _ , _ [notation, in Continuum.Basic_Set_Theory]
π1 [notation, in Continuum.Basic_Set_Theory]
π2 [notation, in Continuum.Basic_Set_Theory]
𝒫 [notation, in Continuum.Basic_Set_Theory]
σ [abbreviation, in Continuum.Basic_Set_Theory]
Notation Index
other
_ ⊔ _ [in Continuum.Basic_Set_Theory]_ × _ [in Continuum.Basic_Set_Theory]
_ \ _ [in Continuum.Basic_Set_Theory]
_ ∩ _ [in Continuum.Basic_Set_Theory]
_ @ _ [in Continuum.Basic_Set_Theory]
_ ∪ _ [in Continuum.Basic_Set_Theory]
_ '' _ [in Continuum.Basic_Set_Theory]
_ ⊆ _ [in Continuum.Basic_Set_Theory]
_ ∉ _ [in Continuum.Basic_Set_Theory]
_ ∈ _ [in Continuum.Basic_Set_Theory]
_ ↠ _ [in Continuum.Cardinality]
_ ↪ _ [in Continuum.Cardinality]
_ ∼ _ [in Continuum.Cardinality]
_ ⁻¹ [in Continuum.Cardinality]
_ <= _ <= _ [in Continuum.Cardinality]
_ <= _ [in Continuum.Cardinality]
_ ≃ _ [in Continuum.Ordinals]
_ > _ [in Continuum.Ordinals]
_ < _ [in Continuum.Ordinals]
`( _ , _ ) [in Continuum.Basic_Set_Theory]
`{ _ , .. , _ } [in Continuum.Basic_Set_Theory]
`{ } [in Continuum.Basic_Set_Theory]
`{ _ in _ | _ } [in Continuum.Basic_Set_Theory]
`{ _ | _ in _ , _ } [in Continuum.Basic_Set_Theory]
`{ _ | _ in _ } [in Continuum.Basic_Set_Theory]
∅ [in Continuum.Basic_Set_Theory]
⋂ _ ∈ _ , _ [in Continuum.Basic_Set_Theory]
⋃ _ ∈ _ , _ [in Continuum.Basic_Set_Theory]
δ _ : _ , _ [in Continuum.Basic_Set_Theory]
π1 [in Continuum.Basic_Set_Theory]
π2 [in Continuum.Basic_Set_Theory]
𝒫 [in Continuum.Basic_Set_Theory]
Library Index
B
Basic_Set_TheoryC
CardinalityH
Hartogs_NumberO
OrdinalsS
Sierpinskis_TheoremLemma Index
B
bijection_is_injective [in Continuum.Cardinality]bijection_relation_transitivity [in Continuum.Cardinality]
bijection_relation_symmetry [in Continuum.Cardinality]
bijection_relation_reflexivity [in Continuum.Cardinality]
C
cancel_inverse_left [in Continuum.Cardinality]cancel_inverse_right [in Continuum.Cardinality]
cantors_theorem [in Continuum.Cardinality]
cartesian_product_upper_bound [in Continuum.Basic_Set_Theory]
cartesian_product_eta [in Continuum.Basic_Set_Theory]
class_as_set_equiv_set [in Continuum.Cardinality]
comprehension_condition [in Continuum.Basic_Set_Theory]
D
decode_encode [in Continuum.Ordinals]description_is_solution [in Continuum.Basic_Set_Theory]
disjoint_union_iter_reduction_right [in Continuum.Basic_Set_Theory]
disjoint_union_iter_reduction_left [in Continuum.Basic_Set_Theory]
disjoint_union_iter_property [in Continuum.Basic_Set_Theory]
disjoint_union_is_increasing_on_right [in Continuum.Cardinality]
disjoint_union_is_increasing_on_left [in Continuum.Cardinality]
disjoint_union_associative [in Continuum.Cardinality]
double_induction [in Continuum.Ordinals]
E
element_equality [in Continuum.Basic_Set_Theory]element_of_ordinal_is_subset [in Continuum.Ordinals]
empty_set_ind [in Continuum.Basic_Set_Theory]
exists_element_of_explicit_set_iff [in Continuum.Basic_Set_Theory]
explicit_set_equals_explicit_set_iff [in Continuum.Basic_Set_Theory]
explicit_set_is_subset_of_explicit_set_iff [in Continuum.Basic_Set_Theory]
extract_from_right_is_injective [in Continuum.Basic_Set_Theory]
F
forall_elements_of_explicit_set_iff [in Continuum.Basic_Set_Theory]from_left_or_right [in Continuum.Basic_Set_Theory]
function_compose_inverse [in Continuum.Cardinality]
H
hartogs_number_has_upper_bound [in Continuum.Hartogs_Number]hartogs_number_is_not_smaller [in Continuum.Hartogs_Number]
hartogs_number_as_class_is_a_set [in Continuum.Hartogs_Number]
hartogs_number_as_class_has_upper_bound [in Continuum.Hartogs_Number]
I
image_under_id [in Continuum.Basic_Set_Theory]image_of_image [in Continuum.Basic_Set_Theory]
image_of_injection_is_equipotent [in Continuum.Cardinality]
injection_relation_transitivity [in Continuum.Cardinality]
injection_relation_reflexivity [in Continuum.Cardinality]
inj1_extract_from_left [in Continuum.Basic_Set_Theory]
inj1_and_inj2_are_disjoint [in Continuum.Basic_Set_Theory]
inj1_is_injective [in Continuum.Basic_Set_Theory]
inj2_is_injective [in Continuum.Basic_Set_Theory]
inverse_compose_function [in Continuum.Cardinality]
in_Numeral_iff [in Continuum.Basic_Set_Theory]
in_difference_iff [in Continuum.Basic_Set_Theory]
in_intersection_iff [in Continuum.Basic_Set_Theory]
in_indexed_intersection_iff [in Continuum.Basic_Set_Theory]
in_indexed_union_iff [in Continuum.Basic_Set_Theory]
in_explicit_set_iff [in Continuum.Basic_Set_Theory]
in_adjunction_iff [in Continuum.Basic_Set_Theory]
in_union_iff [in Continuum.Basic_Set_Theory]
in_provisional_singleton [in Continuum.Basic_Set_Theory]
in_provisional_unordered_pair_iff [in Continuum.Basic_Set_Theory]
in_comprehension_iff_typed [in Continuum.Basic_Set_Theory]
in_comprehension_iff [in Continuum.Basic_Set_Theory]
in_conditional_fun_replacement_iff [in Continuum.Basic_Set_Theory]
in_image_iff [in Continuum.Basic_Set_Theory]
in_fun_replacement_iff [in Continuum.Basic_Set_Theory]
in_class_as_set_iff [in Continuum.Cardinality]
in_successor_iff [in Continuum.Ordinals]
isomorphic_ordinals_are_equal [in Continuum.Ordinals]
isomorphism_from_ordinal_to_element_is_non_decreasing [in Continuum.Ordinals]
isomorphism_relation_symmetry [in Continuum.Ordinals]
isomorphism_relation_transitivity [in Continuum.Ordinals]
isomorphism_relation_reflexivity [in Continuum.Ordinals]
isomorphism_preserves_relation [in Continuum.Ordinals]
L
left_projection_beta [in Continuum.Basic_Set_Theory]lemma1 [in Continuum.Sierpinskis_Theorem]
lemma2 [in Continuum.Sierpinskis_Theorem]
linearity [in Continuum.Ordinals]
N
nat_to_numeral_is_injective [in Continuum.Basic_Set_Theory]nat_to_numeral_is_monotone [in Continuum.Basic_Set_Theory]
nat_to_numeral_is_nat_to_numeral' [in Continuum.Basic_Set_Theory]
not_gt_implies_leq [in Continuum.Ordinals]
no_set_equals_its_power_set [in Continuum.Basic_Set_Theory]
no_set_contains_itself [in Continuum.Basic_Set_Theory]
Numeral_iter_reduction_S [in Continuum.Basic_Set_Theory]
Numeral_iter_reduction_O [in Continuum.Basic_Set_Theory]
Numeral_iter_property [in Continuum.Basic_Set_Theory]
Numeral_equipotent_Numeral_plus_one [in Continuum.Cardinality]
O
one_ind [in Continuum.Basic_Set_Theory]ordinal_is_not_isomorphic_to_element [in Continuum.Ordinals]
ordinal_linearity [in Continuum.Ordinals]
ordinal_order_transitivity [in Continuum.Ordinals]
ordinal_order_irreflexivity [in Continuum.Ordinals]
P
pair_is_injective_left [in Continuum.Basic_Set_Theory]pair_is_injective_right [in Continuum.Basic_Set_Theory]
power_set_equiv_power_set_plus_power_set [in Continuum.Cardinality]
power_set_of_disjoint_union [in Continuum.Cardinality]
power_set_is_increasing [in Continuum.Cardinality]
R
right_projection_beta [in Continuum.Basic_Set_Theory]S
set_equipotent_set_plus_one [in Continuum.Cardinality]set_equipotent_subset_plus_difference [in Continuum.Cardinality]
set_equals_subset_union_difference [in Continuum.Cardinality]
sierpinskis_theorem [in Continuum.Sierpinskis_Theorem]
small_class_is_a_set [in Continuum.Cardinality]
strip_element [in Continuum.Basic_Set_Theory]
subset_extensionality [in Continuum.Basic_Set_Theory]
successor_linearity [in Continuum.Ordinals]
symmetric_cartesian_product_is_increasing [in Continuum.Cardinality]
T
transitive_set_of_ordinals_is_ordinal [in Continuum.Ordinals]transported_relation_is_isomorphic [in Continuum.Ordinals]
two_times_set_is_disjoin_union [in Continuum.Basic_Set_Theory]
two_is_power_set_of_one [in Continuum.Cardinality]
U
union_of_disjoints_equipotent_disjoint_union [in Continuum.Cardinality]unordered_pair_equals_unordered_pair_iff [in Continuum.Basic_Set_Theory]
untyped_pair_is_injective_right [in Continuum.Basic_Set_Theory]
untyped_pair_is_injective_left [in Continuum.Basic_Set_Theory]
W
well_founded_induction [in Continuum.Basic_Set_Theory]well_order_has_least_elements [in Continuum.Ordinals]
Well_Ordering_to_Choice [in Continuum.Sierpinskis_Theorem]
Axiom Index
B
big_union [in Continuum.Basic_Set_Theory]E
empty_set [in Continuum.Basic_Set_Theory]extensionality [in Continuum.Basic_Set_Theory]
I
in_Numeral_iff' [in Continuum.Basic_Set_Theory]in_replacement_iff [in Continuum.Basic_Set_Theory]
in_power_set_iff [in Continuum.Basic_Set_Theory]
in_big_union_iff [in Continuum.Basic_Set_Theory]
in_empty_set_iff [in Continuum.Basic_Set_Theory]
In_Set [in Continuum.Basic_Set_Theory]
N
Numeral [in Continuum.Basic_Set_Theory]P
power_set [in Continuum.Basic_Set_Theory]R
replacement [in Continuum.Basic_Set_Theory]S
sets_are_well_founded [in Continuum.Basic_Set_Theory]Set_ [in Continuum.Basic_Set_Theory]
Constructor Index
B
big_union_is_ordinal [in Continuum.Ordinals]build_is_unique_solution [in Continuum.Basic_Set_Theory]
build_element [in Continuum.Basic_Set_Theory]
build_class [in Continuum.Basic_Set_Theory]
build_surjection [in Continuum.Cardinality]
build_injection [in Continuum.Cardinality]
build_bijection [in Continuum.Cardinality]
build_well_order [in Continuum.Ordinals]
F
functionality [in Continuum.Basic_Set_Theory]I
in_class [in Continuum.Basic_Set_Theory]is_accessible_intro [in Continuum.Basic_Set_Theory]
S
successor_is_ordinal [in Continuum.Ordinals]Projection Index
B
bijection_left_right [in Continuum.Cardinality]bijection_right_left [in Continuum.Cardinality]
bijection_to_left [in Continuum.Cardinality]
bijection_to_right [in Continuum.Cardinality]
E
element_property [in Continuum.Basic_Set_Theory]element_value [in Continuum.Basic_Set_Theory]
element_predicate [in Continuum.Basic_Set_Theory]
F
functionality [in Continuum.Basic_Set_Theory]I
injection_property [in Continuum.Cardinality]injection_fun [in Continuum.Cardinality]
in_class [in Continuum.Basic_Set_Theory]
S
surjection_is_surjective [in Continuum.Cardinality]surjection_fun [in Continuum.Cardinality]
U
unique_solution_is_unique [in Continuum.Basic_Set_Theory]unique_solution_is_solution [in Continuum.Basic_Set_Theory]
W
well_order_is_well_founded [in Continuum.Ordinals]well_order_is_linear [in Continuum.Ordinals]
well_order_is_irreflexive [in Continuum.Ordinals]
well_order_is_transitive [in Continuum.Ordinals]
well_order_relation [in Continuum.Ordinals]
Inductive Index
F
Functional [in Continuum.Basic_Set_Theory]I
In_Class [in Continuum.Basic_Set_Theory]Is_Accessible_By [in Continuum.Basic_Set_Theory]
Is_Ordinal [in Continuum.Ordinals]
Instance Index
B
bijection_subrelation_flipped_injection [in Continuum.Cardinality]bijection_subrelation_injection [in Continuum.Cardinality]
D
description_is_unique [in Continuum.Basic_Set_Theory]E
element_of_tail_is_element_of_adjunction [in Continuum.Basic_Set_Theory]element_stays_element [in Continuum.Basic_Set_Theory]
element_of_ordinal_is_ordinal [in Continuum.Ordinals]
F
fun_replacement_in_power_set [in Continuum.Basic_Set_Theory]H
head_is_element_of_adjunction [in Continuum.Basic_Set_Theory]I
in_indexed_union [in Continuum.Basic_Set_Theory]in_union_intro_right [in Continuum.Basic_Set_Theory]
in_union_intro_left [in Continuum.Basic_Set_Theory]
in_union_intro2 [in Continuum.Basic_Set_Theory]
in_union_intro1 [in Continuum.Basic_Set_Theory]
in_image_of [in Continuum.Basic_Set_Theory]
in_image_under [in Continuum.Basic_Set_Theory]
in_set_if_in_subset [in Continuum.Basic_Set_Theory]
in_class_of_all_sets [in Continuum.Basic_Set_Theory]
O
ordinal_is_in_Ordinal [in Continuum.Ordinals]ordinal_is_ordinal [in Continuum.Ordinals]
R
reflexive_closure_is_partial_order [in Continuum.Ordinals]reflexive_closure_is_pre_order [in Continuum.Ordinals]
S
set_in_power_set [in Continuum.Basic_Set_Theory]subset_relation_transitivity [in Continuum.Basic_Set_Theory]
subset_relation_reflexivity [in Continuum.Basic_Set_Theory]
subset_subrelation_injection [in Continuum.Cardinality]
W
well_order_is_strict_order [in Continuum.Ordinals]Section Index
D
Description [in Continuum.Basic_Set_Theory]Abbreviation Index
E
element [in Continuum.Basic_Set_Theory]O
ordinal_order_relation [in Continuum.Ordinals]S
S [in Continuum.Basic_Set_Theory]other
σ [in Continuum.Basic_Set_Theory]Definition Index
A
adjunction [in Continuum.Basic_Set_Theory]All [in Continuum.Basic_Set_Theory]
Any [in Continuum.Basic_Set_Theory]
Axiom_Of_Choice [in Continuum.Sierpinskis_Theorem]
Axiom_Of_Choice' [in Continuum.Sierpinskis_Theorem]
B
bijection_relation_on_Set [in Continuum.Cardinality]bijection_relation [in Continuum.Cardinality]
C
cartesian_product [in Continuum.Basic_Set_Theory]class_of_all_sets [in Continuum.Basic_Set_Theory]
class_as_set [in Continuum.Cardinality]
compose_injections [in Continuum.Cardinality]
compose_bijections [in Continuum.Cardinality]
compose_isos [in Continuum.Ordinals]
comprehension [in Continuum.Basic_Set_Theory]
conditional_fun_replacement [in Continuum.Basic_Set_Theory]
D
decode [in Continuum.Ordinals]description [in Continuum.Basic_Set_Theory]
difference [in Continuum.Basic_Set_Theory]
Disjoint [in Continuum.Cardinality]
disjoint_union_ind [in Continuum.Basic_Set_Theory]
disjoint_union_iter [in Continuum.Basic_Set_Theory]
Disjoint_Union_Iter_Property [in Continuum.Basic_Set_Theory]
disjoint_union [in Continuum.Basic_Set_Theory]
E
encode [in Continuum.Ordinals]encodings [in Continuum.Ordinals]
explicit_set [in Continuum.Basic_Set_Theory]
extract_from_right [in Continuum.Basic_Set_Theory]
extract_from_left [in Continuum.Basic_Set_Theory]
F
fun_replacement [in Continuum.Basic_Set_Theory]G
Generalized_Continuum_Hypothesis [in Continuum.Sierpinskis_Theorem]Greater [in Continuum.Ordinals]
H
hartogs_number [in Continuum.Hartogs_Number]hartogs_number_as_class [in Continuum.Hartogs_Number]
I
id_injection [in Continuum.Cardinality]id_bijection [in Continuum.Cardinality]
image_of [in Continuum.Basic_Set_Theory]
image_under [in Continuum.Basic_Set_Theory]
indexed_intersection [in Continuum.Basic_Set_Theory]
indexed_union [in Continuum.Basic_Set_Theory]
Infinite [in Continuum.Sierpinskis_Theorem]
injection_relation_on_Set [in Continuum.Cardinality]
injection_relation [in Continuum.Cardinality]
injection_as_bijection_into_image [in Continuum.Cardinality]
inj1 [in Continuum.Basic_Set_Theory]
inj2 [in Continuum.Basic_Set_Theory]
intersection [in Continuum.Basic_Set_Theory]
inverse_bijection [in Continuum.Cardinality]
Isomorphism [in Continuum.Ordinals]
isomorphism_relation [in Continuum.Ordinals]
isomorphism_inverse [in Continuum.Ordinals]
Is_From_Right [in Continuum.Basic_Set_Theory]
Is_From_Left [in Continuum.Basic_Set_Theory]
Is_Well_Founded [in Continuum.Basic_Set_Theory]
Is_Subset_Of [in Continuum.Basic_Set_Theory]
Is_A_Set [in Continuum.Cardinality]
Is_Surjective [in Continuum.Cardinality]
Is_Transitive_Set [in Continuum.Ordinals]
Is_Linear_Relation [in Continuum.Ordinals]
L
least_element [in Continuum.Ordinals]left_projection [in Continuum.Basic_Set_Theory]
Less [in Continuum.Ordinals]
Less_Or_Equal [in Continuum.Cardinality]
N
nat_to_numeral [in Continuum.Basic_Set_Theory]nat_to_numeral' [in Continuum.Basic_Set_Theory]
Numeral_iter [in Continuum.Basic_Set_Theory]
Numeral_iter_Property [in Continuum.Basic_Set_Theory]
Numeral_ind [in Continuum.Basic_Set_Theory]
numeral_S [in Continuum.Basic_Set_Theory]
numeral_O [in Continuum.Basic_Set_Theory]
O
Ordinal [in Continuum.Ordinals]ordinal_order [in Continuum.Ordinals]
P
pair [in Continuum.Basic_Set_Theory]Preserves_Relation [in Continuum.Ordinals]
provisional_singleton [in Continuum.Basic_Set_Theory]
provisional_unordered_pair [in Continuum.Basic_Set_Theory]
R
reflexive_closure [in Continuum.Ordinals]restrict_well_order [in Continuum.Ordinals]
right_projection [in Continuum.Basic_Set_Theory]
S
solutions [in Continuum.Basic_Set_Theory]T
transport_well_order [in Continuum.Ordinals]transport_relation [in Continuum.Ordinals]
U
union [in Continuum.Basic_Set_Theory]untyped_pair [in Continuum.Basic_Set_Theory]
W
Well_Ordering_Theorem [in Continuum.Sierpinskis_Theorem]Record Index
B
Bijection [in Continuum.Cardinality]C
Class [in Continuum.Basic_Set_Theory]E
Element_Of [in Continuum.Basic_Set_Theory]F
Functional [in Continuum.Basic_Set_Theory]I
Injection [in Continuum.Cardinality]In_Class [in Continuum.Basic_Set_Theory]
Is_Unique_Solution_Of [in Continuum.Basic_Set_Theory]
S
Surjection [in Continuum.Cardinality]W
Well_Order_On [in Continuum.Ordinals]| 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 | (323 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 | (32 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| 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 | (112 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 | (14 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 | (12 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 | (20 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 | (4 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 | (26 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 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 | (84 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 | (9 entries) |
This page has been generated by coqdoc