| 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 | (289 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 | (31 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 | (19 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 | (16 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 | (33 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| 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 | (65 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 | (7 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 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 | (62 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 | (10 entries) |
Global Index
A
and [constructor, in Continuum.Definability]and_is_definable [instance, in Continuum.Definability]
application_is_definable [lemma, in Continuum.Definability]
Axioms [library]
B
`{ _ | _ : _ , _ : _ } [notation, in Continuum.Basic_Constructions]_ ∩ _ [notation, in Continuum.Basic_Constructions]
_ ∪ _ [notation, in Continuum.Basic_Constructions]
⋃ _ : _ , _ [notation, in Continuum.Basic_Constructions]
`{ _ ⊆ _ | _ } [notation, in Continuum.Basic_Constructions]
`{ _ ∈ _ | _ } [notation, in Continuum.Basic_Constructions]
`{ _ | _ : _ } [notation, in Continuum.Basic_Constructions]
`{ _ } [notation, in Continuum.Basic_Constructions]
Basic_Constructions [section, in Continuum.Basic_Constructions]
Basic_Constructions [library]
big_union [projection, in Continuum.Axioms]
big_union_in_L [definition, in Continuum.L]
big_union_is_definable [instance, in Continuum.Basic_Constructions]
build_env_reduction [constructor, in Continuum.Definability]
build_definability [constructor, in Continuum.Definability]
build_zf_model [constructor, in Continuum.Axioms]
build_zf_operations [constructor, in Continuum.Axioms]
build_class_like [constructor, in Continuum.ZF_Structures]
build_encoding [constructor, in Continuum.ZF_Structures]
build_element [constructor, in Continuum.ZF_Structures]
build_class [constructor, in Continuum.ZF_Structures]
build_zf_structure [constructor, in Continuum.ZF_Structures]
build_encoding_from_injection [definition, in Continuum.Basic_Constructions]
build_set_like [constructor, in Continuum.Basic_Constructions]
C
canonical_set_like_is_definable [instance, in Continuum.Basic_Constructions]canonical_class_like_is_definable [instance, in Continuum.Basic_Constructions]
Class [record, in Continuum.ZF_Structures]
Classes [section, in Continuum.ZF_Structures]
Class_Like_weakening [instance, in Continuum.Definability]
Class_weakening [instance, in Continuum.Definability]
class_like_encoding [projection, in Continuum.ZF_Structures]
class_like_type [projection, in Continuum.ZF_Structures]
Class_Like [record, in Continuum.ZF_Structures]
class_as_set [definition, in Continuum.ZF_Structures]
compose_env_reductions [definition, in Continuum.Definability]
composition_is_env_reduction [instance, in Continuum.Definability]
composition_with_env_tail_is_env_reduction [constructor, in Continuum.Definability]
const [constructor, in Continuum.Definability]
constants_form_subset [lemma, in Continuum.L]
constants_of_term_form_subset [lemma, in Continuum.L]
constants_of [definition, in Continuum.L]
constants_of_term [definition, in Continuum.L]
constant_element_is_definable [instance, in Continuum.Definability]
constructible_model [definition, in Continuum.L]
D
decode [projection, in Continuum.ZF_Structures]decode_encode [projection, in Continuum.ZF_Structures]
Def [definition, in Continuum.L]
Definability [section, in Continuum.Definability]
Definability [library]
definability_proof_is_definable [instance, in Continuum.Definability]
definability_on_constant_definability [instance, in Continuum.Definability]
definability_on_Class_Like [instance, in Continuum.Definability]
definability_on_Encoding [instance, in Continuum.Definability]
definability_on_Class [instance, in Continuum.Definability]
definability_on_type_with_encoding [instance, in Continuum.Definability]
definability_on_Prop [instance, in Continuum.Definability]
definability_on_fun_type [definition, in Continuum.Definability]
definability_on_Type [instance, in Continuum.Definability]
definability_on [definition, in Continuum.Definability]
Definability_On [record, in Continuum.Definability]
definability_on_Set_Like [instance, in Continuum.Basic_Constructions]
definable_subset_is_a_set_in_L [lemma, in Continuum.L]
definable_subset_is_in_L [lemma, in Continuum.L]
Def_is_definable [instance, in Continuum.L]
description [axiom, in Continuum.Basic_Constructions]
description_property [axiom, in Continuum.Basic_Constructions]
E
element [abbreviation, in Continuum.ZF_Structures]elements_of_vector_in_countable_union [lemma, in Continuum.L]
elements_of_vector [definition, in Continuum.L]
element_relation_is_definable [instance, in Continuum.Definability]
element_is_definable [instance, in Continuum.Definability]
element_value_is_definable [instance, in Continuum.Definability]
element_equality [lemma, in Continuum.ZF_Structures]
element_property [projection, in Continuum.ZF_Structures]
element_value [projection, in Continuum.ZF_Structures]
Element_Of [record, in Continuum.ZF_Structures]
element_relation [definition, in Continuum.ZF_Structures]
element_predicate [projection, in Continuum.ZF_Structures]
element_relation_on_sets [projection, in Continuum.ZF_Structures]
empty_set [projection, in Continuum.Axioms]
empty_set_in_L [definition, in Continuum.L]
encode [projection, in Continuum.ZF_Structures]
encode_is_definable [instance, in Continuum.Definability]
encode_is_injective [lemma, in Continuum.Basic_Constructions]
Encodings [section, in Continuum.ZF_Structures]
encoding_of_class_is_definable [instance, in Continuum.Definability]
encoding_of_the_universe_is_definable [instance, in Continuum.Definability]
Encoding_weakening [instance, in Continuum.Definability]
encoding_of_set_is_a_set [instance, in Continuum.ZF_Structures]
encoding_of_class [instance, in Continuum.ZF_Structures]
encoding_of_the_universe [instance, in Continuum.ZF_Structures]
encoding_of [definition, in Continuum.ZF_Structures]
encoding_carrier [projection, in Continuum.ZF_Structures]
Encoding_Of [record, in Continuum.ZF_Structures]
encoding_of_nat_is_a_set [instance, in Continuum.L]
encoding_of_nat [instance, in Continuum.L]
Encoding_Of_Vector_Is_A_Set [instance, in Continuum.L]
Encoding_Of_Vector [instance, in Continuum.L]
encoding_of_set_like_is_definable [instance, in Continuum.Basic_Constructions]
Environments [section, in Continuum.Definability]
env_reduction_id [definition, in Continuum.Definability]
env_reduction_property [projection, in Continuum.Definability]
env_reduction_fun [projection, in Continuum.Definability]
Env_Reduction [record, in Continuum.Definability]
env_head [definition, in Continuum.Definability]
env_tail [definition, in Continuum.Definability]
env_cons [definition, in Continuum.Definability]
env_nil [definition, in Continuum.Definability]
env_type_head [definition, in Continuum.Definability]
env_type_tail [definition, in Continuum.Definability]
env_type_cons [definition, in Continuum.Definability]
env_type_nil [definition, in Continuum.Definability]
Env_Type [definition, in Continuum.Definability]
Env_Type_and_Typed_Env [definition, in Continuum.Definability]
equal [constructor, in Continuum.Definability]
equality_is_definable [instance, in Continuum.Definability]
erase_types [definition, in Continuum.Definability]
eval [definition, in Continuum.Definability]
eval_term [definition, in Continuum.Definability]
eval_term_on_lower_term [lemma, in Continuum.L]
eval_over [definition, in Continuum.L]
everything_is_in_full_class [instance, in Continuum.ZF_Structures]
exist [constructor, in Continuum.Definability]
extensionality [projection, in Continuum.Axioms]
ex_statement_is_definable [instance, in Continuum.Definability]
F
False_is_definable [instance, in Continuum.Definability]First_Order_Logic [section, in Continuum.Definability]
forall_statement_is_definable [instance, in Continuum.Definability]
Formula [inductive, in Continuum.Definability]
Formula_Over [definition, in Continuum.L]
foundation [projection, in Continuum.Axioms]
fst_is_definable [instance, in Continuum.Basic_Constructions]
full_class [definition, in Continuum.ZF_Structures]
fun_weakening [lemma, in Continuum.Definability]
I
id_is_env_reduction [constructor, in Continuum.Definability]impl_is_definable [instance, in Continuum.Definability]
indexed_union_of_ordinals_is_ordinal [instance, in Continuum.L]
indexed_union_is_definable [instance, in Continuum.Basic_Constructions]
indexed_union [definition, in Continuum.Basic_Constructions]
infinite_set_property [projection, in Continuum.Axioms]
infinite_set [projection, in Continuum.Axioms]
infinite_set_in_L [definition, in Continuum.L]
intersection [axiom, in Continuum.Basic_Constructions]
in_relation_replacement_iff [projection, in Continuum.Axioms]
in_big_union_iff [projection, in Continuum.Axioms]
in_power_set_iff [projection, in Continuum.Axioms]
in_unordered_pair_iff [projection, in Continuum.Axioms]
in_class_as_set_iff [lemma, in Continuum.ZF_Structures]
in_stage_of_indexed_union [lemma, in Continuum.L]
in_replacement2_iff [lemma, in Continuum.Basic_Constructions]
in_intersection_iff [axiom, in Continuum.Basic_Constructions]
in_union_iff [axiom, in Continuum.Basic_Constructions]
in_indexed_union_iff [lemma, in Continuum.Basic_Constructions]
in_separation_iff [axiom, in Continuum.Basic_Constructions]
in_replacement_iff [lemma, in Continuum.Basic_Constructions]
in_singleton_iff [lemma, in Continuum.Basic_Constructions]
Is_Definable [abbreviation, in Continuum.Definability]
Is_Env_Reduction [inductive, in Continuum.Definability]
Is_Definable [abbreviation, in Continuum.Definability]
Is_Definable_In_Env [projection, in Continuum.Definability]
is_element [constructor, in Continuum.Definability]
Is_A_Set [definition, in Continuum.ZF_Structures]
Is_Well_Founded [definition, in Continuum.ZF_Structures]
Is_Functional [definition, in Continuum.ZF_Structures]
Is_Definable_Over [abbreviation, in Continuum.L]
Is_Limit_Ordinal [definition, in Continuum.Basic_Constructions]
Is_Successor_Ordinal [definition, in Continuum.Basic_Constructions]
Is_Injective [definition, in Continuum.Basic_Constructions]
L
L [definition, in Continuum.L]L [section, in Continuum.L]
L [library]
lambda_is_definable [instance, in Continuum.Definability]
least [definition, in Continuum.L]
least_is_solution [lemma, in Continuum.L]
left_sub_ordinal_max [instance, in Continuum.L]
lift_env [definition, in Continuum.L]
lower_vector [definition, in Continuum.L]
lower_formula [definition, in Continuum.L]
lower_term [definition, in Continuum.L]
L_stage_is_monotone [lemma, in Continuum.L]
L_stage_of_indexed_union [lemma, in Continuum.L]
L_stage_is_definable [instance, in Continuum.L]
L_stage_of_union [lemma, in Continuum.L]
L_is_cumulative [lemma, in Continuum.L]
L_is_transitive [lemma, in Continuum.L]
L_as_class_is_definable [instance, in Continuum.L]
L_as_class [definition, in Continuum.L]
L_stage [definition, in Continuum.L]
M
map_element_value_of_lower_vector [lemma, in Continuum.L]N
not [constructor, in Continuum.Definability]not_is_definable [instance, in Continuum.Definability]
not_in_empty_set [projection, in Continuum.Axioms]
numerals [axiom, in Continuum.Basic_Constructions]
O
ordinals [axiom, in Continuum.Basic_Constructions]ordinals_is_transitive [axiom, in Continuum.Basic_Constructions]
ordinal_max [definition, in Continuum.L]
ordinal_recursion_on_limit [axiom, in Continuum.Basic_Constructions]
ordinal_recursion_on_successor [axiom, in Continuum.Basic_Constructions]
ordinal_recursion_is_definable [instance, in Continuum.Basic_Constructions]
ordinal_recursion [axiom, in Continuum.Basic_Constructions]
ordinal_induction [axiom, in Continuum.Basic_Constructions]
ordinal_zero [definition, in Continuum.Basic_Constructions]
ordinal_limit [axiom, in Continuum.Basic_Constructions]
ordinal_successor [axiom, in Continuum.Basic_Constructions]
or_definable [instance, in Continuum.Definability]
P
pair_is_definable [instance, in Continuum.Basic_Constructions]power_set [projection, in Continuum.Axioms]
power_set_in_L [definition, in Continuum.L]
product_encoding [instance, in Continuum.Basic_Constructions]
prod_is_definable [instance, in Continuum.Basic_Constructions]
Prop_weakening [instance, in Continuum.Definability]
R
reflection_theorem [lemma, in Continuum.L]Reflects [definition, in Continuum.L]
relation_replacement [projection, in Continuum.Axioms]
relation_replacement_in_L [definition, in Continuum.L]
replacement [definition, in Continuum.Basic_Constructions]
replacement_is_definable [instance, in Continuum.Basic_Constructions]
replacement2 [definition, in Continuum.Basic_Constructions]
replacement3 [definition, in Continuum.Basic_Constructions]
right_sub_ordinal_max [instance, in Continuum.L]
S
separation [axiom, in Continuum.Basic_Constructions]set_as_class_is_definable [instance, in Continuum.Definability]
set_like_is_definable [instance, in Continuum.Basic_Constructions]
set_like_encoding_is_definable [instance, in Continuum.Basic_Constructions]
set_like_as_set [definition, in Continuum.Basic_Constructions]
set_like_is_a_set [projection, in Continuum.Basic_Constructions]
set_like_encoding [projection, in Continuum.Basic_Constructions]
set_like_type [projection, in Continuum.Basic_Constructions]
Set_Like [record, in Continuum.Basic_Constructions]
singleton [definition, in Continuum.Basic_Constructions]
singleton_is_definable [instance, in Continuum.Basic_Constructions]
stage_sub_L [instance, in Continuum.L]
strip_element [lemma, in Continuum.L]
subset_of_L_is_subset_of_a_stage [lemma, in Continuum.L]
T
Term [inductive, in Continuum.Definability]True_is_definable [instance, in Continuum.Definability]
type_weakening [instance, in Continuum.Definability]
type_of_sets [projection, in Continuum.ZF_Structures]
U
union [definition, in Continuum.Basic_Constructions]union_of_ordinals_is_ordinal [instance, in Continuum.L]
union_is_definable [instance, in Continuum.Basic_Constructions]
unordered_pair [projection, in Continuum.Axioms]
unordered_pair_in_L [definition, in Continuum.L]
unordered_pair_is_definable [instance, in Continuum.Basic_Constructions]
unordered_pairs_are_equal_iff [lemma, in Continuum.Basic_Constructions]
unordered_pairs_are_equal_iff' [lemma, in Continuum.Basic_Constructions]
unordered_pair_symmetric [lemma, in Continuum.Basic_Constructions]
unordered_pairs_are_equal_impl' [lemma, in Continuum.Basic_Constructions]
V
var [constructor, in Continuum.Definability]Vector_In [definition, in Continuum.L]
W
weakening_on_type_with_encoding [lemma, in Continuum.Definability]Z
zf_operations [projection, in Continuum.Axioms]zf_structure [projection, in Continuum.Axioms]
ZF_Model [record, in Continuum.Axioms]
ZF_Operations [record, in Continuum.Axioms]
ZF_Structure [record, in Continuum.ZF_Structures]
zf_operations_on_L [definition, in Continuum.L]
zf_structure_over [definition, in Continuum.L]
ZF_Structures [library]
other
_ ;; _ [notation, in Continuum.Definability]_ ∪ _ [notation, in Continuum.Axioms]
_ ⊆ _ [notation, in Continuum.ZF_Structures]
_ ∉ _ [notation, in Continuum.ZF_Structures]
_ ∈ _ [notation, in Continuum.ZF_Structures]
_ .+5 [notation, in Continuum.ZF_Structures]
_ .+4 [notation, in Continuum.ZF_Structures]
_ .+3 [notation, in Continuum.ZF_Structures]
_ .+2 [notation, in Continuum.ZF_Structures]
_ .+1 [notation, in Continuum.ZF_Structures]
_ ` _ ` _ [notation, in Continuum.ZF_Structures]
_ ∘ _ [notation, in Continuum.ZF_Structures]
_ ∩ _ [notation, in Continuum.Basic_Constructions]
_ ∪ _ [notation, in Continuum.Basic_Constructions]
`{ _ } [notation, in Continuum.Axioms]
`{ _ , _ } [notation, in Continuum.Axioms]
`{ _ | _ } [notation, in Continuum.ZF_Structures]
`{ _ | _ : _ , _ : _ } [notation, in Continuum.Basic_Constructions]
`{ _ ⊆ _ | _ } [notation, in Continuum.Basic_Constructions]
`{ _ ∈ _ | _ } [notation, in Continuum.Basic_Constructions]
`{ _ | _ : _ } [notation, in Continuum.Basic_Constructions]
`{ _ } [notation, in Continuum.Basic_Constructions]
∅ [notation, in Continuum.Axioms]
⋃ _ : _ , _ [notation, in Continuum.Basic_Constructions]
σ [abbreviation, in Continuum.Basic_Constructions]
𝒫 [abbreviation, in Continuum.Axioms]
Notation Index
B
`{ _ | _ : _ , _ : _ } [in Continuum.Basic_Constructions]_ ∩ _ [in Continuum.Basic_Constructions]
_ ∪ _ [in Continuum.Basic_Constructions]
⋃ _ : _ , _ [in Continuum.Basic_Constructions]
`{ _ ⊆ _ | _ } [in Continuum.Basic_Constructions]
`{ _ ∈ _ | _ } [in Continuum.Basic_Constructions]
`{ _ | _ : _ } [in Continuum.Basic_Constructions]
`{ _ } [in Continuum.Basic_Constructions]
other
_ ;; _ [in Continuum.Definability]_ ∪ _ [in Continuum.Axioms]
_ ⊆ _ [in Continuum.ZF_Structures]
_ ∉ _ [in Continuum.ZF_Structures]
_ ∈ _ [in Continuum.ZF_Structures]
_ .+5 [in Continuum.ZF_Structures]
_ .+4 [in Continuum.ZF_Structures]
_ .+3 [in Continuum.ZF_Structures]
_ .+2 [in Continuum.ZF_Structures]
_ .+1 [in Continuum.ZF_Structures]
_ ` _ ` _ [in Continuum.ZF_Structures]
_ ∘ _ [in Continuum.ZF_Structures]
_ ∩ _ [in Continuum.Basic_Constructions]
_ ∪ _ [in Continuum.Basic_Constructions]
`{ _ } [in Continuum.Axioms]
`{ _ , _ } [in Continuum.Axioms]
`{ _ | _ } [in Continuum.ZF_Structures]
`{ _ | _ : _ , _ : _ } [in Continuum.Basic_Constructions]
`{ _ ⊆ _ | _ } [in Continuum.Basic_Constructions]
`{ _ ∈ _ | _ } [in Continuum.Basic_Constructions]
`{ _ | _ : _ } [in Continuum.Basic_Constructions]
`{ _ } [in Continuum.Basic_Constructions]
∅ [in Continuum.Axioms]
⋃ _ : _ , _ [in Continuum.Basic_Constructions]
Library Index
A
AxiomsB
Basic_ConstructionsD
DefinabilityL
LZ
ZF_StructuresLemma Index
A
application_is_definable [in Continuum.Definability]C
constants_form_subset [in Continuum.L]constants_of_term_form_subset [in Continuum.L]
D
definable_subset_is_a_set_in_L [in Continuum.L]definable_subset_is_in_L [in Continuum.L]
E
elements_of_vector_in_countable_union [in Continuum.L]element_equality [in Continuum.ZF_Structures]
encode_is_injective [in Continuum.Basic_Constructions]
eval_term_on_lower_term [in Continuum.L]
F
fun_weakening [in Continuum.Definability]I
in_class_as_set_iff [in Continuum.ZF_Structures]in_stage_of_indexed_union [in Continuum.L]
in_replacement2_iff [in Continuum.Basic_Constructions]
in_indexed_union_iff [in Continuum.Basic_Constructions]
in_replacement_iff [in Continuum.Basic_Constructions]
in_singleton_iff [in Continuum.Basic_Constructions]
L
least_is_solution [in Continuum.L]L_stage_is_monotone [in Continuum.L]
L_stage_of_indexed_union [in Continuum.L]
L_stage_of_union [in Continuum.L]
L_is_cumulative [in Continuum.L]
L_is_transitive [in Continuum.L]
M
map_element_value_of_lower_vector [in Continuum.L]R
reflection_theorem [in Continuum.L]S
strip_element [in Continuum.L]subset_of_L_is_subset_of_a_stage [in Continuum.L]
U
unordered_pairs_are_equal_iff [in Continuum.Basic_Constructions]unordered_pairs_are_equal_iff' [in Continuum.Basic_Constructions]
unordered_pair_symmetric [in Continuum.Basic_Constructions]
unordered_pairs_are_equal_impl' [in Continuum.Basic_Constructions]
W
weakening_on_type_with_encoding [in Continuum.Definability]Constructor Index
A
and [in Continuum.Definability]B
build_env_reduction [in Continuum.Definability]build_definability [in Continuum.Definability]
build_zf_model [in Continuum.Axioms]
build_zf_operations [in Continuum.Axioms]
build_class_like [in Continuum.ZF_Structures]
build_encoding [in Continuum.ZF_Structures]
build_element [in Continuum.ZF_Structures]
build_class [in Continuum.ZF_Structures]
build_zf_structure [in Continuum.ZF_Structures]
build_set_like [in Continuum.Basic_Constructions]
C
composition_with_env_tail_is_env_reduction [in Continuum.Definability]const [in Continuum.Definability]
E
equal [in Continuum.Definability]exist [in Continuum.Definability]
I
id_is_env_reduction [in Continuum.Definability]is_element [in Continuum.Definability]
N
not [in Continuum.Definability]V
var [in Continuum.Definability]Axiom Index
D
description [in Continuum.Basic_Constructions]description_property [in Continuum.Basic_Constructions]
I
intersection [in Continuum.Basic_Constructions]in_intersection_iff [in Continuum.Basic_Constructions]
in_union_iff [in Continuum.Basic_Constructions]
in_separation_iff [in Continuum.Basic_Constructions]
N
numerals [in Continuum.Basic_Constructions]O
ordinals [in Continuum.Basic_Constructions]ordinals_is_transitive [in Continuum.Basic_Constructions]
ordinal_recursion_on_limit [in Continuum.Basic_Constructions]
ordinal_recursion_on_successor [in Continuum.Basic_Constructions]
ordinal_recursion [in Continuum.Basic_Constructions]
ordinal_induction [in Continuum.Basic_Constructions]
ordinal_limit [in Continuum.Basic_Constructions]
ordinal_successor [in Continuum.Basic_Constructions]
S
separation [in Continuum.Basic_Constructions]Projection Index
B
big_union [in Continuum.Axioms]C
class_like_encoding [in Continuum.ZF_Structures]class_like_type [in Continuum.ZF_Structures]
D
decode [in Continuum.ZF_Structures]decode_encode [in Continuum.ZF_Structures]
E
element_property [in Continuum.ZF_Structures]element_value [in Continuum.ZF_Structures]
element_predicate [in Continuum.ZF_Structures]
element_relation_on_sets [in Continuum.ZF_Structures]
empty_set [in Continuum.Axioms]
encode [in Continuum.ZF_Structures]
encoding_carrier [in Continuum.ZF_Structures]
env_reduction_property [in Continuum.Definability]
env_reduction_fun [in Continuum.Definability]
extensionality [in Continuum.Axioms]
F
foundation [in Continuum.Axioms]I
infinite_set_property [in Continuum.Axioms]infinite_set [in Continuum.Axioms]
in_relation_replacement_iff [in Continuum.Axioms]
in_big_union_iff [in Continuum.Axioms]
in_power_set_iff [in Continuum.Axioms]
in_unordered_pair_iff [in Continuum.Axioms]
Is_Definable_In_Env [in Continuum.Definability]
N
not_in_empty_set [in Continuum.Axioms]P
power_set [in Continuum.Axioms]R
relation_replacement [in Continuum.Axioms]S
set_like_is_a_set [in Continuum.Basic_Constructions]set_like_encoding [in Continuum.Basic_Constructions]
set_like_type [in Continuum.Basic_Constructions]
T
type_of_sets [in Continuum.ZF_Structures]U
unordered_pair [in Continuum.Axioms]Z
zf_operations [in Continuum.Axioms]zf_structure [in Continuum.Axioms]
Inductive Index
F
Formula [in Continuum.Definability]I
Is_Env_Reduction [in Continuum.Definability]T
Term [in Continuum.Definability]Instance Index
A
and_is_definable [in Continuum.Definability]B
big_union_is_definable [in Continuum.Basic_Constructions]C
canonical_set_like_is_definable [in Continuum.Basic_Constructions]canonical_class_like_is_definable [in Continuum.Basic_Constructions]
Class_Like_weakening [in Continuum.Definability]
Class_weakening [in Continuum.Definability]
composition_is_env_reduction [in Continuum.Definability]
constant_element_is_definable [in Continuum.Definability]
D
definability_proof_is_definable [in Continuum.Definability]definability_on_constant_definability [in Continuum.Definability]
definability_on_Class_Like [in Continuum.Definability]
definability_on_Encoding [in Continuum.Definability]
definability_on_Class [in Continuum.Definability]
definability_on_type_with_encoding [in Continuum.Definability]
definability_on_Prop [in Continuum.Definability]
definability_on_Type [in Continuum.Definability]
definability_on_Set_Like [in Continuum.Basic_Constructions]
Def_is_definable [in Continuum.L]
E
element_relation_is_definable [in Continuum.Definability]element_is_definable [in Continuum.Definability]
element_value_is_definable [in Continuum.Definability]
encode_is_definable [in Continuum.Definability]
encoding_of_class_is_definable [in Continuum.Definability]
encoding_of_the_universe_is_definable [in Continuum.Definability]
Encoding_weakening [in Continuum.Definability]
encoding_of_set_is_a_set [in Continuum.ZF_Structures]
encoding_of_class [in Continuum.ZF_Structures]
encoding_of_the_universe [in Continuum.ZF_Structures]
encoding_of_nat_is_a_set [in Continuum.L]
encoding_of_nat [in Continuum.L]
Encoding_Of_Vector_Is_A_Set [in Continuum.L]
Encoding_Of_Vector [in Continuum.L]
encoding_of_set_like_is_definable [in Continuum.Basic_Constructions]
equality_is_definable [in Continuum.Definability]
everything_is_in_full_class [in Continuum.ZF_Structures]
ex_statement_is_definable [in Continuum.Definability]
F
False_is_definable [in Continuum.Definability]forall_statement_is_definable [in Continuum.Definability]
fst_is_definable [in Continuum.Basic_Constructions]
I
impl_is_definable [in Continuum.Definability]indexed_union_of_ordinals_is_ordinal [in Continuum.L]
indexed_union_is_definable [in Continuum.Basic_Constructions]
L
lambda_is_definable [in Continuum.Definability]left_sub_ordinal_max [in Continuum.L]
L_stage_is_definable [in Continuum.L]
L_as_class_is_definable [in Continuum.L]
N
not_is_definable [in Continuum.Definability]O
ordinal_recursion_is_definable [in Continuum.Basic_Constructions]or_definable [in Continuum.Definability]
P
pair_is_definable [in Continuum.Basic_Constructions]product_encoding [in Continuum.Basic_Constructions]
prod_is_definable [in Continuum.Basic_Constructions]
Prop_weakening [in Continuum.Definability]
R
replacement_is_definable [in Continuum.Basic_Constructions]right_sub_ordinal_max [in Continuum.L]
S
set_as_class_is_definable [in Continuum.Definability]set_like_is_definable [in Continuum.Basic_Constructions]
set_like_encoding_is_definable [in Continuum.Basic_Constructions]
singleton_is_definable [in Continuum.Basic_Constructions]
stage_sub_L [in Continuum.L]
T
True_is_definable [in Continuum.Definability]type_weakening [in Continuum.Definability]
U
union_of_ordinals_is_ordinal [in Continuum.L]union_is_definable [in Continuum.Basic_Constructions]
unordered_pair_is_definable [in Continuum.Basic_Constructions]
Section Index
B
Basic_Constructions [in Continuum.Basic_Constructions]C
Classes [in Continuum.ZF_Structures]D
Definability [in Continuum.Definability]E
Encodings [in Continuum.ZF_Structures]Environments [in Continuum.Definability]
F
First_Order_Logic [in Continuum.Definability]L
L [in Continuum.L]Abbreviation Index
E
element [in Continuum.ZF_Structures]I
Is_Definable [in Continuum.Definability]Is_Definable [in Continuum.Definability]
Is_Definable_Over [in Continuum.L]
other
σ [in Continuum.Basic_Constructions]𝒫 [in Continuum.Axioms]
Definition Index
B
big_union_in_L [in Continuum.L]build_encoding_from_injection [in Continuum.Basic_Constructions]
C
class_as_set [in Continuum.ZF_Structures]compose_env_reductions [in Continuum.Definability]
constants_of [in Continuum.L]
constants_of_term [in Continuum.L]
constructible_model [in Continuum.L]
D
Def [in Continuum.L]definability_on_fun_type [in Continuum.Definability]
definability_on [in Continuum.Definability]
E
elements_of_vector [in Continuum.L]element_relation [in Continuum.ZF_Structures]
empty_set_in_L [in Continuum.L]
encoding_of [in Continuum.ZF_Structures]
env_reduction_id [in Continuum.Definability]
env_head [in Continuum.Definability]
env_tail [in Continuum.Definability]
env_cons [in Continuum.Definability]
env_nil [in Continuum.Definability]
env_type_head [in Continuum.Definability]
env_type_tail [in Continuum.Definability]
env_type_cons [in Continuum.Definability]
env_type_nil [in Continuum.Definability]
Env_Type [in Continuum.Definability]
Env_Type_and_Typed_Env [in Continuum.Definability]
erase_types [in Continuum.Definability]
eval [in Continuum.Definability]
eval_term [in Continuum.Definability]
eval_over [in Continuum.L]
F
Formula_Over [in Continuum.L]full_class [in Continuum.ZF_Structures]
I
indexed_union [in Continuum.Basic_Constructions]infinite_set_in_L [in Continuum.L]
Is_A_Set [in Continuum.ZF_Structures]
Is_Well_Founded [in Continuum.ZF_Structures]
Is_Functional [in Continuum.ZF_Structures]
Is_Limit_Ordinal [in Continuum.Basic_Constructions]
Is_Successor_Ordinal [in Continuum.Basic_Constructions]
Is_Injective [in Continuum.Basic_Constructions]
L
L [in Continuum.L]least [in Continuum.L]
lift_env [in Continuum.L]
lower_vector [in Continuum.L]
lower_formula [in Continuum.L]
lower_term [in Continuum.L]
L_as_class [in Continuum.L]
L_stage [in Continuum.L]
O
ordinal_max [in Continuum.L]ordinal_zero [in Continuum.Basic_Constructions]
P
power_set_in_L [in Continuum.L]R
Reflects [in Continuum.L]relation_replacement_in_L [in Continuum.L]
replacement [in Continuum.Basic_Constructions]
replacement2 [in Continuum.Basic_Constructions]
replacement3 [in Continuum.Basic_Constructions]
S
set_like_as_set [in Continuum.Basic_Constructions]singleton [in Continuum.Basic_Constructions]
U
union [in Continuum.Basic_Constructions]unordered_pair_in_L [in Continuum.L]
V
Vector_In [in Continuum.L]Z
zf_operations_on_L [in Continuum.L]zf_structure_over [in Continuum.L]
Record Index
C
Class [in Continuum.ZF_Structures]Class_Like [in Continuum.ZF_Structures]
D
Definability_On [in Continuum.Definability]E
Element_Of [in Continuum.ZF_Structures]Encoding_Of [in Continuum.ZF_Structures]
Env_Reduction [in Continuum.Definability]
S
Set_Like [in Continuum.Basic_Constructions]Z
ZF_Model [in Continuum.Axioms]ZF_Operations [in Continuum.Axioms]
ZF_Structure [in Continuum.ZF_Structures]
| 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 | (289 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 | (31 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 | (19 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 | (16 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 | (33 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| 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 | (65 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 | (7 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 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 | (62 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 | (10 entries) |
This page has been generated by coqdoc