| 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 | (224 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (20 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 | (15 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 | (34 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 | (92 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 | (1 entry) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (28 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 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 | (25 entries) |
Global Index
A
and_commutative [lemma, in CoursDeCoq.ex1]and_commutative [lemma, in CoursDeCoq.ex1_auto]
Antisymmetric [definition, in CoursDeCoq.Relations_1]
B
Bottom [inductive, in CoursDeCoq.podefs_1]Bottom_definition [constructor, in CoursDeCoq.podefs_1]
Bounds [section, in CoursDeCoq.podefs_1]
Bounds.C [variable, in CoursDeCoq.podefs_1]
Bounds.D [variable, in CoursDeCoq.podefs_1]
Bounds.R [variable, in CoursDeCoq.podefs_1]
Bounds.U [variable, in CoursDeCoq.podefs_1]
C
Carrier [definition, in CoursDeCoq.podefs]Carrier_of [lemma, in CoursDeCoq.podefs]
Chain [definition, in CoursDeCoq.podefs_1]
coherent [definition, in CoursDeCoq.Relations_3]
coherent_symmetric [lemma, in CoursDeCoq.Relations_3_facts]
Compatible [definition, in CoursDeCoq.podefs_1]
Compatible_is_symmetric [lemma, in CoursDeCoq.Partial_order_facts]
Compatible_is_reflexive [lemma, in CoursDeCoq.Partial_order_facts]
Complement [definition, in CoursDeCoq.Relations_1_facts]
Complete [inductive, in CoursDeCoq.podefs_1]
Conditionally_complete [inductive, in CoursDeCoq.podefs_1]
Conditionally_complete_has_a_bottom [lemma, in CoursDeCoq.Partial_order_facts]
Confluent [definition, in CoursDeCoq.Relations_3]
confluent [definition, in CoursDeCoq.Relations_3]
contains [definition, in CoursDeCoq.Relations_1]
contains_is_preorder [lemma, in CoursDeCoq.Relations_1_facts]
Couple [inductive, in CoursDeCoq.Ensembles]
Couple_is_symmetric [lemma, in CoursDeCoq.Partial_order_facts]
Couple_included_in_carrier [lemma, in CoursDeCoq.Partial_order_facts]
Couple_r [constructor, in CoursDeCoq.Ensembles]
Couple_l [constructor, in CoursDeCoq.Ensembles]
Cpo [definition, in CoursDeCoq.podefs_1]
D
Definition_of_Conditionally_complete [constructor, in CoursDeCoq.podefs_1]Definition_of_Complete [constructor, in CoursDeCoq.podefs_1]
Definition_of_Directed [constructor, in CoursDeCoq.podefs_1]
Definition_of_PO [constructor, in CoursDeCoq.podefs]
Definition_of_PER [constructor, in CoursDeCoq.Relations_1]
Definition_of_equivalence [constructor, in CoursDeCoq.Relations_1]
Definition_of_order [constructor, in CoursDeCoq.Relations_1]
Definition_of_preorder [constructor, in CoursDeCoq.Relations_1]
Definition_of_Power_set [constructor, in CoursDeCoq.ps]
definition_of_noetherian [constructor, in CoursDeCoq.Relations_3]
Directed [inductive, in CoursDeCoq.podefs_1]
Disjoint [inductive, in CoursDeCoq.Ensembles]
Disjoint_intro [constructor, in CoursDeCoq.Ensembles]
drinker [library]
drinker's_theorem [lemma, in CoursDeCoq.drinker]
E
Empty_set_has_lub [lemma, in CoursDeCoq.Partial_order_facts]Empty_set_has_Upper_Bound [lemma, in CoursDeCoq.Partial_order_facts]
Empty_is_finite [constructor, in CoursDeCoq.Ensembles]
Empty_set [inductive, in CoursDeCoq.Ensembles]
Empty_set_zero [lemma, in CoursDeCoq.ps]
Empty_set_is_Bottom [lemma, in CoursDeCoq.ps]
Empty_set_minimal [lemma, in CoursDeCoq.ps]
Ensemble [definition, in CoursDeCoq.Ensembles]
Ensembles [section, in CoursDeCoq.Ensembles]
Ensembles [library]
Ensembles.U [variable, in CoursDeCoq.Ensembles]
Equivalence [inductive, in CoursDeCoq.Relations_1]
Equiv_from_order [lemma, in CoursDeCoq.Relations_1_facts]
Equiv_from_preorder [lemma, in CoursDeCoq.Relations_1_facts]
Extensionality_Ensembles [axiom, in CoursDeCoq.Ensembles]
ex1 [library]
ex1_auto [library]
F
Fil [library]Finite [inductive, in CoursDeCoq.Ensembles]
Finite_plus_one_is_finite [lemma, in CoursDeCoq.ps]
First_inductive_lemmas.D [variable, in CoursDeCoq.Fil]
First_inductive_lemmas.B [variable, in CoursDeCoq.Fil]
First_inductive_lemmas.U [variable, in CoursDeCoq.Fil]
First_inductive_lemmas [section, in CoursDeCoq.Fil]
G
Glb [inductive, in CoursDeCoq.podefs_1]Glb_definition [constructor, in CoursDeCoq.podefs_1]
I
In [definition, in CoursDeCoq.Ensembles]Included [definition, in CoursDeCoq.Ensembles]
Inclusion_is_transitive [lemma, in CoursDeCoq.ps]
Inclusion_is_an_order [lemma, in CoursDeCoq.ps]
Intersection [inductive, in CoursDeCoq.Ensembles]
Intersection_intro [constructor, in CoursDeCoq.Ensembles]
Intersection_is_Glb [lemma, in CoursDeCoq.ps]
Intersection_decreases_r [lemma, in CoursDeCoq.ps]
Intersection_decreases_l [lemma, in CoursDeCoq.ps]
Intersection_maximal [lemma, in CoursDeCoq.ps]
In_singleton [constructor, in CoursDeCoq.Ensembles]
L
Lemmas_on_partial_orders.D [variable, in CoursDeCoq.Partial_order_facts]Lemmas_on_partial_orders.B [variable, in CoursDeCoq.Partial_order_facts]
Lemmas_on_partial_orders.U [variable, in CoursDeCoq.Partial_order_facts]
Lemmas_on_partial_orders [section, in CoursDeCoq.Partial_order_facts]
Lemma1 [lemma, in CoursDeCoq.Relations_2_facts]
Locally_confluent [definition, in CoursDeCoq.Relations_3]
locally_confluent [definition, in CoursDeCoq.Relations_3]
Lower_Bound_definition [constructor, in CoursDeCoq.podefs_1]
Lower_Bound [inductive, in CoursDeCoq.podefs_1]
Lub [inductive, in CoursDeCoq.podefs_1]
Lub_definition [constructor, in CoursDeCoq.podefs_1]
Lub_is_in_Carrier [lemma, in CoursDeCoq.Partial_order_facts]
M
mini_cases [lemma, in CoursDeCoq.ex1]mini_cases [lemma, in CoursDeCoq.ex1_auto]
mp [lemma, in CoursDeCoq.ex1]
mp [lemma, in CoursDeCoq.ex1_auto]
N
Newman [lemma, in CoursDeCoq.Relations_3_facts]Noetherian [definition, in CoursDeCoq.Relations_3]
noetherian [inductive, in CoursDeCoq.Relations_3]
Noetherian_contains_Noetherian [lemma, in CoursDeCoq.Relations_3_facts]
Non_empty_intro [constructor, in CoursDeCoq.Ensembles]
Non_empty [inductive, in CoursDeCoq.Ensembles]
Non_disjoint_union [lemma, in CoursDeCoq.ps]
not_quite_classic [lemma, in CoursDeCoq.ex1]
not_not_converse [lemma, in CoursDeCoq.ex1]
not_not [lemma, in CoursDeCoq.ex1]
not_quite_classic [lemma, in CoursDeCoq.ex1_auto]
not_not_converse [lemma, in CoursDeCoq.ex1_auto]
not_not [lemma, in CoursDeCoq.ex1_auto]
O
Order [inductive, in CoursDeCoq.Relations_1]or_commutative [lemma, in CoursDeCoq.ex1]
or_commutative [lemma, in CoursDeCoq.ex1_auto]
P
Pairs_are_enough [lemma, in CoursDeCoq.Fil]Pairs_are_enough_finite_case [lemma, in CoursDeCoq.Fil]
Partial_orders.U [variable, in CoursDeCoq.podefs]
Partial_orders [section, in CoursDeCoq.podefs]
Partial_order_facts [library]
Peirce [lemma, in CoursDeCoq.ex1_auto]
PER [inductive, in CoursDeCoq.Relations_1]
PO [inductive, in CoursDeCoq.podefs]
podefs [library]
podefs_1 [library]
Power_set_PO [lemma, in CoursDeCoq.ps]
Power_set_non_empty [lemma, in CoursDeCoq.ps]
Power_set [inductive, in CoursDeCoq.ps]
Praeclarum [lemma, in CoursDeCoq.ex1]
Praeclarum [lemma, in CoursDeCoq.ex1_auto]
Preorder [inductive, in CoursDeCoq.Relations_1]
ps [library]
R
Reflexive [definition, in CoursDeCoq.Relations_1]Rel [definition, in CoursDeCoq.podefs]
Relation [definition, in CoursDeCoq.Relations_1]
Relations_1.R [variable, in CoursDeCoq.Relations_1]
Relations_1.U [variable, in CoursDeCoq.Relations_1]
Relations_1 [section, in CoursDeCoq.Relations_1]
Relations_2.R [variable, in CoursDeCoq.Relations_2]
Relations_2.U [variable, in CoursDeCoq.Relations_2]
Relations_2 [section, in CoursDeCoq.Relations_2]
Relations_3.R [variable, in CoursDeCoq.Relations_3]
Relations_3.U [variable, in CoursDeCoq.Relations_3]
Relations_3 [section, in CoursDeCoq.Relations_3]
Relations_2 [library]
Relations_3 [library]
Relations_1 [library]
Relations_1_facts [library]
Relations_2_facts [library]
Relations_3_facts [library]
Rel_of_transitive [lemma, in CoursDeCoq.Partial_order_facts]
Rel_of_antisymmetric [lemma, in CoursDeCoq.Partial_order_facts]
Rel_of_reflexive [lemma, in CoursDeCoq.Partial_order_facts]
Rel_of [lemma, in CoursDeCoq.podefs]
resolution [lemma, in CoursDeCoq.ex1]
resolution [lemma, in CoursDeCoq.ex1_auto]
Rplus [inductive, in CoursDeCoq.Relations_2]
Rplus_n [constructor, in CoursDeCoq.Relations_2]
Rplus_0 [constructor, in CoursDeCoq.Relations_2]
Rplus_contains_R [lemma, in CoursDeCoq.Relations_2_facts]
Rstar [inductive, in CoursDeCoq.Relations_2]
RstarRplus_RRstar [lemma, in CoursDeCoq.Relations_2_facts]
Rstar_n [constructor, in CoursDeCoq.Relations_2]
Rstar_0 [constructor, in CoursDeCoq.Relations_2]
Rstar_equiv_Rstar1 [lemma, in CoursDeCoq.Relations_2_facts]
Rstar_cases [lemma, in CoursDeCoq.Relations_2_facts]
Rstar_transitive [lemma, in CoursDeCoq.Relations_2_facts]
Rstar_contains_Rplus [lemma, in CoursDeCoq.Relations_2_facts]
Rstar_contains_R [lemma, in CoursDeCoq.Relations_2_facts]
Rstar_reflexive [lemma, in CoursDeCoq.Relations_2_facts]
Rstar_imp_coherent [lemma, in CoursDeCoq.Relations_3_facts]
Rstar1 [inductive, in CoursDeCoq.Relations_2]
Rstar1_n [constructor, in CoursDeCoq.Relations_2]
Rstar1_1 [constructor, in CoursDeCoq.Relations_2]
Rstar1_0 [constructor, in CoursDeCoq.Relations_2]
Rsym_imp_Rstarsym [lemma, in CoursDeCoq.Relations_2_facts]
Rsym_imp_notRsym [lemma, in CoursDeCoq.Relations_1_facts]
S
S [lemma, in CoursDeCoq.ex1]S [lemma, in CoursDeCoq.ex1_auto]
same_relation [definition, in CoursDeCoq.Relations_1]
Same_set_intro [lemma, in CoursDeCoq.Ensembles]
Same_set [definition, in CoursDeCoq.Ensembles]
Same_set_reflexive [lemma, in CoursDeCoq.ps]
Same_set_equivalence [lemma, in CoursDeCoq.ps]
same_relation_is_equivalence [lemma, in CoursDeCoq.Relations_1_facts]
Setminus [inductive, in CoursDeCoq.Ensembles]
Setminus_intro [constructor, in CoursDeCoq.Ensembles]
Simple [lemma, in CoursDeCoq.ex1]
Simple [lemma, in CoursDeCoq.ex1_auto]
Singleton [inductive, in CoursDeCoq.Ensembles]
Singleton_has_lub [lemma, in CoursDeCoq.Partial_order_facts]
Singleton_is_finite [lemma, in CoursDeCoq.ps]
SRel_of [definition, in CoursDeCoq.podefs]
Sstar_contains_Rstar [lemma, in CoursDeCoq.Relations_2_facts]
star_monotone [lemma, in CoursDeCoq.Relations_2_facts]
Strongly_confluent [definition, in CoursDeCoq.Relations_2]
Strong_confluence_direct [lemma, in CoursDeCoq.Relations_3_facts]
Strong_confluence [lemma, in CoursDeCoq.Relations_3_facts]
Symmetric [definition, in CoursDeCoq.Relations_1]
T
The_power_set_partial_order.A [variable, in CoursDeCoq.ps]The_power_set_partial_order.U [variable, in CoursDeCoq.ps]
The_power_set_partial_order [section, in CoursDeCoq.ps]
Totally_ordered_definition [constructor, in CoursDeCoq.podefs_1]
Totally_ordered [inductive, in CoursDeCoq.podefs_1]
Transitive [definition, in CoursDeCoq.Relations_1]
trivial [lemma, in CoursDeCoq.ex1]
trivial [lemma, in CoursDeCoq.ex1_auto]
U
Union [inductive, in CoursDeCoq.Ensembles]Union_is_finite [constructor, in CoursDeCoq.Ensembles]
Union_intror [constructor, in CoursDeCoq.Ensembles]
Union_introl [constructor, in CoursDeCoq.Ensembles]
Union_of_finite_is_finite [lemma, in CoursDeCoq.ps]
Union_associative [lemma, in CoursDeCoq.ps]
Union_commutative [lemma, in CoursDeCoq.ps]
Union_is_Lub [lemma, in CoursDeCoq.ps]
Union_increases_r [lemma, in CoursDeCoq.ps]
Union_increases_l [lemma, in CoursDeCoq.ps]
Union_minimal [lemma, in CoursDeCoq.ps]
Upper_Bound_definition [constructor, in CoursDeCoq.podefs_1]
Upper_Bound [inductive, in CoursDeCoq.podefs_1]
Upper_downward_stable [lemma, in CoursDeCoq.Partial_order_facts]
W
Witnesses [lemma, in CoursDeCoq.ex1]Witnesses [lemma, in CoursDeCoq.ex1_auto]
Variable Index
B
Bounds.C [in CoursDeCoq.podefs_1]Bounds.D [in CoursDeCoq.podefs_1]
Bounds.R [in CoursDeCoq.podefs_1]
Bounds.U [in CoursDeCoq.podefs_1]
E
Ensembles.U [in CoursDeCoq.Ensembles]F
First_inductive_lemmas.D [in CoursDeCoq.Fil]First_inductive_lemmas.B [in CoursDeCoq.Fil]
First_inductive_lemmas.U [in CoursDeCoq.Fil]
L
Lemmas_on_partial_orders.D [in CoursDeCoq.Partial_order_facts]Lemmas_on_partial_orders.B [in CoursDeCoq.Partial_order_facts]
Lemmas_on_partial_orders.U [in CoursDeCoq.Partial_order_facts]
P
Partial_orders.U [in CoursDeCoq.podefs]R
Relations_1.R [in CoursDeCoq.Relations_1]Relations_1.U [in CoursDeCoq.Relations_1]
Relations_2.R [in CoursDeCoq.Relations_2]
Relations_2.U [in CoursDeCoq.Relations_2]
Relations_3.R [in CoursDeCoq.Relations_3]
Relations_3.U [in CoursDeCoq.Relations_3]
T
The_power_set_partial_order.A [in CoursDeCoq.ps]The_power_set_partial_order.U [in CoursDeCoq.ps]
Library Index
D
drinkerE
Ensemblesex1
ex1_auto
F
FilP
Partial_order_factspodefs
podefs_1
ps
R
Relations_2Relations_3
Relations_1
Relations_1_facts
Relations_2_facts
Relations_3_facts
Constructor Index
B
Bottom_definition [in CoursDeCoq.podefs_1]C
Couple_r [in CoursDeCoq.Ensembles]Couple_l [in CoursDeCoq.Ensembles]
D
Definition_of_Conditionally_complete [in CoursDeCoq.podefs_1]Definition_of_Complete [in CoursDeCoq.podefs_1]
Definition_of_Directed [in CoursDeCoq.podefs_1]
Definition_of_PO [in CoursDeCoq.podefs]
Definition_of_PER [in CoursDeCoq.Relations_1]
Definition_of_equivalence [in CoursDeCoq.Relations_1]
Definition_of_order [in CoursDeCoq.Relations_1]
Definition_of_preorder [in CoursDeCoq.Relations_1]
Definition_of_Power_set [in CoursDeCoq.ps]
definition_of_noetherian [in CoursDeCoq.Relations_3]
Disjoint_intro [in CoursDeCoq.Ensembles]
E
Empty_is_finite [in CoursDeCoq.Ensembles]G
Glb_definition [in CoursDeCoq.podefs_1]I
Intersection_intro [in CoursDeCoq.Ensembles]In_singleton [in CoursDeCoq.Ensembles]
L
Lower_Bound_definition [in CoursDeCoq.podefs_1]Lub_definition [in CoursDeCoq.podefs_1]
N
Non_empty_intro [in CoursDeCoq.Ensembles]R
Rplus_n [in CoursDeCoq.Relations_2]Rplus_0 [in CoursDeCoq.Relations_2]
Rstar_n [in CoursDeCoq.Relations_2]
Rstar_0 [in CoursDeCoq.Relations_2]
Rstar1_n [in CoursDeCoq.Relations_2]
Rstar1_1 [in CoursDeCoq.Relations_2]
Rstar1_0 [in CoursDeCoq.Relations_2]
S
Setminus_intro [in CoursDeCoq.Ensembles]T
Totally_ordered_definition [in CoursDeCoq.podefs_1]U
Union_is_finite [in CoursDeCoq.Ensembles]Union_intror [in CoursDeCoq.Ensembles]
Union_introl [in CoursDeCoq.Ensembles]
Upper_Bound_definition [in CoursDeCoq.podefs_1]
Lemma Index
A
and_commutative [in CoursDeCoq.ex1]and_commutative [in CoursDeCoq.ex1_auto]
C
Carrier_of [in CoursDeCoq.podefs]coherent_symmetric [in CoursDeCoq.Relations_3_facts]
Compatible_is_symmetric [in CoursDeCoq.Partial_order_facts]
Compatible_is_reflexive [in CoursDeCoq.Partial_order_facts]
Conditionally_complete_has_a_bottom [in CoursDeCoq.Partial_order_facts]
contains_is_preorder [in CoursDeCoq.Relations_1_facts]
Couple_is_symmetric [in CoursDeCoq.Partial_order_facts]
Couple_included_in_carrier [in CoursDeCoq.Partial_order_facts]
D
drinker's_theorem [in CoursDeCoq.drinker]E
Empty_set_has_lub [in CoursDeCoq.Partial_order_facts]Empty_set_has_Upper_Bound [in CoursDeCoq.Partial_order_facts]
Empty_set_zero [in CoursDeCoq.ps]
Empty_set_is_Bottom [in CoursDeCoq.ps]
Empty_set_minimal [in CoursDeCoq.ps]
Equiv_from_order [in CoursDeCoq.Relations_1_facts]
Equiv_from_preorder [in CoursDeCoq.Relations_1_facts]
F
Finite_plus_one_is_finite [in CoursDeCoq.ps]I
Inclusion_is_transitive [in CoursDeCoq.ps]Inclusion_is_an_order [in CoursDeCoq.ps]
Intersection_is_Glb [in CoursDeCoq.ps]
Intersection_decreases_r [in CoursDeCoq.ps]
Intersection_decreases_l [in CoursDeCoq.ps]
Intersection_maximal [in CoursDeCoq.ps]
L
Lemma1 [in CoursDeCoq.Relations_2_facts]Lub_is_in_Carrier [in CoursDeCoq.Partial_order_facts]
M
mini_cases [in CoursDeCoq.ex1]mini_cases [in CoursDeCoq.ex1_auto]
mp [in CoursDeCoq.ex1]
mp [in CoursDeCoq.ex1_auto]
N
Newman [in CoursDeCoq.Relations_3_facts]Noetherian_contains_Noetherian [in CoursDeCoq.Relations_3_facts]
Non_disjoint_union [in CoursDeCoq.ps]
not_quite_classic [in CoursDeCoq.ex1]
not_not_converse [in CoursDeCoq.ex1]
not_not [in CoursDeCoq.ex1]
not_quite_classic [in CoursDeCoq.ex1_auto]
not_not_converse [in CoursDeCoq.ex1_auto]
not_not [in CoursDeCoq.ex1_auto]
O
or_commutative [in CoursDeCoq.ex1]or_commutative [in CoursDeCoq.ex1_auto]
P
Pairs_are_enough [in CoursDeCoq.Fil]Pairs_are_enough_finite_case [in CoursDeCoq.Fil]
Peirce [in CoursDeCoq.ex1_auto]
Power_set_PO [in CoursDeCoq.ps]
Power_set_non_empty [in CoursDeCoq.ps]
Praeclarum [in CoursDeCoq.ex1]
Praeclarum [in CoursDeCoq.ex1_auto]
R
Rel_of_transitive [in CoursDeCoq.Partial_order_facts]Rel_of_antisymmetric [in CoursDeCoq.Partial_order_facts]
Rel_of_reflexive [in CoursDeCoq.Partial_order_facts]
Rel_of [in CoursDeCoq.podefs]
resolution [in CoursDeCoq.ex1]
resolution [in CoursDeCoq.ex1_auto]
Rplus_contains_R [in CoursDeCoq.Relations_2_facts]
RstarRplus_RRstar [in CoursDeCoq.Relations_2_facts]
Rstar_equiv_Rstar1 [in CoursDeCoq.Relations_2_facts]
Rstar_cases [in CoursDeCoq.Relations_2_facts]
Rstar_transitive [in CoursDeCoq.Relations_2_facts]
Rstar_contains_Rplus [in CoursDeCoq.Relations_2_facts]
Rstar_contains_R [in CoursDeCoq.Relations_2_facts]
Rstar_reflexive [in CoursDeCoq.Relations_2_facts]
Rstar_imp_coherent [in CoursDeCoq.Relations_3_facts]
Rsym_imp_Rstarsym [in CoursDeCoq.Relations_2_facts]
Rsym_imp_notRsym [in CoursDeCoq.Relations_1_facts]
S
S [in CoursDeCoq.ex1]S [in CoursDeCoq.ex1_auto]
Same_set_intro [in CoursDeCoq.Ensembles]
Same_set_reflexive [in CoursDeCoq.ps]
Same_set_equivalence [in CoursDeCoq.ps]
same_relation_is_equivalence [in CoursDeCoq.Relations_1_facts]
Simple [in CoursDeCoq.ex1]
Simple [in CoursDeCoq.ex1_auto]
Singleton_has_lub [in CoursDeCoq.Partial_order_facts]
Singleton_is_finite [in CoursDeCoq.ps]
Sstar_contains_Rstar [in CoursDeCoq.Relations_2_facts]
star_monotone [in CoursDeCoq.Relations_2_facts]
Strong_confluence_direct [in CoursDeCoq.Relations_3_facts]
Strong_confluence [in CoursDeCoq.Relations_3_facts]
T
trivial [in CoursDeCoq.ex1]trivial [in CoursDeCoq.ex1_auto]
U
Union_of_finite_is_finite [in CoursDeCoq.ps]Union_associative [in CoursDeCoq.ps]
Union_commutative [in CoursDeCoq.ps]
Union_is_Lub [in CoursDeCoq.ps]
Union_increases_r [in CoursDeCoq.ps]
Union_increases_l [in CoursDeCoq.ps]
Union_minimal [in CoursDeCoq.ps]
Upper_downward_stable [in CoursDeCoq.Partial_order_facts]
W
Witnesses [in CoursDeCoq.ex1]Witnesses [in CoursDeCoq.ex1_auto]
Axiom Index
E
Extensionality_Ensembles [in CoursDeCoq.Ensembles]Inductive Index
B
Bottom [in CoursDeCoq.podefs_1]C
Complete [in CoursDeCoq.podefs_1]Conditionally_complete [in CoursDeCoq.podefs_1]
Couple [in CoursDeCoq.Ensembles]
D
Directed [in CoursDeCoq.podefs_1]Disjoint [in CoursDeCoq.Ensembles]
E
Empty_set [in CoursDeCoq.Ensembles]Equivalence [in CoursDeCoq.Relations_1]
F
Finite [in CoursDeCoq.Ensembles]G
Glb [in CoursDeCoq.podefs_1]I
Intersection [in CoursDeCoq.Ensembles]L
Lower_Bound [in CoursDeCoq.podefs_1]Lub [in CoursDeCoq.podefs_1]
N
noetherian [in CoursDeCoq.Relations_3]Non_empty [in CoursDeCoq.Ensembles]
O
Order [in CoursDeCoq.Relations_1]P
PER [in CoursDeCoq.Relations_1]PO [in CoursDeCoq.podefs]
Power_set [in CoursDeCoq.ps]
Preorder [in CoursDeCoq.Relations_1]
R
Rplus [in CoursDeCoq.Relations_2]Rstar [in CoursDeCoq.Relations_2]
Rstar1 [in CoursDeCoq.Relations_2]
S
Setminus [in CoursDeCoq.Ensembles]Singleton [in CoursDeCoq.Ensembles]
T
Totally_ordered [in CoursDeCoq.podefs_1]U
Union [in CoursDeCoq.Ensembles]Upper_Bound [in CoursDeCoq.podefs_1]
Section Index
B
Bounds [in CoursDeCoq.podefs_1]E
Ensembles [in CoursDeCoq.Ensembles]F
First_inductive_lemmas [in CoursDeCoq.Fil]L
Lemmas_on_partial_orders [in CoursDeCoq.Partial_order_facts]P
Partial_orders [in CoursDeCoq.podefs]R
Relations_1 [in CoursDeCoq.Relations_1]Relations_2 [in CoursDeCoq.Relations_2]
Relations_3 [in CoursDeCoq.Relations_3]
T
The_power_set_partial_order [in CoursDeCoq.ps]Definition Index
A
Antisymmetric [in CoursDeCoq.Relations_1]C
Carrier [in CoursDeCoq.podefs]Chain [in CoursDeCoq.podefs_1]
coherent [in CoursDeCoq.Relations_3]
Compatible [in CoursDeCoq.podefs_1]
Complement [in CoursDeCoq.Relations_1_facts]
Confluent [in CoursDeCoq.Relations_3]
confluent [in CoursDeCoq.Relations_3]
contains [in CoursDeCoq.Relations_1]
Cpo [in CoursDeCoq.podefs_1]
E
Ensemble [in CoursDeCoq.Ensembles]I
In [in CoursDeCoq.Ensembles]Included [in CoursDeCoq.Ensembles]
L
Locally_confluent [in CoursDeCoq.Relations_3]locally_confluent [in CoursDeCoq.Relations_3]
N
Noetherian [in CoursDeCoq.Relations_3]R
Reflexive [in CoursDeCoq.Relations_1]Rel [in CoursDeCoq.podefs]
Relation [in CoursDeCoq.Relations_1]
S
same_relation [in CoursDeCoq.Relations_1]Same_set [in CoursDeCoq.Ensembles]
SRel_of [in CoursDeCoq.podefs]
Strongly_confluent [in CoursDeCoq.Relations_2]
Symmetric [in CoursDeCoq.Relations_1]
T
Transitive [in CoursDeCoq.Relations_1]| 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 | (224 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (20 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 | (15 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 | (34 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 | (92 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 | (1 entry) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (28 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 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 | (25 entries) |