| 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 | (2040 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 | (17 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 | (91 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 | (14 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 | (1530 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 | (81 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 | (4 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 | (2 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 | (230 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 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 | (7 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 | (51 entries) |
Global Index
A
AB_fixed.B [variable, in Epsilon]AB_fixed.A [variable, in Epsilon]
AB_fixed [section, in Epsilon]
acute [definition, in Ch11_angles]
acute_comp_not_acute [lemma, in Ch13_4_cos]
acute_not_obtuse [lemma, in Ch13_4_cos]
acute_col_out [lemma, in Ch13_3_angles]
acute_not_bet [lemma, in Ch13_3_angles]
acute_not_per [lemma, in Ch13_5_Pappus_Pascal]
acute_trivial [lemma, in Ch13_5_Pappus_Pascal]
acute_distinct [lemma, in Ch11_angles]
acute_lea_acute [lemma, in Ch11_angles]
acute_sym [lemma, in Ch11_angles]
addition [projection, in hilbert_axioms]
allButLastCP [definition, in arity]
allButLastCPTl [lemma, in arity]
all_eqaa [lemma, in Ch13_3_angles]
all_eqa [lemma, in Ch13_3_angles]
all_eql [lemma, in Ch13_2_length]
all_one_side_par_strict [lemma, in Ch12_parallel]
altitude_intersect [lemma, in orthocenter]
altitude_is_perp_bisect [lemma, in orthocenter]
ang [definition, in Ch13_3_angles]
anga [definition, in Ch13_3_angles]
anga_col_null [lemma, in Ch13_4_cos]
anga_not_lg_null [lemma, in Ch13_4_cos]
anga_out_anga [lemma, in Ch13_4_cos]
anga_conga_anga [lemma, in Ch13_4_cos]
anga_col_out [lemma, in Ch13_4_cos]
anga_const_o [lemma, in Ch13_3_angles]
anga_not_flat [lemma, in Ch13_3_angles]
anga_acute [lemma, in Ch13_3_angles]
anga_const [lemma, in Ch13_3_angles]
anga_distincts [lemma, in Ch13_3_angles]
anga_not_null_lg [lemma, in Ch13_3_angles]
anga_sym [lemma, in Ch13_3_angles]
anga_distinct [lemma, in Ch13_3_angles]
anga_conga [lemma, in Ch13_3_angles]
anga_is_ang [lemma, in Ch13_3_angles]
anga_exists [lemma, in Ch13_3_angles]
angle [definition, in tarski_to_hilbert]
Angle [definition, in tarski_to_hilbert]
angle [definition, in Ch13_3_angles]
anglea [definition, in Ch13_3_angles]
Angles_5 [section, in Ch13_3_angles]
Angles_4 [section, in Ch13_3_angles]
Angles_3 [section, in Ch13_3_angles]
Angles_2 [section, in Ch13_3_angles]
Angles_1 [section, in Ch13_3_angles]
angle_construction_3 [lemma, in Ch11_angles]
angle_construction_2 [lemma, in Ch11_angles]
angle_construction_1 [lemma, in Ch11_angles]
ang_not_lg_null [lemma, in Ch13_4_cos]
ang_cong_ang [lemma, in Ch13_3_angles]
ang_const_o [lemma, in Ch13_3_angles]
ang_distincts [lemma, in Ch13_3_angles]
ang_not_null_lg [lemma, in Ch13_3_angles]
ang_sym [lemma, in Ch13_3_angles]
ang_const [lemma, in Ch13_3_angles]
ang_distinct [lemma, in Ch13_3_angles]
ang_conga [lemma, in Ch13_3_angles]
ang_exists [lemma, in Ch13_3_angles]
another_point [lemma, in Ch03_bet]
another_point [lemma, in tarski_to_beeson]
app [definition, in arity]
app_2_n_app_eq [lemma, in arity]
app_app_2_n_default [lemma, in arity]
app_app_2_n [lemma, in arity]
app_2_n_app_default [lemma, in arity]
app_2_n_app [lemma, in arity]
app_2_n [definition, in arity]
app_1_n_app_eq [lemma, in arity]
app_app_1_n [lemma, in arity]
app_1_n_app [lemma, in arity]
app_1_n [definition, in arity]
app_n_1_app_eq [lemma, in arity]
app_app_n_1 [lemma, in arity]
app_n_1_app [lemma, in arity]
app_n_1 [definition, in arity]
arity [definition, in arity]
Arity [record, in tactics_axioms]
arity [library]
aux [lemma, in tarski_to_hilbert]
aux [projection, in hilbert_axioms]
aux [library]
axiom_cong_5' [lemma, in tarski_to_hilbert]
axiom_hcong_4_unicity [lemma, in tarski_to_hilbert]
axiom_hcong_4_existence [lemma, in tarski_to_hilbert]
axiom_hcong_3 [lemma, in tarski_to_hilbert]
axiom_hcong_refl [lemma, in tarski_to_hilbert]
axiom_hcong_trans [lemma, in tarski_to_hilbert]
axiom_hcong_scott [lemma, in tarski_to_hilbert]
axiom_hcong_1_unicity [lemma, in tarski_to_hilbert]
axiom_hcong_1_existence [lemma, in tarski_to_hilbert]
axiom_euclid_unicity [lemma, in tarski_to_hilbert]
axiom_euclid_existence [lemma, in tarski_to_hilbert]
axiom_pasch [lemma, in tarski_to_hilbert]
axiom_between_one [lemma, in tarski_to_hilbert]
axiom_between_only_one [lemma, in tarski_to_hilbert]
axiom_between_out [lemma, in tarski_to_hilbert]
axiom_between_comm [lemma, in tarski_to_hilbert]
axiom_between_col [lemma, in tarski_to_hilbert]
axiom_plan [lemma, in tarski_to_hilbert]
axiom_two_points_on_line [lemma, in tarski_to_hilbert]
axiom_line_unicity [lemma, in tarski_to_hilbert]
axiom_line_existence [lemma, in tarski_to_hilbert]
B
Beeson_2.Bet_stability [variable, in Ch03_bet]Beeson_2 [section, in Ch03_bet]
Beeson_1.Cong_stability [variable, in Ch03_bet]
Beeson_1 [section, in Ch03_bet]
Beeson_follows_from_Tarski [instance, in tarski_to_beeson]
Bet [projection, in tarski_axioms]
BetH [definition, in tarski_to_beeson]
BetH [projection, in hilbert_axioms]
BetH_Bet [lemma, in tarski_to_beeson]
BetM [projection, in tarski_axioms]
BetT [definition, in tarski_to_beeson]
BetT_id [lemma, in tarski_to_beeson]
BetT_symmetry [lemma, in tarski_to_beeson]
between_exchange4 [lemma, in Ch03_bet]
between_exchange2 [lemma, in Ch03_bet]
between_exchange3 [lemma, in Ch03_bet]
between_inner_transitivity [lemma, in Ch03_bet]
between_egality [lemma, in Ch03_bet]
between_trivial2 [lemma, in Ch03_bet]
between_symmetry [lemma, in Ch03_bet]
between_trivial [lemma, in Ch03_bet]
between_one [lemma, in tarski_to_hilbert]
Between_H [definition, in tarski_to_hilbert]
between_symmetry [lemma, in tarski_to_makarios]
between_trivial [lemma, in tarski_to_makarios]
between_identity [projection, in tarski_axioms]
between_symmetry_B [lemma, in tarski_to_beeson]
between_inner_transitivity_B [lemma, in tarski_to_beeson]
between_identity_B [lemma, in tarski_to_beeson]
between_symmetric [lemma, in Ch11_angles]
between_cong_3 [lemma, in Ch05_bet_le]
between_cong_2 [lemma, in Ch05_bet_le]
between_cong [lemma, in Ch05_bet_le]
between_one [projection, in hilbert_axioms]
between_only_one [projection, in hilbert_axioms]
between_out [projection, in hilbert_axioms]
between_comm [projection, in hilbert_axioms]
between_col [projection, in hilbert_axioms]
bet_half_bet [lemma, in orientation]
bet_double_bet [lemma, in orientation]
bet_le_le [lemma, in orientation]
bet_out_out_bet [lemma, in Ch06_out_lines]
bet_dec_eq_dec_b [lemma, in Ch03_bet]
Bet_4 [definition, in Ch03_bet]
Bet_perm [lemma, in Ch03_bet]
Bet_cases [lemma, in Ch03_bet]
bet_dec_eq_dec [lemma, in Ch03_bet]
bet_col [lemma, in Ch03_bet]
Bet_tagged_Bet [lemma, in Tagged_predicates]
Bet_Bet_tagged [lemma, in Tagged_predicates]
Bet_tagged [definition, in Tagged_predicates]
Bet_Between_H [lemma, in tarski_to_hilbert]
bet_flat_ang [lemma, in Ch13_3_angles]
Bet_stability [projection, in tarski_axioms]
bet_cong3 [lemma, in Ch08_orthogonality]
bet_cong_bet [lemma, in quadrilaterals]
bet_half_bet [lemma, in quadrilaterals]
bet_double_bet [lemma, in quadrilaterals]
bet_le_le [lemma, in quadrilaterals]
bet_col2 [lemma, in Ch07_midpoint]
bet_col1 [lemma, in Ch07_midpoint]
bet_id [lemma, in tarski_to_beeson]
Bet_T [lemma, in tarski_to_beeson]
bet_stability [lemma, in tarski_to_beeson]
bet_le_eq [lemma, in Ch11_angles]
bet_in_angle_bet [lemma, in Ch11_angles]
bet_conga_bet [lemma, in Ch11_angles]
bet_out [lemma, in Ch11_angles]
bet_same_dir2 [lemma, in vectors]
bet_same_dir1 [lemma, in vectors]
bet_cong_eq [lemma, in Ch05_bet_le]
Bet_dec [lemma, in Ch05_bet_le]
bet2_cong_bet [lemma, in quadrilaterals]
bet2_out_out [lemma, in Ch11_angles]
bet3_cong3_bet [lemma, in quadrilaterals]
build_couple [constructor, in aux]
build_triple [constructor, in aux]
C
cartesianPower [definition, in arity]cartesianPowerAux [definition, in arity]
chasles [lemma, in vectors]
choice_fun_ind [lemma, in Epsilon]
choice_fun_e [lemma, in Epsilon]
choice_fun [definition, in Epsilon]
Ch02_cong [library]
Ch03_bet [library]
Ch04_cong_bet [library]
Ch04_col [library]
Ch05_bet_le [library]
Ch06_out_lines [library]
Ch07_midpoint [library]
Ch08_orthogonality [library]
Ch09_plane [library]
Ch10_line_reflexivity [library]
Ch10_line_reflexivity_2D [library]
Ch11_angles [library]
Ch12 [section, in orientation]
Ch12_parallel_inter_dec [library]
Ch12_parallel [library]
Ch13_3_angles [library]
Ch13_2_length [library]
Ch13_6_Desargues_Hessenberg [library]
Ch13_4_cos [library]
Ch13_1 [library]
Ch13_5_Pappus_Pascal [library]
circPermNConsOK [lemma, in arity]
circPermNConsTlOK [lemma, in arity]
circPermNCP [definition, in arity]
circPermNCPOK [lemma, in arity]
circPermNCP0 [lemma, in arity]
circPermNId [lemma, in arity]
circPermNIdAux [lemma, in arity]
circPermNIdFirst [lemma, in arity]
circPermPerm [lemma, in arity]
Circumcenter [section, in circumcenter]
circumcenter [library]
circumcenter_intersect [lemma, in circumcenter]
circumcenter_perp [lemma, in circumcenter]
circumcenter_cong [lemma, in circumcenter]
coapp [projection, in tactics_axioms]
coapp_perm_2 [projection, in tactics_axioms]
coapp_perm_1 [projection, in tactics_axioms]
Coapp_theory [record, in tactics_axioms]
Coapp_predicates [record, in tactics_axioms]
COATpoint [projection, in tactics_axioms]
Col [definition, in Ch03_bet]
col [definition, in tarski_to_coapp_theory]
ColB [definition, in tarski_to_beeson]
ColB_Col [lemma, in tarski_to_beeson]
collect_diffs [lemma, in ColR]
collect_cols [lemma, in ColR]
ColR [library]
cols_coincide_2 [lemma, in tarski_to_hilbert]
cols_coincide_1 [lemma, in tarski_to_hilbert]
colx [lemma, in Ch09_plane]
col_proj_proj [lemma, in orientation]
col_proj_col [lemma, in orientation]
col_transitivity_2 [lemma, in Ch06_out_lines]
col_transitivity_1 [lemma, in Ch06_out_lines]
col_cong_cong [lemma, in quadrilaterals_inter_dec]
Col_tagged_Col [lemma, in ColR]
Col_Col_tagged [lemma, in ColR]
Col_tagged [definition, in ColR]
Col_refl [section, in ColR]
Col_tagged_Col [lemma, in Tagged_predicates]
Col_Col_tagged [lemma, in Tagged_predicates]
Col_tagged [definition, in Tagged_predicates]
col_incident [lemma, in tarski_to_hilbert]
col_disjoint_bet [lemma, in tarski_to_hilbert]
Col_H [definition, in tarski_to_hilbert]
col_perm_2 [lemma, in tarski_to_coapp_theory]
col_perm_1 [lemma, in tarski_to_coapp_theory]
col_eq [lemma, in Ch09_plane]
col_preserves_two_sides [lemma, in Ch09_plane]
col_col_per_per [lemma, in Ch08_orthogonality]
col_cong_mid2 [lemma, in quadrilaterals]
col_cong_mid1 [lemma, in quadrilaterals]
col_bet2_cong2 [lemma, in quadrilaterals]
col_bet2_cong1 [lemma, in quadrilaterals]
col_cong2_bet4 [lemma, in quadrilaterals]
col_cong2_bet3 [lemma, in quadrilaterals]
col_cong2_bet2 [lemma, in quadrilaterals]
col_cong2_bet1 [lemma, in quadrilaterals]
col_cong_bet [lemma, in quadrilaterals]
col_not_plgs [lemma, in quadrilaterals]
col_cong_mid [lemma, in quadrilaterals]
col_trivial_3 [lemma, in Ch04_col]
col_trivial_2 [lemma, in Ch04_col]
col_trivial_1 [lemma, in Ch04_col]
Col_perm [lemma, in Ch04_col]
Col_cases [lemma, in Ch04_col]
col_permutation_5 [lemma, in Ch04_col]
col_permutation_4 [lemma, in Ch04_col]
col_permutation_3 [lemma, in Ch04_col]
col_permutation_2 [lemma, in Ch04_col]
col_permutation_1 [lemma, in Ch04_col]
col_par_par_col [lemma, in Ch12_parallel_inter_dec]
col_per_perp [lemma, in Ch10_line_reflexivity]
Col_theory [record, in tactics_axioms]
Col_dec [lemma, in tarski_to_beeson]
col_perp_perp_col [lemma, in Ch11_angles]
col_two_sides_bet [lemma, in Ch11_angles]
col_one_side_out [lemma, in Ch11_angles]
col_conga_col [lemma, in Ch11_angles]
col_out2_col [lemma, in Ch11_angles]
col_in_angle_out [lemma, in Ch11_angles]
col_in_angle [lemma, in Ch11_angles]
col_one_side [lemma, in Ch11_angles]
col_two_sides [lemma, in Ch11_angles]
Col_dec [lemma, in Ch05_bet_le]
col_par [lemma, in Ch12_parallel]
col_not_col_not_par [lemma, in Ch12_parallel]
col3 [lemma, in Ch06_out_lines]
compute_new_set_of_sets_of_collinear_points_ok [lemma, in ColR]
Cond [projection, in aux]
Cong [projection, in tarski_axioms]
Conga [definition, in Ch11_angles]
CongaH [projection, in hilbert_axioms]
conga_to_par_os [lemma, in quadrilaterals_inter_dec]
conga_to_par_ts [lemma, in quadrilaterals_inter_dec]
Conga_3 [definition, in project]
conga_distinct [lemma, in Ch11_angles]
Conga_dec [lemma, in Ch11_angles]
conga_sym_equiv [lemma, in Ch11_angles]
conga_preserves_gta [lemma, in Ch11_angles]
conga_preserves_lta [lemma, in Ch11_angles]
conga_preserves_in_angle [lemma, in Ch11_angles]
conga_ex_cong3 [lemma, in Ch11_angles]
conga_line [lemma, in Ch11_angles]
conga_comm [lemma, in Ch11_angles]
conga_left_comm [lemma, in Ch11_angles]
conga_right_comm [lemma, in Ch11_angles]
conga_trivial_1 [lemma, in Ch11_angles]
conga_pseudo_refl [lemma, in Ch11_angles]
conga_trans [lemma, in Ch11_angles]
conga_diff2 [lemma, in Ch11_angles]
conga_diff1 [lemma, in Ch11_angles]
conga_sym [lemma, in Ch11_angles]
conga_refl [lemma, in Ch11_angles]
CongH [projection, in hilbert_axioms]
CongM [projection, in tarski_axioms]
cong_le_le [lemma, in orientation]
cong_identity_inv [lemma, in orientation]
cong_dec_eq_dec_b [lemma, in Ch03_bet]
Cong_tagged_Cong [lemma, in Tagged_predicates]
Cong_Cong_tagged [lemma, in Tagged_predicates]
Cong_tagged [definition, in Tagged_predicates]
cong_conga3_cong3 [lemma, in project]
cong_pseudo_reflexivity [lemma, in tarski_to_makarios]
cong_left_commutativity [lemma, in tarski_to_makarios]
cong_symmetry [lemma, in tarski_to_makarios]
cong_reflexivity [lemma, in tarski_to_makarios]
Cong_stability [projection, in tarski_axioms]
cong_inner_transitivity [projection, in tarski_axioms]
cong_identity [projection, in tarski_axioms]
cong_pseudo_reflexivity [projection, in tarski_axioms]
cong_le_le [lemma, in quadrilaterals]
cong_identity_inv [lemma, in quadrilaterals]
Cong_perm [lemma, in Ch02_cong]
Cong_cases [lemma, in Ch02_cong]
cong_3_swap_2 [lemma, in Ch02_cong]
cong_3_swap [lemma, in Ch02_cong]
cong_3_sym [lemma, in Ch02_cong]
Cong_3 [definition, in Ch02_cong]
cong_diff_4 [lemma, in Ch02_cong]
cong_diff_3 [lemma, in Ch02_cong]
cong_diff_2 [lemma, in Ch02_cong]
cong_diff [lemma, in Ch02_cong]
cong_dec_eq_dec [lemma, in Ch02_cong]
cong_commutativity [lemma, in Ch02_cong]
cong_reverse_identity [lemma, in Ch02_cong]
cong_trivial_identity [lemma, in Ch02_cong]
cong_right_commutativity [lemma, in Ch02_cong]
cong_left_commutativity [lemma, in Ch02_cong]
cong_transitivity [lemma, in Ch02_cong]
cong_symmetry [lemma, in Ch02_cong]
cong_reflexivity [lemma, in Ch02_cong]
cong_cong_half_2 [lemma, in Ch07_midpoint]
cong_cong_half_1 [lemma, in Ch07_midpoint]
cong_col_mid [lemma, in Ch07_midpoint]
cong_conga_perp [lemma, in Ch12_parallel_inter_dec]
cong_stability_eq_stability [lemma, in tarski_to_beeson]
cong_stability [lemma, in tarski_to_beeson]
cong_perp_bisect [lemma, in perp_bisect]
cong_perp_conga [lemma, in Ch13_1]
cong_preserves_le [definition, in Ch11_angles]
cong_preserves_bet [lemma, in Ch11_angles]
Cong_dec [lemma, in Ch05_bet_le]
cong_5 [projection, in hilbert_axioms]
cong_unicity [projection, in hilbert_axioms]
cong_existence [projection, in hilbert_axioms]
cong_refl [projection, in hilbert_axioms]
cong_pseudo_transitivity [projection, in hilbert_axioms]
cong2_conga_cong [lemma, in Ch11_angles]
cong3_par2_par [lemma, in quadrilaterals_inter_dec]
cong3_id [lemma, in quadrilaterals]
cong3_transitivity [lemma, in Ch02_cong]
cong3_bet_eq [lemma, in Ch04_cong_bet]
cong3_preserves_out [lemma, in Ch11_angles]
cong3_conga2 [lemma, in Ch11_angles]
cong3_conga [lemma, in Ch11_angles]
cong3_symmetry [lemma, in Ch05_bet_le]
consHdTlTlHd [lemma, in arity]
consHeadCP [definition, in arity]
consHeadCPHd [lemma, in arity]
consHeadCPOK [lemma, in arity]
consHeadCPTl [lemma, in arity]
consTailCP [definition, in arity]
consTailCPAbl [lemma, in arity]
consTailCPLast [lemma, in arity]
consTailCPOK [lemma, in arity]
consTailCPTl [lemma, in arity]
consTailCPTlD [lemma, in arity]
consTailOK [lemma, in arity]
consTailPerm [lemma, in arity]
consTlHdHdTl [lemma, in arity]
construction_unicity [lemma, in Ch02_cong]
construction_functions [library]
construct_triangle [lemma, in orthocenter]
construct_intersection [lemma, in orthocenter]
coplanar [definition, in Ch10_line_reflexivity]
coplanar [definition, in Ch12_parallel]
coplanar_perm_11 [lemma, in Ch10_line_reflexivity]
coplanar_perm_10 [lemma, in Ch10_line_reflexivity]
coplanar_perm_9 [lemma, in Ch10_line_reflexivity]
coplanar_perm_8 [lemma, in Ch10_line_reflexivity]
coplanar_perm_7 [lemma, in Ch10_line_reflexivity]
coplanar_perm_6 [lemma, in Ch10_line_reflexivity]
coplanar_perm_5 [lemma, in Ch10_line_reflexivity]
coplanar_perm_4 [lemma, in Ch10_line_reflexivity]
coplanar_perm_3 [lemma, in Ch10_line_reflexivity]
coplanar_perm_2 [lemma, in Ch10_line_reflexivity]
coplanar_perm_1 [lemma, in Ch10_line_reflexivity]
Cosinus [section, in Ch13_4_cos]
Couple [record, in aux]
CPCPL [lemma, in arity]
CPLCP [lemma, in arity]
CPLHd [lemma, in arity]
CPLHdTlOK [lemma, in arity]
CPLOCPTlOK [lemma, in sets]
CPLOK [lemma, in arity]
CPLRec [lemma, in arity]
CPPair [definition, in arity]
CPToList [definition, in arity]
CPToListOK [lemma, in arity]
CPToListTl1 [lemma, in arity]
CPToListTl2 [lemma, in arity]
CP_ind [lemma, in arity]
CTcol_trivial_2 [lemma, in ColR]
CTcol_trivial_1 [lemma, in ColR]
CTcol_permutation_4 [lemma, in ColR]
CTcol_permutation_3 [lemma, in ColR]
CTcol_permutation_2 [lemma, in ColR]
CTcol_permutation_5 [lemma, in ColR]
CTcol_permutation_2 [projection, in tactics_axioms]
CTcol_permutation_1 [projection, in tactics_axioms]
CTcol_trivial [projection, in tactics_axioms]
CTcol3 [projection, in tactics_axioms]
cut [definition, in tarski_to_hilbert]
cut_two_sides [lemma, in tarski_to_hilbert]
D
dd' [lemma, in Epsilon]dd'' [lemma, in Epsilon]
definite_description [section, in Epsilon]
Desargues_Hessenberg [section, in Ch13_6_Desargues_Hessenberg]
diff [definition, in tarski_to_coapp_theory]
Diff_tagged_Diff [lemma, in ColR]
Diff_Diff_tagged [lemma, in ColR]
Diff_tagged [definition, in ColR]
Diff_perm [lemma, in Tagged_predicates]
Diff_tagged_Diff [lemma, in Tagged_predicates]
Diff_Diff_tagged [lemma, in Tagged_predicates]
Diff_tagged [definition, in Tagged_predicates]
diff_or_col [lemma, in tarski_to_coapp_theory]
diff_perm_2 [lemma, in tarski_to_coapp_theory]
diff_perm_1 [lemma, in tarski_to_coapp_theory]
diff_col_ex3 [lemma, in Ch09_plane]
diff_bet_ex3 [lemma, in Ch09_plane]
diff_col_ex [lemma, in Ch09_plane]
diff_per_diff [lemma, in Ch08_orthogonality]
diff_bet [lemma, in Ch07_midpoint]
diff_not_col_col_par4_mid [lemma, in orthocenter]
Diff_Col_ColB [lemma, in tarski_to_beeson]
diff_out [lemma, in Ch11_angles]
disjoint [definition, in tarski_to_hilbert]
distinct [lemma, in Ch09_plane]
distinct [lemma, in Ch08_orthogonality]
Distincts [definition, in Ch11_angles]
DistLn [definition, in Ch08_orthogonality]
E
Epsilon [library]epsilon_extensionality [definition, in Epsilon]
epsilon_equiv [lemma, in Epsilon]
epsilon_ind [lemma, in Epsilon]
Eq [definition, in tarski_to_hilbert]
eqA [definition, in Ch13_3_angles]
eqA_preserves_anga [lemma, in Ch13_4_cos]
eqA' [definition, in Ch13_3_angles]
EqDecidability [record, in tarski_axioms]
eqL [definition, in Ch13_2_length]
EqL [projection, in hilbert_axioms]
eql_lg [lemma, in Ch13_4_cos]
eql_lcos_null [lemma, in Ch13_4_cos]
eql_trans [lemma, in Ch13_2_length]
eql_sym [lemma, in Ch13_2_length]
eql_refl [lemma, in Ch13_2_length]
EqL_Equiv [projection, in hilbert_axioms]
eqo [definition, in orientation]
eqop [definition, in ColR]
eqopp [definition, in ColR]
eqo_refl [lemma, in orientation]
eqo_one_side [lemma, in orientation]
eqo_eq_o [lemma, in orientation]
equilateral [definition, in triangles]
equilateral_strict_conga_3 [lemma, in triangles]
equilateral_strict_conga_2 [lemma, in triangles]
equilateral_strict_conga_1 [lemma, in triangles]
equilateral_strict_swap_5 [lemma, in triangles]
equilateral_strict_swap_4 [lemma, in triangles]
equilateral_strict_swap_3 [lemma, in triangles]
equilateral_strict_swap_2 [lemma, in triangles]
equilateral_strict_swap_1 [lemma, in triangles]
equilateral_strict_neq [lemma, in triangles]
equilateral_isosceles_3 [lemma, in triangles]
equilateral_isosceles_2 [lemma, in triangles]
equilateral_isosceles_1 [lemma, in triangles]
equilateral_swap_rot [lemma, in triangles]
equilateral_swap_2 [lemma, in triangles]
equilateral_rot_2 [lemma, in triangles]
equilateral_swap [lemma, in triangles]
equilateral_rot [lemma, in triangles]
equilateral_cong [lemma, in triangles]
equilateral_strict_equilateral [lemma, in triangles]
equilateral_strict [definition, in triangles]
eqV [definition, in vectors]
eqv_cong [lemma, in project]
eqv_eq_project [lemma, in project]
eqv_project_eq_eq [lemma, in project]
eqv_mid [lemma, in vectors]
eqv_sum [lemma, in vectors]
eqv_opp_null [lemma, in vectors]
eqv_par [lemma, in vectors]
eqv_permut [lemma, in vectors]
eqv_trivial [lemma, in vectors]
eqv_comm [lemma, in vectors]
eqv_trans [lemma, in vectors]
eqv_sym [lemma, in vectors]
eqv_refl [lemma, in vectors]
eq_o_refl [lemma, in orientation]
eq_o_one_side [lemma, in orientation]
eq_o_eqo [lemma, in orientation]
eq_o [definition, in orientation]
eq_eq_tagged [lemma, in ColR]
eq_tagged [definition, in ColR]
eq_incident [lemma, in tarski_to_hilbert]
Eq_Equiv [instance, in tarski_to_hilbert]
eq_symmetry [lemma, in tarski_to_hilbert]
eq_reflexivity [lemma, in tarski_to_hilbert]
eq_transitivity [lemma, in tarski_to_hilbert]
eq_dec_points [projection, in tarski_axioms]
eq_dec [lemma, in tarski_to_beeson]
eq_conga_out [lemma, in Ch11_angles]
euclid [projection, in tarski_axioms]
Euclid [section, in perp_bisect]
euclid_unicity [projection, in hilbert_axioms]
euclid_existence [projection, in hilbert_axioms]
Exercises [section, in exercises]
exercises [library]
exists_witness_ok [lemma, in ColR]
exists_witness [definition, in ColR]
exists_not_incident [lemma, in tarski_to_hilbert]
ex_col1 [lemma, in orientation]
ex_col [lemma, in orientation]
ex_unique_introduction [lemma, in Epsilon]
ex_anga [lemma, in Ch13_3_angles]
ex_eqaa [lemma, in Ch13_3_angles]
ex_points_anga [lemma, in Ch13_3_angles]
ex_ang [lemma, in Ch13_3_angles]
ex_eqa [lemma, in Ch13_3_angles]
ex_points_ang [lemma, in Ch13_3_angles]
ex_lg [lemma, in Ch13_2_length]
ex_eql [lemma, in Ch13_2_length]
ex_points_lg_not_col [lemma, in Ch13_2_length]
ex_point_lg_bet [lemma, in Ch13_2_length]
ex_point_lg_out [lemma, in Ch13_2_length]
ex_point_lg [lemma, in Ch13_2_length]
ex_points_lg [lemma, in Ch13_2_length]
ex_col2 [lemma, in Ch08_orthogonality]
ex_col3 [lemma, in quadrilaterals]
ex_sym1 [lemma, in Ch10_line_reflexivity]
ex_sym [lemma, in Ch10_line_reflexivity]
ex_per_cong [lemma, in Ch11_angles]
F
five_segments [lemma, in tarski_to_makarios]five_segments' [lemma, in tarski_to_makarios]
five_segments [projection, in tarski_axioms]
five_segments_with_def [lemma, in Ch02_cong]
five_segments [lemma, in tarski_to_beeson]
five_segments_B [lemma, in tarski_to_beeson]
fixLastCP [definition, in arity]
fixLastCPOK [lemma, in arity]
flat_not_acute [lemma, in Ch13_4_cos]
flat_ang [lemma, in Ch13_3_angles]
forall_def [lemma, in Epsilon]
fourth_point [lemma, in Ch05_bet_le]
FSC [definition, in Ch04_col]
fstpp [definition, in sets]
fst_sp [definition, in ColR]
fst_ss [definition, in ColR]
functional [definition, in Epsilon]
G
ge [definition, in Ch05_bet_le]gea [definition, in Ch11_angles]
general_tactics [library]
get_suitable_pair_of_sets_ok_2 [lemma, in ColR]
get_suitable_pair_of_sets_ok_1 [lemma, in ColR]
get_suitable_pair_of_sets [definition, in ColR]
get_suitable_pair_of_sets_aux [definition, in ColR]
ge_comm [lemma, in Ch11_angles]
ge_right_comm [lemma, in Ch11_angles]
ge_left_comm [lemma, in Ch11_angles]
GravityCenter [section, in gravityCenter]
gravityCenter [library]
gravity_center [definition, in construction_functions]
gt [definition, in Ch05_bet_le]
gta [definition, in Ch11_angles]
gta_trans [lemma, in Ch11_angles]
gt_comm [lemma, in Ch11_angles]
gt_right_comm [lemma, in Ch11_angles]
gt_left_comm [lemma, in Ch11_angles]
H
half_plgs [lemma, in quadrilaterals_inter_dec]have_pair_distinct_points [definition, in ColR]
Hcong [definition, in tarski_to_hilbert]
Hconga [definition, in tarski_to_hilbert]
hconga_Equiv [instance, in tarski_to_hilbert]
hconga_trans [lemma, in tarski_to_hilbert]
hconga_sym [lemma, in tarski_to_hilbert]
hconga_refl [lemma, in tarski_to_hilbert]
hcong_4_unicity [projection, in hilbert_axioms]
hcong_4_existence [projection, in hilbert_axioms]
headCP [definition, in arity]
hEq [definition, in tarski_to_hilbert]
hEq_Equiv [instance, in tarski_to_hilbert]
hEq_trans [lemma, in tarski_to_hilbert]
hEq_sym [lemma, in tarski_to_hilbert]
hEq_refl [lemma, in tarski_to_hilbert]
Hilbert [record, in hilbert_axioms]
Hilbert_follow_from_Tarski [instance, in tarski_to_hilbert]
Hilbert_to_Tarski [section, in tarski_to_hilbert]
hilbert_axioms [library]
hlin [definition, in tarski_to_hilbert]
HLine [definition, in tarski_to_hilbert]
hline_construction [definition, in tarski_to_hilbert]
I
IBet [projection, in tarski_axioms]Ibetween_inner_transitivity [projection, in tarski_axioms]
Ibetween_symmetry [projection, in tarski_axioms]
Ibetween_identity [projection, in tarski_axioms]
ICong [projection, in tarski_axioms]
Icong_inner_transitivity [projection, in tarski_axioms]
Icong_pseudo_reflexivity [projection, in tarski_axioms]
Icong_identity [projection, in tarski_axioms]
Ifive_segments [projection, in tarski_axioms]
IFSC [definition, in Ch04_cong_bet]
Iinner_pasch [projection, in tarski_axioms]
Ilower_dim [projection, in tarski_axioms]
image_cong_col [lemma, in Ch10_line_reflexivity_2D]
image_col [lemma, in Ch10_line_reflexivity]
image_preserves_per [lemma, in Ch10_line_reflexivity]
image_preserves_midpoint [lemma, in Ch10_line_reflexivity]
image_gen_preserves_bet [lemma, in Ch10_line_reflexivity]
image_preserves_bet [lemma, in Ch10_line_reflexivity]
image_in_col0 [lemma, in Ch10_line_reflexivity]
image_in_col [lemma, in Ch10_line_reflexivity]
image_image_in [lemma, in Ch10_line_reflexivity]
image_in_gen_is_image [lemma, in Ch10_line_reflexivity]
image_in_is_image_spec [lemma, in Ch10_line_reflexivity]
image_id [lemma, in Ch10_line_reflexivity]
InAngle [definition, in Ch11_angles]
InAngleH [definition, in tarski_to_hilbert]
inangle_one_side2 [lemma, in Ch13_1]
inangle_one_side [lemma, in Ch13_1]
Incid [projection, in hilbert_axioms]
Incident [definition, in tarski_to_hilbert]
IncidentH [definition, in tarski_to_hilbert]
incident_col [lemma, in tarski_to_hilbert]
incident_Proper [instance, in tarski_to_hilbert]
incident_eq [lemma, in tarski_to_hilbert]
Incid_line [lemma, in tarski_to_hilbert]
InCP [definition, in arity]
InCPOCP [lemma, in sets]
InCPOK [lemma, in arity]
inhabited_bool [lemma, in Epsilon]
inner_pasch [projection, in tarski_axioms]
inner_pasch_B [lemma, in tarski_to_beeson]
InNth [lemma, in arity]
inter [definition, in Ch12_parallel]
InterDecidability [record, in tarski_axioms]
interp [definition, in ColR]
intersection_two_medians_exist_unique [lemma, in gravityCenter]
intersection_two_medians_exist [lemma, in gravityCenter]
inter_unicity [lemma, in Ch09_plane]
inter_dec [projection, in tarski_axioms]
inter_comm [lemma, in Ch12_parallel]
inter_right_comm [lemma, in Ch12_parallel]
inter_left_comm [lemma, in Ch12_parallel]
inter_sym [lemma, in Ch12_parallel]
inter_trivial [lemma, in Ch12_parallel]
inter_unicity_not_par [lemma, in Ch12_parallel]
intuitionistic_Tarski_neutral_dimensionless [record, in tarski_axioms]
Intuitionistic_Tarski_to_Tarski [section, in tarski_to_beeson]
invert_one_side [lemma, in Ch09_plane]
invert_two_sides [lemma, in Ch09_plane]
in_angleH_trivial [lemma, in tarski_to_hilbert]
in_angleH_in_angle [lemma, in tarski_to_hilbert]
in_angle_equiv [lemma, in tarski_to_hilbert]
in_angle_reverse [lemma, in Ch11_angles]
in_angle_asym [lemma, in Ch11_angles]
in_angle_trans [lemma, in Ch11_angles]
in_angle_line [lemma, in Ch11_angles]
in_angle_trivial_2 [lemma, in Ch11_angles]
in_angle_trivial_1 [lemma, in Ch11_angles]
in_angle_one_side [lemma, in Ch11_angles]
in_angle_out [lemma, in Ch11_angles]
in_angle_two_sides [lemma, in Ch11_angles]
iota [definition, in Epsilon]
iota_rw [lemma, in Epsilon]
iota_fun_rw [lemma, in Epsilon]
iota_fun_ind [lemma, in Epsilon]
iota_fun_e [lemma, in Epsilon]
iota_fun [definition, in Epsilon]
iota_parameter_rw [lemma, in Epsilon]
iota_ind_weak [lemma, in Epsilon]
iota_ind [lemma, in Epsilon]
iota_e_weak [lemma, in Epsilon]
iota_e [lemma, in Epsilon]
Isegment_construction [projection, in tarski_axioms]
ise_to_is [lemma, in vectors]
isosceles [definition, in triangles]
isosceles_conga [lemma, in triangles]
isosceles_sym [lemma, in triangles]
is_gravity_center_exist_unique [lemma, in gravityCenter]
is_gravity_center [definition, in gravityCenter]
is_null_anga_dec [lemma, in Ch13_4_cos]
is_null_all [lemma, in Ch13_4_cos]
is_symmetric [definition, in Ch09_plane]
is_null_ang_out [lemma, in Ch13_3_angles]
is_null_anga_out [lemma, in Ch13_3_angles]
is_null_anga' [definition, in Ch13_3_angles]
is_null_anga [definition, in Ch13_3_angles]
is_flat_ang' [definition, in Ch13_3_angles]
is_null_ang' [definition, in Ch13_3_angles]
is_flat_ang [definition, in Ch13_3_angles]
is_null_ang [definition, in Ch13_3_angles]
is_anga_distinct [lemma, in Ch13_3_angles]
is_anga_conga_is_anga [lemma, in Ch13_3_angles]
is_anga_conga [lemma, in Ch13_3_angles]
is_anga_to_is_ang [lemma, in Ch13_3_angles]
is_anga [definition, in Ch13_3_angles]
is_ang_distinct [lemma, in Ch13_3_angles]
is_ang_conga_is_ang [lemma, in Ch13_3_angles]
is_ang_conga [lemma, in Ch13_3_angles]
is_ang [definition, in Ch13_3_angles]
is_len_cong_is_len [lemma, in Ch13_2_length]
is_len_cong [lemma, in Ch13_2_length]
is_len [definition, in Ch13_2_length]
is_circumcenter [definition, in circumcenter]
is_midpoint_id_2 [lemma, in Ch07_midpoint]
is_midpoint_id [lemma, in Ch07_midpoint]
is_midpoint_dec [lemma, in Ch07_midpoint]
is_midpoint [definition, in Ch07_midpoint]
is_orthocenter [definition, in orthocenter]
is_image_spec_dec [lemma, in Ch10_line_reflexivity]
is_image_spec_triv [lemma, in Ch10_line_reflexivity]
is_image_rev [lemma, in Ch10_line_reflexivity]
is_image_spec_rev [lemma, in Ch10_line_reflexivity]
is_image_spec_in_gen [definition, in Ch10_line_reflexivity]
is_image_spec_in [definition, in Ch10_line_reflexivity]
is_image_spec_col_cong [lemma, in Ch10_line_reflexivity]
is_image_col_cong [lemma, in Ch10_line_reflexivity]
is_image_is_image_spec [lemma, in Ch10_line_reflexivity]
is_image [definition, in Ch10_line_reflexivity]
is_image_spec [definition, in Ch10_line_reflexivity]
is_on_perp_bisect [definition, in perp_bisect]
is_to_ise [lemma, in vectors]
is_sum_exists [definition, in vectors]
is_sum [definition, in vectors]
ITpoint [projection, in tarski_axioms]
IT_to_T [instance, in tarski_to_beeson]
IT_trivial [lemma, in tarski_to_beeson]
IT_chara [lemma, in tarski_to_beeson]
K
ker_par [lemma, in project]ker_col [lemma, in project]
Kite [definition, in quadrilaterals]
Kite_comm [lemma, in quadrilaterals]
L
lastCP [definition, in arity]lastCPIn [lemma, in arity]
lastCPTl [lemma, in arity]
lastTailOK [lemma, in arity]
lcos [definition, in Ch13_4_cos]
lcos_lg [lemma, in Ch13_4_cos]
lcos_per [lemma, in Ch13_4_cos]
lcos_const_o [lemma, in Ch13_4_cos]
lcos_not_lg_null [lemma, in Ch13_4_cos]
lcos_eql_lcos [lemma, in Ch13_4_cos]
lcos_lg_anga [lemma, in Ch13_4_cos]
lcos_const_cb [lemma, in Ch13_4_cos]
lcos_const_ab [lemma, in Ch13_4_cos]
lcos_const_a [lemma, in Ch13_4_cos]
lcos_lg_distincts [lemma, in Ch13_4_cos]
lcos_const [lemma, in Ch13_4_cos]
lcos_const1 [lemma, in Ch13_4_cos]
lcos_const0 [lemma, in Ch13_4_cos]
lcos_lg_not_null [lemma, in Ch13_4_cos]
lcos_lcos_col [lemma, in Ch13_5_Pappus_Pascal]
lcos_per_anga [lemma, in Ch13_5_Pappus_Pascal]
lcos_eq_lcos3_eq [lemma, in Ch13_5_Pappus_Pascal]
lcos_eq_lcos2_eq [lemma, in Ch13_5_Pappus_Pascal]
lcos_eq_trans [lemma, in Ch13_5_Pappus_Pascal]
lcos_eq_sym [lemma, in Ch13_5_Pappus_Pascal]
lcos_eq_refl [lemma, in Ch13_5_Pappus_Pascal]
lcos_eq [definition, in Ch13_5_Pappus_Pascal]
lcos_exists [lemma, in Ch13_5_Pappus_Pascal]
lcos_eqa_lcos [lemma, in Ch13_5_Pappus_Pascal]
lcos2 [definition, in Ch13_5_Pappus_Pascal]
lcos2_lcos [lemma, in Ch13_5_Pappus_Pascal]
lcos2_eq_lcos3_eq [lemma, in Ch13_5_Pappus_Pascal]
lcos2_lg_not_null [lemma, in Ch13_5_Pappus_Pascal]
lcos2_eq_trans [lemma, in Ch13_5_Pappus_Pascal]
lcos2_lg_anga [lemma, in Ch13_5_Pappus_Pascal]
lcos2_eql_lcos2 [lemma, in Ch13_5_Pappus_Pascal]
lcos2_unicity [lemma, in Ch13_5_Pappus_Pascal]
lcos2_eq_sym [lemma, in Ch13_5_Pappus_Pascal]
lcos2_eq_refl [lemma, in Ch13_5_Pappus_Pascal]
lcos2_eq [definition, in Ch13_5_Pappus_Pascal]
lcos2_exists' [lemma, in Ch13_5_Pappus_Pascal]
lcos2_exists [lemma, in Ch13_5_Pappus_Pascal]
lcos2_comm [lemma, in Ch13_5_Pappus_Pascal]
lcos3 [definition, in Ch13_5_Pappus_Pascal]
lcos3_lcos2 [lemma, in Ch13_5_Pappus_Pascal]
lcos3_eq_trans [lemma, in Ch13_5_Pappus_Pascal]
lcos3_lg_not_null [lemma, in Ch13_5_Pappus_Pascal]
lcos3_lg_anga [lemma, in Ch13_5_Pappus_Pascal]
lcos3_eql_lcos3 [lemma, in Ch13_5_Pappus_Pascal]
lcos3_unicity [lemma, in Ch13_5_Pappus_Pascal]
lcos3_eq_sym [lemma, in Ch13_5_Pappus_Pascal]
lcos3_eq_refl [lemma, in Ch13_5_Pappus_Pascal]
lcos3_eq [definition, in Ch13_5_Pappus_Pascal]
lcos3_exists [lemma, in Ch13_5_Pappus_Pascal]
lcos3_permut2 [lemma, in Ch13_5_Pappus_Pascal]
lcos3_permut1 [lemma, in Ch13_5_Pappus_Pascal]
lcos3_permut3 [lemma, in Ch13_5_Pappus_Pascal]
lcos3_lcos_2_1 [lemma, in Ch13_5_Pappus_Pascal]
lcos3_lcos_1_2 [lemma, in Ch13_5_Pappus_Pascal]
le [definition, in Ch05_bet_le]
lea [definition, in Ch11_angles]
lea_cases [lemma, in Ch12_parallel_inter_dec]
lea_in_angle [lemma, in Ch13_1]
lea_acute_obtuse [lemma, in Ch11_angles]
lea_comm [lemma, in Ch11_angles]
lea_right_comm [lemma, in Ch11_angles]
lea_left_comm [lemma, in Ch11_angles]
lea_asym [lemma, in Ch11_angles]
lea_trans [lemma, in Ch11_angles]
lea_refl [lemma, in Ch11_angles]
lea_line [lemma, in Ch11_angles]
lengthOfCPToList [lemma, in arity]
_ =l= _ [notation, in Ch13_2_length]
Length_4 [section, in Ch13_2_length]
Length_3 [section, in Ch13_2_length]
Length_2 [section, in Ch13_2_length]
Length_1 [section, in Ch13_2_length]
le_cong_le [lemma, in orientation]
le_comm [lemma, in orientation]
le_right_comm [lemma, in orientation]
le_left_comm [lemma, in orientation]
le_bet [lemma, in Ch08_orthogonality]
le_cong_le [lemma, in quadrilaterals]
le_comm [lemma, in quadrilaterals]
le_right_comm [lemma, in quadrilaterals]
le_left_comm [lemma, in quadrilaterals]
le_comm [lemma, in Ch11_angles]
le_right_comm [lemma, in Ch11_angles]
le_left_comm [lemma, in Ch11_angles]
le_zero [lemma, in Ch05_bet_le]
le_cases [lemma, in Ch05_bet_le]
le_trivial [lemma, in Ch05_bet_le]
le_anti_symmetry [lemma, in Ch05_bet_le]
le_transitivity [lemma, in Ch05_bet_le]
le_reflexivity [lemma, in Ch05_bet_le]
lg [definition, in Ch13_2_length]
lg_null_dec [lemma, in Ch13_2_length]
lg_null_trivial [lemma, in Ch13_2_length]
lg_null_instance [lemma, in Ch13_2_length]
lg_null [definition, in Ch13_2_length]
lg_sym [lemma, in Ch13_2_length]
lg_cong_lg [lemma, in Ch13_2_length]
lg_cong [lemma, in Ch13_2_length]
lg_exists [lemma, in Ch13_2_length]
Lin [definition, in tarski_to_hilbert]
Line [definition, in tarski_to_hilbert]
Line [projection, in hilbert_axioms]
line_of_hline [definition, in tarski_to_hilbert]
line_of_hline [projection, in hilbert_axioms]
line_unicity [projection, in hilbert_axioms]
line_existence [projection, in hilbert_axioms]
line_dec [lemma, in Ch12_parallel]
link_betwenn_wd_and_coapp [projection, in tactics_axioms]
listInd [lemma, in arity]
ListToCP [definition, in arity]
ListToCPTl [lemma, in arity]
list_assoc_inv [definition, in ColR]
long [definition, in Ch13_2_length]
lower_dim [projection, in tarski_axioms]
lower_dim [lemma, in tarski_to_beeson]
lower_dim_B [lemma, in tarski_to_beeson]
lt [definition, in Ch05_bet_le]
lta [definition, in Ch11_angles]
ltac_something_show [lemma, in general_tactics]
ltac_something_hide [lemma, in general_tactics]
ltac_something_eq [lemma, in general_tactics]
ltac_something [definition, in general_tactics]
lta_diff [lemma, in Ch11_angles]
lta_not_conga [lemma, in Ch11_angles]
lta_comm [lemma, in Ch11_angles]
lta_right_comm [lemma, in Ch11_angles]
lta_left_comm [lemma, in Ch11_angles]
lta_trans [lemma, in Ch11_angles]
lt_comm [lemma, in Ch11_angles]
lt_left_comm [lemma, in Ch11_angles]
lt_right_comm [lemma, in Ch11_angles]
l_3_9_4 [lemma, in Ch03_bet]
l10_16 [lemma, in Ch10_line_reflexivity]
l10_15 [lemma, in Ch10_line_reflexivity]
l10_14 [lemma, in Ch10_line_reflexivity]
l10_12 [lemma, in Ch10_line_reflexivity]
l10_10 [lemma, in Ch10_line_reflexivity]
l10_10_spec [lemma, in Ch10_line_reflexivity]
l10_8 [lemma, in Ch10_line_reflexivity]
l10_7 [lemma, in Ch10_line_reflexivity]
l10_6_existence [lemma, in Ch10_line_reflexivity]
l10_6_existence_spec [lemma, in Ch10_line_reflexivity]
l10_6_unicity [lemma, in Ch10_line_reflexivity]
l10_5 [lemma, in Ch10_line_reflexivity]
l10_4 [lemma, in Ch10_line_reflexivity]
l10_4_spec [lemma, in Ch10_line_reflexivity]
l10_2_existence [lemma, in Ch10_line_reflexivity]
l10_2_existence_spec [lemma, in Ch10_line_reflexivity]
l10_2_unicity [lemma, in Ch10_line_reflexivity]
l11_53 [lemma, in Ch11_angles]
l11_52 [lemma, in Ch11_angles]
l11_51 [lemma, in Ch11_angles]
l11_50_2 [lemma, in Ch11_angles]
l11_50_1 [lemma, in Ch11_angles]
l11_49 [lemma, in Ch11_angles]
l11_47 [lemma, in Ch11_angles]
l11_46 [lemma, in Ch11_angles]
l11_44_2 [lemma, in Ch11_angles]
l11_44_1 [lemma, in Ch11_angles]
l11_44_2_b [lemma, in Ch11_angles]
l11_44_1_b [lemma, in Ch11_angles]
l11_44_2_a [lemma, in Ch11_angles]
l11_44_1_a [lemma, in Ch11_angles]
l11_43 [lemma, in Ch11_angles]
l11_43_aux [lemma, in Ch11_angles]
l11_41 [lemma, in Ch11_angles]
l11_41_aux [lemma, in Ch11_angles]
l11_36 [lemma, in Ch11_angles]
l11_31_2 [lemma, in Ch11_angles]
l11_31_1 [lemma, in Ch11_angles]
l11_30 [lemma, in Ch11_angles]
l11_29_b [lemma, in Ch11_angles]
l11_29_a [lemma, in Ch11_angles]
l11_28 [lemma, in Ch11_angles]
l11_25 [lemma, in Ch11_angles]
l11_25_aux [lemma, in Ch11_angles]
l11_24 [lemma, in Ch11_angles]
l11_22 [lemma, in Ch11_angles]
l11_22b [lemma, in Ch11_angles]
l11_22a [lemma, in Ch11_angles]
l11_22_bet [lemma, in Ch11_angles]
l11_19 [lemma, in Ch11_angles]
l11_15 [lemma, in Ch11_angles]
l11_22_aux [lemma, in Ch11_angles]
l11_21_b [lemma, in Ch11_angles]
l11_21_a [lemma, in Ch11_angles]
l11_18_2 [lemma, in Ch11_angles]
l11_18_1 [lemma, in Ch11_angles]
l11_17 [lemma, in Ch11_angles]
l11_16 [lemma, in Ch11_angles]
l11_14 [lemma, in Ch11_angles]
l11_13 [lemma, in Ch11_angles]
l11_10 [lemma, in Ch11_angles]
l11_4_2 [lemma, in Ch11_angles]
l11_4_1 [lemma, in Ch11_angles]
l11_3_bis [lemma, in Ch11_angles]
l11_aux [lemma, in Ch11_angles]
l11_3 [lemma, in Ch11_angles]
l12_23 [lemma, in Ch12_parallel_inter_dec]
l12_22 [lemma, in Ch12_parallel_inter_dec]
l12_22_a [lemma, in Ch12_parallel_inter_dec]
l12_21 [lemma, in Ch12_parallel_inter_dec]
l12_21_a [lemma, in Ch12_parallel_inter_dec]
l12_20 [lemma, in Ch12_parallel_inter_dec]
l12_20_bis [lemma, in Ch12_parallel_inter_dec]
l12_19 [lemma, in Ch12_parallel_inter_dec]
l12_16 [lemma, in Ch12_parallel_inter_dec]
l12_22_b [lemma, in Ch12_parallel]
l12_22_aux [lemma, in Ch12_parallel]
l12_21_b [lemma, in Ch12_parallel]
l12_18 [lemma, in Ch12_parallel]
l12_18_d [lemma, in Ch12_parallel]
l12_18_c [lemma, in Ch12_parallel]
l12_18_b [lemma, in Ch12_parallel]
l12_18_a [lemma, in Ch12_parallel]
l12_17 [lemma, in Ch12_parallel]
l12_9 [lemma, in Ch12_parallel]
l12_6 [lemma, in Ch12_parallel]
L13 [section, in Ch13_1]
l13_7 [lemma, in Ch13_4_cos]
l13_6 [lemma, in Ch13_4_cos]
l13_14 [lemma, in Ch13_5_Pappus_Pascal]
l13_11 [lemma, in Ch13_5_Pappus_Pascal]
l13_10 [lemma, in Ch13_5_Pappus_Pascal]
l13_10_aux5 [lemma, in Ch13_5_Pappus_Pascal]
l13_10_aux4 [lemma, in Ch13_5_Pappus_Pascal]
l13_10_aux3 [lemma, in Ch13_5_Pappus_Pascal]
l13_6_bis [lemma, in Ch13_5_Pappus_Pascal]
l13_10_aux2 [lemma, in Ch13_5_Pappus_Pascal]
l13_10_aux1 [lemma, in Ch13_5_Pappus_Pascal]
l13_19_par [lemma, in Ch13_6_Desargues_Hessenberg]
l13_19_par_aux [lemma, in Ch13_6_Desargues_Hessenberg]
l13_19 [lemma, in Ch13_6_Desargues_Hessenberg]
l13_19_aux [lemma, in Ch13_6_Desargues_Hessenberg]
l13_18 [lemma, in Ch13_6_Desargues_Hessenberg]
l13_18_3 [lemma, in Ch13_6_Desargues_Hessenberg]
l13_18_2 [lemma, in Ch13_6_Desargues_Hessenberg]
l13_15_par [lemma, in Ch13_6_Desargues_Hessenberg]
l13_15 [lemma, in Ch13_6_Desargues_Hessenberg]
l13_15_2 [lemma, in Ch13_6_Desargues_Hessenberg]
l13_15_2_aux [lemma, in Ch13_6_Desargues_Hessenberg]
l13_15_1 [lemma, in Ch13_6_Desargues_Hessenberg]
l13_8 [lemma, in Ch13_1]
l13_2 [lemma, in Ch13_1]
l13_2_1 [lemma, in Ch13_1]
l13_1 [lemma, in Ch13_1]
l2_11_b [lemma, in Ch03_bet]
l2_11 [lemma, in Ch02_cong]
l3_17 [lemma, in Ch03_bet]
l4_3_1 [lemma, in Ch08_orthogonality]
l4_19 [lemma, in Ch04_col]
l4_18 [lemma, in Ch04_col]
l4_17 [lemma, in Ch04_col]
l4_16 [lemma, in Ch04_col]
l4_14 [lemma, in Ch04_col]
l4_13 [lemma, in Ch04_col]
l4_6 [lemma, in Ch04_cong_bet]
l4_5 [lemma, in Ch04_cong_bet]
l4_3 [lemma, in Ch04_cong_bet]
l4_2 [lemma, in Ch04_cong_bet]
l5_12_b [lemma, in Ch11_angles]
l5_12_a [lemma, in Ch11_angles]
l5_6 [lemma, in Ch05_bet_le]
l5_5_2 [lemma, in Ch05_bet_le]
l5_5_1 [lemma, in Ch05_bet_le]
l5_3 [lemma, in Ch05_bet_le]
l5_2 [lemma, in Ch05_bet_le]
l5_1 [lemma, in Ch05_bet_le]
l6_25 [lemma, in Ch06_out_lines]
l6_21 [lemma, in Ch06_out_lines]
l6_16_1 [lemma, in Ch06_out_lines]
l6_13_2 [lemma, in Ch06_out_lines]
l6_13_1 [lemma, in Ch06_out_lines]
l6_11_existence [lemma, in Ch06_out_lines]
l6_11_unicity [lemma, in Ch06_out_lines]
l6_7 [lemma, in Ch06_out_lines]
l6_6 [lemma, in Ch06_out_lines]
l6_4_2 [lemma, in Ch06_out_lines]
l6_4_1 [lemma, in Ch06_out_lines]
l6_3_2 [lemma, in Ch06_out_lines]
l6_3_1 [lemma, in Ch06_out_lines]
l6_2 [lemma, in Ch06_out_lines]
l6_7_1 [lemma, in Ch12_parallel]
l7_25 [lemma, in Ch07_midpoint]
l7_22 [lemma, in Ch07_midpoint]
l7_22_aux [lemma, in Ch07_midpoint]
l7_21 [lemma, in Ch07_midpoint]
l7_20 [lemma, in Ch07_midpoint]
l7_17_bis [lemma, in Ch07_midpoint]
l7_17 [lemma, in Ch07_midpoint]
l7_16 [lemma, in Ch07_midpoint]
l7_15 [lemma, in Ch07_midpoint]
l7_13 [lemma, in Ch07_midpoint]
l7_9 [lemma, in Ch07_midpoint]
l7_3_2 [lemma, in Ch07_midpoint]
l7_3 [lemma, in Ch07_midpoint]
l7_2 [lemma, in Ch07_midpoint]
l8_24 [lemma, in Ch08_orthogonality]
l8_22_bis [lemma, in Ch08_orthogonality]
l8_22 [lemma, in Ch08_orthogonality]
l8_21 [lemma, in Ch08_orthogonality]
l8_21_aux [lemma, in Ch08_orthogonality]
l8_18_existence [lemma, in Ch08_orthogonality]
l8_20_2 [lemma, in Ch08_orthogonality]
l8_20_1 [lemma, in Ch08_orthogonality]
l8_18_unicity [lemma, in Ch08_orthogonality]
l8_16_2 [lemma, in Ch08_orthogonality]
l8_16_1 [lemma, in Ch08_orthogonality]
l8_15_2 [lemma, in Ch08_orthogonality]
l8_15_1 [lemma, in Ch08_orthogonality]
l8_14_3 [lemma, in Ch08_orthogonality]
l8_14_2_2 [lemma, in Ch08_orthogonality]
l8_14_2_1b_bis [lemma, in Ch08_orthogonality]
l8_14_2_1b [lemma, in Ch08_orthogonality]
l8_14_2_1a [lemma, in Ch08_orthogonality]
l8_14_1 [lemma, in Ch08_orthogonality]
l8_13_2 [lemma, in Ch08_orthogonality]
l8_12 [lemma, in Ch08_orthogonality]
l8_10 [lemma, in Ch08_orthogonality]
l8_9 [lemma, in Ch08_orthogonality]
l8_8 [lemma, in Ch08_orthogonality]
l8_7 [lemma, in Ch08_orthogonality]
l8_6 [lemma, in Ch08_orthogonality]
l8_5 [lemma, in Ch08_orthogonality]
l8_4 [lemma, in Ch08_orthogonality]
l8_3 [lemma, in Ch08_orthogonality]
l8_2 [lemma, in Ch08_orthogonality]
l9_19 [lemma, in Ch09_plane]
l9_18 [lemma, in Ch09_plane]
l9_17 [lemma, in Ch09_plane]
l9_10 [lemma, in Ch09_plane]
l9_9_bis [lemma, in Ch09_plane]
l9_9 [lemma, in Ch09_plane]
l9_8_2 [lemma, in Ch09_plane]
l9_8_1 [lemma, in Ch09_plane]
l9_5 [lemma, in Ch09_plane]
l9_4_2 [lemma, in Ch09_plane]
l9_4_2_aux [lemma, in Ch09_plane]
l9_4_1 [lemma, in Ch09_plane]
l9_4_1_aux [lemma, in Ch09_plane]
l9_3 [lemma, in Ch09_plane]
l9_2 [lemma, in Ch09_plane]
l9_31 [lemma, in Ch11_angles]
M
Makarios_variant_to_Tarski83 [section, in tarski_to_makarios]Makarios_Variant_follows_from_Tarski [instance, in tarski_to_makarios]
Mbetween_identity [projection, in tarski_axioms]
Mcong_left_commutativity [lemma, in tarski_to_makarios]
Mcong_symmetry [lemma, in tarski_to_makarios]
Mcong_reflexivity [lemma, in tarski_to_makarios]
Mcong_inner_transitivity [projection, in tarski_axioms]
Mcong_identity [projection, in tarski_axioms]
Mfive_segments [projection, in tarski_axioms]
midpoint_preserves_bet [lemma, in orientation]
midpoint_par_strict [lemma, in orientation]
midpoint_par [lemma, in orientation]
midpoint_col [lemma, in orientation]
midpoint_existence [lemma, in Ch08_orthogonality]
midpoint_existence_aux [lemma, in Ch08_orthogonality]
midpoint_cong_unicity [lemma, in quadrilaterals]
midpoint_preserves_bet [lemma, in quadrilaterals]
midpoint_par_strict [lemma, in quadrilaterals]
midpoint_par [lemma, in quadrilaterals]
midpoint_midpoint_col [lemma, in quadrilaterals]
midpoint_not_midpoint [lemma, in Ch07_midpoint]
midpoint_cong [lemma, in Ch07_midpoint]
midpoint_col [lemma, in Ch07_midpoint]
midpoint_bet [lemma, in Ch07_midpoint]
midpoint_def [lemma, in Ch07_midpoint]
midpoint_distinct_3 [lemma, in Ch07_midpoint]
midpoint_distinct_2 [lemma, in Ch07_midpoint]
midpoint_distinct_1 [lemma, in Ch07_midpoint]
midpoint_preserves_per [lemma, in Ch10_line_reflexivity]
midpoint_preserves_image [lemma, in Ch10_line_reflexivity]
midpoint_thales_reci [lemma, in midpoint_thales]
midpoint_thales [lemma, in midpoint_thales]
midpoint_preserves_out [lemma, in Ch12_parallel]
midpoint_thales [library]
Mid_tagged_Mid [lemma, in Tagged_predicates]
Mid_Mid_tagged [lemma, in Tagged_predicates]
Mid_tagged [definition, in Tagged_predicates]
mid_two_sides [lemma, in Ch09_plane]
mid_preserves_col [lemma, in Ch09_plane]
mid_plg_2 [lemma, in quadrilaterals]
mid_plg_1 [lemma, in quadrilaterals]
mid_plg [lemma, in quadrilaterals]
mid_plgf [lemma, in quadrilaterals]
mid_plgf_aux [lemma, in quadrilaterals]
mid_plgs [lemma, in quadrilaterals]
mid_par_cong [lemma, in quadrilaterals]
mid_par_cong2 [lemma, in quadrilaterals]
mid_par_cong1 [lemma, in quadrilaterals]
Mid_perm [lemma, in Ch07_midpoint]
Mid_cases [lemma, in Ch07_midpoint]
mid_eqv [lemma, in vectors]
Minner_pasch [projection, in tarski_axioms]
minus_n1_n2_0 [lemma, in arity]
minus_n_0 [lemma, in arity]
Mlower_dim [projection, in tarski_axioms]
Msegment_construction [projection, in tarski_axioms]
MTpoint [projection, in tarski_axioms]
N
n [projection, in tactics_axioms]NColB_NColOrEq [lemma, in tarski_to_beeson]
NColB_NDiffCol [lemma, in tarski_to_beeson]
NCol_tagged_NCol [lemma, in Tagged_predicates]
NCol_NCol_tagged [lemma, in Tagged_predicates]
NCol_tagged [definition, in Tagged_predicates]
NCol_perm [lemma, in Ch04_col]
NCol_cases [lemma, in Ch04_col]
ncol_conga_ncol [lemma, in Ch11_angles]
new_pair_2 [definition, in ColR]
new_pair_1 [definition, in ColR]
not_par_pars_not_cong [lemma, in quadrilaterals_inter_dec]
not_two_sides_id [lemma, in Ch09_plane]
not_null_not_col [lemma, in Ch13_3_angles]
not_null_anga [definition, in Ch13_3_angles]
not_flat_ang_def_equiv [lemma, in Ch13_3_angles]
not_null_ang_def_equiv [lemma, in Ch13_3_angles]
not_null_ang_ang [lemma, in Ch13_3_angles]
not_flat_ang' [definition, in Ch13_3_angles]
not_null_ang' [definition, in Ch13_3_angles]
not_flat_ang [definition, in Ch13_3_angles]
not_null_ang [definition, in Ch13_3_angles]
not_cong_is_anga1 [lemma, in Ch13_3_angles]
not_conga_is_anga [lemma, in Ch13_3_angles]
not_cong_is_ang1 [lemma, in Ch13_3_angles]
not_conga_is_ang [lemma, in Ch13_3_angles]
not_conga_not_ang [lemma, in Ch13_3_angles]
not_cong_is_len1 [lemma, in Ch13_2_length]
not_cong_is_len [lemma, in Ch13_2_length]
not_col_exists [lemma, in quadrilaterals]
not_col_sym_not_col [lemma, in quadrilaterals]
not_col_distincts [lemma, in Ch04_col]
not_col_permutation_5 [lemma, in Ch04_col]
not_col_permutation_4 [lemma, in Ch04_col]
not_col_permutation_3 [lemma, in Ch04_col]
not_col_permutation_2 [lemma, in Ch04_col]
not_col_permutation_1 [lemma, in Ch04_col]
not_col_par_col2_diff [lemma, in orthocenter]
not_par_one_not_par [lemma, in Ch12_parallel_inter_dec]
not_par_inter [lemma, in Ch12_parallel_inter_dec]
not_par_strict_inter_exists [lemma, in Ch12_parallel_inter_dec]
not_lta_gea [lemma, in Ch12_parallel_inter_dec]
not_one_side_two_sides [lemma, in Ch12_parallel_inter_dec]
not_par_other_side [lemma, in Ch12_parallel_inter_dec]
not_par_two_sides [lemma, in Ch12_parallel_inter_dec]
not_par_inter_exists [lemma, in Ch12_parallel_inter_dec]
not_col_exists [lemma, in Ch10_line_reflexivity]
not_lta_and_gta [lemma, in Ch11_angles]
not_gta_and_cong [lemma, in Ch11_angles]
not_lta_and_cong [lemma, in Ch11_angles]
not_and_lta [lemma, in Ch11_angles]
not_conga_sym [lemma, in Ch11_angles]
not_conga [lemma, in Ch11_angles]
not_two_sides_one_side [lemma, in Ch11_angles]
not_two_sides_one_side_aux [lemma, in Ch11_angles]
not_bet_and_out [lemma, in Ch11_angles]
not_out_bet [lemma, in Ch11_angles]
not_two_sides [lemma, in Ch11_angles]
not_bet_out [lemma, in Ch11_angles]
not_par_inter_unicity [lemma, in Ch12_parallel]
not_par_not_col [lemma, in Ch12_parallel]
not_strict_par [lemma, in Ch12_parallel]
not_strict_par2 [lemma, in Ch12_parallel]
not_strict_par1 [lemma, in Ch12_parallel]
not_par_strict_id [lemma, in Ch12_parallel]
nthCircPermNAny [lemma, in arity]
nthCircPerm1 [lemma, in arity]
nthCircPerm1Eq [lemma, in arity]
nthCircPerm2 [lemma, in arity]
nthCircPerm2Eq [lemma, in arity]
nthCP [definition, in arity]
nthCPTlOK [lemma, in arity]
nthCP01 [lemma, in arity]
nthEqOK [lemma, in arity]
nthFirst [lemma, in arity]
nthLast [lemma, in arity]
NT_NBet [lemma, in tarski_to_beeson]
null_lcos [lemma, in Ch13_4_cos]
null_lcos_eql [lemma, in Ch13_4_cos]
null_anga_null_anga' [lemma, in Ch13_3_angles]
null_anga [lemma, in Ch13_3_angles]
null_ang [lemma, in Ch13_3_angles]
null_len [lemma, in Ch13_2_length]
null_sum_eq [lemma, in vectors]
null_sum [lemma, in vectors]
null_vector [lemma, in vectors]
O
obtuse [definition, in Ch11_angles]obtuse_not_acute [lemma, in Ch13_4_cos]
obtuse_gea_obtuse [lemma, in Ch11_angles]
obtuse_sym [lemma, in Ch11_angles]
OCP [definition, in sets]
OCPALengthOK [lemma, in sets]
OCPAux [definition, in sets]
OCPIdempotent [lemma, in sets]
OCPOK [lemma, in sets]
OCPPerm [lemma, in sets]
OCPSortedAux [lemma, in sets]
OCPSortedTl [lemma, in sets]
OCPTlOK [lemma, in sets]
OFSC [definition, in Ch02_cong]
one_side_eqo [lemma, in orientation]
one_side_eq_o [lemma, in orientation]
one_side_same_side [lemma, in tarski_to_hilbert]
one_side_transitivity [lemma, in Ch09_plane]
one_side_symmetry [lemma, in Ch09_plane]
one_side_reflexivity [lemma, in Ch09_plane]
one_side_chara [lemma, in Ch09_plane]
one_side [definition, in Ch09_plane]
one_side_dec [lemma, in Ch12_parallel_inter_dec]
one_or_two_sides [lemma, in Ch12_parallel_inter_dec]
one_side_not_col [lemma, in Ch11_angles]
one_side_col_out [lemma, in vectors]
opposite_sum [lemma, in vectors]
opp_not_same_dir [lemma, in vectors]
opp_dir_to_null [lemma, in vectors]
opp_dir_id [lemma, in vectors]
opp_dir [definition, in vectors]
orientation [library]
Orthocenter [section, in orthocenter]
orthocenter [library]
or_to_sumbool [lemma, in Epsilon]
or_lta_conga_gta [lemma, in Ch12_parallel_inter_dec]
or_lt_cong_gt [lemma, in Ch11_angles]
or_bet_out [lemma, in Ch11_angles]
osym_not_col [lemma, in Ch10_line_reflexivity]
os_cong_par_cong_par [lemma, in quadrilaterals_inter_dec]
os_out_os [lemma, in Ch13_1]
other_point_exists [lemma, in Ch12_parallel]
out [definition, in Ch06_out_lines]
outer_transitivity_between [lemma, in Ch03_bet]
outer_transitivity_between2 [lemma, in Ch03_bet]
outer_pasch [lemma, in Ch09_plane]
outH [definition, in tarski_to_hilbert]
outH_in_angleH_colH [lemma, in tarski_to_hilbert]
outH_out [lemma, in tarski_to_hilbert]
out_preserves_eqo [lemma, in orientation]
out_preserves_eqo1 [lemma, in orientation]
out_preserves_eq_o [lemma, in orientation]
out_trivial [lemma, in Ch06_out_lines]
out_col [lemma, in Ch06_out_lines]
out_distinct [lemma, in Ch06_out_lines]
out_diff2 [lemma, in Ch06_out_lines]
out_diff1 [lemma, in Ch06_out_lines]
out_dec [lemma, in Ch06_out_lines]
out_outH [lemma, in tarski_to_hilbert]
out_acute [lemma, in Ch13_4_cos]
out_out_anga [lemma, in Ch13_4_cos]
out_out_two_sides [lemma, in Ch09_plane]
out_null_anga [lemma, in Ch13_3_angles]
out_null_ang [lemma, in Ch13_3_angles]
out_len_eq [lemma, in Ch13_3_angles]
out_is_len_eq [lemma, in Ch13_3_angles]
out_two_sides_two_sides [lemma, in Ch11_angles]
out_bet_out_2 [lemma, in Ch11_angles]
out_bet_out_1 [lemma, in Ch11_angles]
out_one_side [lemma, in Ch11_angles]
out_conga_out [lemma, in Ch11_angles]
out_out_one_side [lemma, in Ch11_angles]
out_in_angle_out [lemma, in Ch11_angles]
out_in_angle [lemma, in Ch11_angles]
out_to_bet [lemma, in Ch11_angles]
out_conga [lemma, in Ch11_angles]
out_cong_cong [lemma, in Ch11_angles]
out_one_side_1 [lemma, in Ch12_parallel]
out2_bet_out [lemma, in Ch06_out_lines]
out2_out_2 [lemma, in Ch11_angles]
out2_out_1 [lemma, in Ch11_angles]
P
Pappus_Pascal [section, in Ch13_5_Pappus_Pascal]Par [definition, in Ch12_parallel]
Para [definition, in tarski_to_hilbert]
Parallelogram [definition, in quadrilaterals]
parallelogram_strict_midpoint [lemma, in quadrilaterals_inter_dec]
parallelogram_strict_not_col_4 [lemma, in quadrilaterals_inter_dec]
parallelogram_strict_not_col_3 [lemma, in quadrilaterals_inter_dec]
parallelogram_strict_not_col_2 [lemma, in quadrilaterals_inter_dec]
parallelogram_equiv_plg [lemma, in quadrilaterals_inter_dec]
parallelogram_to_plg [lemma, in quadrilaterals_inter_dec]
parallelogram_strict_not_col [lemma, in quadrilaterals]
Parallelogram_strict_Parallelogram [lemma, in quadrilaterals]
Parallelogram_flat [definition, in quadrilaterals]
Parallelogram_strict [definition, in quadrilaterals]
parallel_2_plg [lemma, in quadrilaterals_inter_dec]
parallel_existence1 [lemma, in Ch12_parallel_inter_dec]
parallel_trans [lemma, in Ch12_parallel_inter_dec]
parallel_unicity [lemma, in Ch12_parallel_inter_dec]
parallel_unicity_aux [lemma, in Ch12_parallel_inter_dec]
parallel_existence_spec [lemma, in Ch12_parallel]
parallel_existence [lemma, in Ch12_parallel]
Para_Par [lemma, in tarski_to_hilbert]
pars_par_plg [lemma, in quadrilaterals_inter_dec]
pars_par_pars [lemma, in quadrilaterals_inter_dec]
partition_sp_2 [definition, in ColR]
partition_sp_1 [definition, in ColR]
partition_ss [definition, in ColR]
par_col [lemma, in orientation]
par_cong_mid [lemma, in orientation]
par_strict_trans [lemma, in quadrilaterals_inter_dec]
par_cong3_rect [lemma, in quadrilaterals_inter_dec]
par_cong_plg_2 [lemma, in quadrilaterals_inter_dec]
par_cong_plg [lemma, in quadrilaterals_inter_dec]
par_cong_cong [lemma, in quadrilaterals_inter_dec]
par_perp_perp [lemma, in quadrilaterals_inter_dec]
par_2_plg [lemma, in quadrilaterals_inter_dec]
par_preserves_conga_os [lemma, in quadrilaterals_inter_dec]
par_preserves_conga_ts [lemma, in quadrilaterals_inter_dec]
par_cong_mid [lemma, in quadrilaterals_inter_dec]
par_strict_cong_mid1 [lemma, in quadrilaterals_inter_dec]
par_strict_cong_mid [lemma, in quadrilaterals_inter_dec]
par_cong_mid_os [lemma, in quadrilaterals_inter_dec]
par_cong_mid_ts [lemma, in quadrilaterals_inter_dec]
Par_tagged_Par [lemma, in Tagged_predicates]
Par_Par_tagged [lemma, in Tagged_predicates]
Par_tagged [definition, in Tagged_predicates]
Par_strict_tagged_Par_strict [lemma, in Tagged_predicates]
Par_strict_Par_strict_tagged [lemma, in Tagged_predicates]
Par_strict_tagged [definition, in Tagged_predicates]
par_col_project [lemma, in project]
par_strict_not_col [lemma, in Ch12_parallel_inter_dec]
par_one_or_two_sides [lemma, in Ch12_parallel_inter_dec]
par_inter [lemma, in Ch12_parallel_inter_dec]
par_not_par [lemma, in Ch12_parallel_inter_dec]
Par_dec [lemma, in Ch12_parallel_inter_dec]
par_strict_all_one_side [lemma, in Ch12_parallel_inter_dec]
par_strict_one_side [lemma, in Ch12_parallel_inter_dec]
par_trans [lemma, in Ch12_parallel_inter_dec]
par_perp2 [lemma, in Ch13_1]
par_ts_same_dir [lemma, in vectors]
par_strict_distinct [lemma, in Ch12_parallel]
par_strict_par [lemma, in Ch12_parallel]
par_two_sides_two_sides [lemma, in Ch12_parallel]
par_distinct [lemma, in Ch12_parallel]
par_strict_col2_par_strict [lemma, in Ch12_parallel]
par_strict_col_par_strict [lemma, in Ch12_parallel]
par_col2_par [lemma, in Ch12_parallel]
par_col_par_2 [lemma, in Ch12_parallel]
par_not_col_strict [lemma, in Ch12_parallel]
par_distincts [lemma, in Ch12_parallel]
par_not_col [lemma, in Ch12_parallel]
par_col_par [lemma, in Ch12_parallel]
Par_strict_perm [lemma, in Ch12_parallel]
Par_strict_cases [lemma, in Ch12_parallel]
Par_perm [lemma, in Ch12_parallel]
Par_cases [lemma, in Ch12_parallel]
par_strict_comm [lemma, in Ch12_parallel]
par_strict_right_comm [lemma, in Ch12_parallel]
par_strict_left_comm [lemma, in Ch12_parallel]
par_comm [lemma, in Ch12_parallel]
par_right_comm [lemma, in Ch12_parallel]
par_left_comm [lemma, in Ch12_parallel]
par_symmetry [lemma, in Ch12_parallel]
par_strict_symmetry [lemma, in Ch12_parallel]
par_id_5 [lemma, in Ch12_parallel]
par_id_4 [lemma, in Ch12_parallel]
par_id_3 [lemma, in Ch12_parallel]
par_id_2 [lemma, in Ch12_parallel]
par_id_1 [lemma, in Ch12_parallel]
par_strict_not_col_4 [lemma, in Ch12_parallel]
par_strict_not_col_3 [lemma, in Ch12_parallel]
par_strict_not_col_2 [lemma, in Ch12_parallel]
par_strict_not_col_1 [lemma, in Ch12_parallel]
par_id [lemma, in Ch12_parallel]
par_strict_irreflexivity [lemma, in Ch12_parallel]
par_reflexivity [lemma, in Ch12_parallel]
Par_strict [definition, in Ch12_parallel]
par3_conga3 [lemma, in project]
pasch [lemma, in tarski_to_beeson]
pasch [projection, in hilbert_axioms]
pasch_col_case [lemma, in tarski_to_beeson]
Per [definition, in Ch08_orthogonality]
perBAB [lemma, in Ch08_orthogonality]
PermCoappOK [lemma, in Permutations]
PermOK [lemma, in arity]
PermOKAux [lemma, in arity]
PermSorted [lemma, in sets]
Permutations [section, in Permutations]
Permutations [library]
PermWdOK [lemma, in Permutations]
Perp [definition, in Ch08_orthogonality]
PerpBisect_3 [section, in perp_bisect]
PerpBisect_2 [section, in perp_bisect]
PerpBisect_1 [section, in perp_bisect]
perp_not_eq_3 [lemma, in orientation]
perp_3_rect [lemma, in quadrilaterals_inter_dec]
perp_3_perp [lemma, in quadrilaterals_inter_dec]
perp_rmb [lemma, in quadrilaterals_inter_dec]
Perp_tagged_Perp [lemma, in Tagged_predicates]
Perp_Perp_tagged [lemma, in Tagged_predicates]
Perp_tagged [definition, in Tagged_predicates]
Perp_in_tagged_Perp_in [lemma, in Tagged_predicates]
Perp_in_Perp_in_tagged [lemma, in Tagged_predicates]
Perp_in_tagged [definition, in Tagged_predicates]
perp_projp [lemma, in project]
perp_vector [lemma, in project]
perp_acute [lemma, in Ch13_4_cos]
perp_bet_obtuse [lemma, in Ch13_4_cos]
perp_obtuse_bet [lemma, in Ch13_4_cos]
perp_out__acute [lemma, in Ch13_4_cos]
perp_out_acute [lemma, in Ch13_4_cos]
perp_acute_out [lemma, in Ch13_4_cos]
perp_col2 [lemma, in Ch09_plane]
perp_in_perp [lemma, in Ch09_plane]
perp_in_col_perp_in [lemma, in Ch08_orthogonality]
perp_not_col2 [lemma, in Ch08_orthogonality]
perp_proj [lemma, in Ch08_orthogonality]
perp_in_perp [lemma, in Ch08_orthogonality]
perp_in_id [lemma, in Ch08_orthogonality]
perp_cong [lemma, in Ch08_orthogonality]
perp_not_eq_2 [lemma, in Ch08_orthogonality]
perp_not_eq_1 [lemma, in Ch08_orthogonality]
perp_col2 [lemma, in Ch08_orthogonality]
perp_col [lemma, in Ch08_orthogonality]
perp_per_2 [lemma, in Ch08_orthogonality]
perp_per_1 [lemma, in Ch08_orthogonality]
perp_perp_in [lemma, in Ch08_orthogonality]
perp_in_col [lemma, in Ch08_orthogonality]
perp_col1 [lemma, in Ch08_orthogonality]
Perp_in_perm [lemma, in Ch08_orthogonality]
Perp_in_cases [lemma, in Ch08_orthogonality]
Perp_perm [lemma, in Ch08_orthogonality]
Perp_cases [lemma, in Ch08_orthogonality]
perp_in_comm [lemma, in Ch08_orthogonality]
perp_in_right_comm [lemma, in Ch08_orthogonality]
perp_in_left_comm [lemma, in Ch08_orthogonality]
perp_in_sym [lemma, in Ch08_orthogonality]
perp_comm [lemma, in Ch08_orthogonality]
perp_right_comm [lemma, in Ch08_orthogonality]
perp_left_comm [lemma, in Ch08_orthogonality]
perp_col0 [lemma, in Ch08_orthogonality]
perp_sym [lemma, in Ch08_orthogonality]
perp_in_per [lemma, in Ch08_orthogonality]
perp_in_distinct [lemma, in Ch08_orthogonality]
perp_distinct [lemma, in Ch08_orthogonality]
Perp_in_dec [lemma, in Ch08_orthogonality]
Perp_in [definition, in Ch08_orthogonality]
perp_inter_perp_in [lemma, in Ch12_parallel_inter_dec]
perp_inter_exists [lemma, in Ch12_parallel_inter_dec]
perp_exists [lemma, in Ch10_line_reflexivity]
perp_not_col [lemma, in Ch10_line_reflexivity]
perp_mid_perp_bisect [lemma, in perp_bisect]
perp_bisect_is_on_perp_bisect [lemma, in perp_bisect]
perp_bisect_conc [lemma, in perp_bisect]
perp_bisect_cong [lemma, in perp_bisect]
perp_bisect_cong_2 [lemma, in perp_bisect]
perp_bisect_cong_1 [lemma, in perp_bisect]
perp_bisect_perp [lemma, in perp_bisect]
perp_in_per_4 [lemma, in perp_bisect]
perp_in_per_3 [lemma, in perp_bisect]
perp_in_per_2 [lemma, in perp_bisect]
perp_in_per_1 [lemma, in perp_bisect]
perp_bisect_sym_3 [lemma, in perp_bisect]
perp_bisect_sym_2 [lemma, in perp_bisect]
perp_bisect_sym_1 [lemma, in perp_bisect]
perp_bisect [definition, in perp_bisect]
perp_vector1 [lemma, in Ch13_1]
perp_not_par [lemma, in Ch12_parallel]
perp_perp_col_col [lemma, in Ch12_parallel]
Perp_dec [lemma, in Ch12_parallel]
perp_perp_col [lemma, in Ch12_parallel]
perp_bisect [library]
Perp2 [definition, in Ch13_1]
perp2_preserves_bet1 [lemma, in Ch13_4_cos]
perp2_perp_in [lemma, in Ch13_1]
perp2_preserves_bet [lemma, in Ch13_1]
perp2_par [lemma, in Ch13_1]
perp2_trans [lemma, in Ch13_1]
perp2_comm [lemma, in Ch13_1]
perp2_right_comm [lemma, in Ch13_1]
perp2_left_comm [lemma, in Ch13_1]
perp2_sym [lemma, in Ch13_1]
perp2_refl [lemma, in Ch13_1]
per_one_side [lemma, in orientation]
per_preserves_bet [lemma, in orientation]
per_diff [lemma, in orientation]
per_preserves_bet_aux2 [lemma, in orientation]
per_preserves_bet_aux1 [lemma, in orientation]
per_id [lemma, in orientation]
per_proj [lemma, in orientation]
per_rmb [lemma, in quadrilaterals_inter_dec]
Per_tagged_Per [lemma, in Tagged_predicates]
Per_Per_tagged [lemma, in Tagged_predicates]
Per_tagged [definition, in Tagged_predicates]
per_col_eq [lemma, in Ch09_plane]
per_mid_per [lemma, in Ch09_plane]
per_per_perp [lemma, in Ch13_5_Pappus_Pascal]
per_cong [lemma, in Ch08_orthogonality]
per_not_col [lemma, in Ch08_orthogonality]
per_not_colp [lemma, in Ch08_orthogonality]
per_perp [lemma, in Ch08_orthogonality]
per_perp_in [lemma, in Ch08_orthogonality]
per_col [lemma, in Ch08_orthogonality]
Per_perm [lemma, in Ch08_orthogonality]
Per_cases [lemma, in Ch08_orthogonality]
Per_dec [lemma, in Ch08_orthogonality]
per_per_cong_gen [lemma, in Ch10_line_reflexivity_2D]
per_per_cong [lemma, in Ch10_line_reflexivity_2D]
per_per_cong_1 [lemma, in Ch10_line_reflexivity_2D]
Per_mid_rectangle [lemma, in exercises]
per_double_cong [lemma, in Ch10_line_reflexivity]
per_per_perp [lemma, in Ch10_line_reflexivity]
per_per_col [lemma, in Ch10_line_reflexivity]
per_lt [lemma, in Ch13_1]
per_cong_mid [lemma, in Ch11_angles]
plan [projection, in hilbert_axioms]
Plg [definition, in quadrilaterals]
plgf_plgf_plgf [lemma, in quadrilaterals_inter_dec]
plgf_plgs_trans [lemma, in quadrilaterals_inter_dec]
plgf_rect_id [lemma, in quadrilaterals_inter_dec]
plgf_comm2 [lemma, in quadrilaterals_inter_dec]
plgf_bet [lemma, in quadrilaterals]
plgf_trivial [lemma, in quadrilaterals]
plgf_trivial_trans [lemma, in quadrilaterals]
plgf_trivial_neq [lemma, in quadrilaterals]
plgf_not_point [lemma, in quadrilaterals]
plgf_trivial2 [lemma, in quadrilaterals]
plgf_trivial1 [lemma, in quadrilaterals]
plgf_cong [lemma, in quadrilaterals]
plgf_not_comm [lemma, in quadrilaterals]
plgf_mid [lemma, in quadrilaterals]
plgf_irreflexive [lemma, in quadrilaterals]
plgf_sym [lemma, in quadrilaterals]
plgf_permut [lemma, in quadrilaterals]
plgf_out_plgf [lemma, in vectors]
plgf_plgf_bet [lemma, in vectors]
plgf3_mid [lemma, in quadrilaterals]
plgs_in_angle [lemma, in quadrilaterals_inter_dec]
plgs_pseudo_trans [lemma, in quadrilaterals_inter_dec]
plgs_trans_trivial [lemma, in quadrilaterals_inter_dec]
plgs_pars_2 [lemma, in quadrilaterals_inter_dec]
plgs_pars_1 [lemma, in quadrilaterals_inter_dec]
plgs_cong_2 [lemma, in quadrilaterals_inter_dec]
plgs_cong_1 [lemma, in quadrilaterals_inter_dec]
plgs_half_plgs [lemma, in quadrilaterals_inter_dec]
plgs_comm2 [lemma, in quadrilaterals_inter_dec]
plgs_half_plgs_aux [lemma, in quadrilaterals_inter_dec]
plgs_par_strict [lemma, in quadrilaterals_inter_dec]
plgs_two_sides [lemma, in quadrilaterals_inter_dec]
plgs_not_comm [lemma, in quadrilaterals_inter_dec]
plgs_mid [lemma, in quadrilaterals_inter_dec]
plgs_sym [lemma, in quadrilaterals_inter_dec]
plgs_permut [lemma, in quadrilaterals_inter_dec]
plgs_cong [lemma, in quadrilaterals_inter_dec]
plgs_existence [lemma, in quadrilaterals]
plgs_diff [lemma, in quadrilaterals]
plgs_not_col [lemma, in quadrilaterals]
plgs_one_side [lemma, in quadrilaterals]
plgs_irreflexive [lemma, in quadrilaterals]
plgs_plgs_bet [lemma, in vectors]
plgs_out_plgs [lemma, in vectors]
plg_pseudo_trans [lemma, in quadrilaterals_inter_dec]
plg_unicity [lemma, in quadrilaterals_inter_dec]
plg_par_2 [lemma, in quadrilaterals_inter_dec]
plg_par_1 [lemma, in quadrilaterals_inter_dec]
plg_par [lemma, in quadrilaterals_inter_dec]
plg_per_rect [lemma, in quadrilaterals_inter_dec]
plg_per_rect4 [lemma, in quadrilaterals_inter_dec]
plg_per_rect3 [lemma, in quadrilaterals_inter_dec]
plg_per_rect2 [lemma, in quadrilaterals_inter_dec]
plg_per_rect1 [lemma, in quadrilaterals_inter_dec]
plg_not_comm_2 [lemma, in quadrilaterals_inter_dec]
plg_not_comm_1 [lemma, in quadrilaterals_inter_dec]
Plg_perm [lemma, in quadrilaterals_inter_dec]
plg_cong_2 [lemma, in quadrilaterals_inter_dec]
plg_cong_1 [lemma, in quadrilaterals_inter_dec]
plg_comm2 [lemma, in quadrilaterals_inter_dec]
plg_conga [lemma, in quadrilaterals_inter_dec]
plg_not_comm [lemma, in quadrilaterals_inter_dec]
plg_mid [lemma, in quadrilaterals_inter_dec]
plg_sym [lemma, in quadrilaterals_inter_dec]
plg_permut [lemma, in quadrilaterals_inter_dec]
plg_conga1 [lemma, in quadrilaterals_inter_dec]
plg_cong [lemma, in quadrilaterals_inter_dec]
Plg_tagged_Plg [lemma, in Tagged_predicates]
Plg_Plg_tagged [lemma, in Tagged_predicates]
Plg_tagged [definition, in Tagged_predicates]
plg_existence [lemma, in quadrilaterals]
plg_bet1 [lemma, in quadrilaterals]
plg_col_plgf [lemma, in quadrilaterals]
plg_trivial1 [lemma, in quadrilaterals]
plg_trivial [lemma, in quadrilaterals]
plg_cong_rectangle [lemma, in quadrilaterals]
plg_to_parallelogram [lemma, in quadrilaterals]
plg_irreflexive [lemma, in quadrilaterals]
plg_opp_dir [lemma, in vectors]
plg_out_plg [lemma, in vectors]
plg_plg_bet [lemma, in vectors]
plus_n_1 [lemma, in arity]
plus_n_0 [lemma, in arity]
plus_0_n [lemma, in arity]
Point [projection, in hilbert_axioms]
point_construction_different [lemma, in Ch03_bet]
positive_dec [lemma, in ColR]
PosOrder [module, in sets]
PosOrder.leb [definition, in sets]
PosOrder.leb_dec [lemma, in sets]
PosOrder.leb_total [lemma, in sets]
PosOrder.t [definition, in sets]
PosSort [module, in sets]
Pred [projection, in aux]
proj [definition, in orientation]
project [definition, in project]
project [library]
Projections [section, in project]
project_project_par [lemma, in project]
project_par_project [lemma, in project]
project_to_projp [lemma, in project]
project_preserves_eqv [lemma, in project]
project_idem [lemma, in project]
project_par_dir [lemma, in project]
project_par_eqv [lemma, in project]
project_preserves_bet [lemma, in project]
project_col_eq [lemma, in project]
project_existence [lemma, in project]
project_unicity [lemma, in project]
project_par [lemma, in project]
project_not_col [lemma, in project]
project_col [lemma, in project]
project_not_id [lemma, in project]
project_id [lemma, in project]
projp [definition, in project]
projp_idem [lemma, in project]
projp_preserves_eqv [lemma, in project]
projp_preserves_bet [lemma, in project]
projp_id [lemma, in project]
projp_project_to_perp [lemma, in project]
projp_to_project [lemma, in project]
projp_is_project_perp [lemma, in project]
projp_is_project [lemma, in project]
proj_preserves_bet [lemma, in orientation]
proj_preserves_bet1 [lemma, in orientation]
proj_diff_not_col_inv [lemma, in orientation]
proj_diff_not_col [lemma, in orientation]
proj_perp_id [lemma, in orientation]
proj_inv_exists [lemma, in orientation]
proj_diff [lemma, in orientation]
proj_id [lemma, in orientation]
proj_par_strict [lemma, in orientation]
proj_not_eq_not_col [lemma, in orientation]
proj_not_eq [lemma, in orientation]
proj_comm [lemma, in orientation]
proj_not_col [lemma, in orientation]
proj_par [lemma, in orientation]
proj_eq_col [lemma, in orientation]
proj_one_side [lemma, in orientation]
proj_col_proj [lemma, in orientation]
proj_col [lemma, in orientation]
proj_unicity [lemma, in orientation]
proj_per [lemma, in orientation]
proj_exists [lemma, in orientation]
proj_distinct [lemma, in project]
proj3_id [lemma, in orientation]
proj3_col [lemma, in orientation]
Proof_of_eq_stability_in_IT [section, in tarski_to_beeson]
proper_9 [lemma, in ColR]
proper_8 [lemma, in ColR]
proper_7 [lemma, in ColR]
proper_6 [lemma, in ColR]
proper_5 [lemma, in ColR]
proper_4 [lemma, in ColR]
proper_3 [lemma, in ColR]
proper_2 [lemma, in ColR]
proper_1 [lemma, in ColR]
proper_0 [lemma, in ColR]
proper_00 [lemma, in ColR]
pseudo_trans [lemma, in tarski_to_coapp_theory]
pseudo_trans_of_coapp [projection, in tactics_axioms]
P1 [projection, in aux]
P2 [projection, in aux]
Q
Quadrilateral [section, in quadrilaterals]quadrilaterals [library]
quadrilaterals_inter_dec [library]
Quadrilateral_inter_dec_3 [section, in quadrilaterals_inter_dec]
Quadrilateral_inter_dec_2 [section, in quadrilaterals_inter_dec]
Quadrilateral_inter_dec_1 [section, in quadrilaterals_inter_dec]
quasi_classic [lemma, in Epsilon]
R
Rectangle [definition, in quadrilaterals]Rectangle_not_triv_2 [lemma, in quadrilaterals]
Rectangle_triv [lemma, in quadrilaterals]
Rectangle_not_triv [lemma, in quadrilaterals]
Rectangle_Parallelogram [lemma, in quadrilaterals]
Rectangle_Plg [lemma, in quadrilaterals]
rect_per [lemma, in quadrilaterals_inter_dec]
rect_per4 [lemma, in quadrilaterals_inter_dec]
rect_per3 [lemma, in quadrilaterals_inter_dec]
rect_per2 [lemma, in quadrilaterals_inter_dec]
rect_per1 [lemma, in quadrilaterals_inter_dec]
rect_comm2 [lemma, in quadrilaterals_inter_dec]
rect_permut [lemma, in quadrilaterals_inter_dec]
restricted_epsilon_extensionality [definition, in Epsilon]
Rhombus [definition, in quadrilaterals]
rhombus_cong_square [lemma, in quadrilaterals]
Rhombus_Rectangle_Square [lemma, in quadrilaterals]
Rhombus_Plg [lemma, in quadrilaterals]
rmb_perp [lemma, in quadrilaterals_inter_dec]
rmb_per [lemma, in quadrilaterals_inter_dec]
rmb_cong [lemma, in quadrilaterals_inter_dec]
S
S [module, in sets]same_side_sym [lemma, in tarski_to_hilbert]
same_side_trans [lemma, in tarski_to_hilbert]
same_side_one_side [lemma, in tarski_to_hilbert]
same_side [definition, in tarski_to_hilbert]
same_side_scott [definition, in tarski_to_hilbert]
same_not_opp_dir [lemma, in vectors]
same_dir_to_null [lemma, in vectors]
same_dir_id [lemma, in vectors]
same_or_opp_dir [lemma, in vectors]
same_dir_dec [lemma, in vectors]
same_dir_comm [lemma, in vectors]
same_dir_trans [lemma, in vectors]
same_dir_sym [lemma, in vectors]
same_dir_null [lemma, in vectors]
same_dir_out1 [lemma, in vectors]
same_dir_out [lemma, in vectors]
same_dir_ts [lemma, in vectors]
same_dir_refl [lemma, in vectors]
same_dir [definition, in vectors]
segment_construction [projection, in tarski_axioms]
segment_construction [lemma, in tarski_to_beeson]
segment_construction_B [lemma, in tarski_to_beeson]
segment_construction_0 [lemma, in Ch11_angles]
segment_construction_3 [lemma, in Ch11_angles]
segment_construction_2 [lemma, in Ch05_bet_le]
select [definition, in Epsilon]
select_the_rw [lemma, in Epsilon]
select_the_ind [lemma, in Epsilon]
select_the_e [lemma, in Epsilon]
select_ind [lemma, in Epsilon]
select_e [lemma, in Epsilon]
select_the [definition, in Epsilon]
SetOfPairsOfPositiveOrderedType [module, in sets]
SetOfPairsOfPositiveOrderedType.compare [definition, in sets]
SetOfPairsOfPositiveOrderedType.compare_spec [lemma, in sets]
SetOfPairsOfPositiveOrderedType.eq [definition, in sets]
SetOfPairsOfPositiveOrderedType.eqb [definition, in sets]
SetOfPairsOfPositiveOrderedType.eqb_eq [lemma, in sets]
SetOfPairsOfPositiveOrderedType.lt [definition, in sets]
SetOfPairsOfPositiveOrderedType.lt_strorder [instance, in sets]
SetOfPairsOfPositiveOrderedType.lt_compat [instance, in sets]
SetOfPairsOfPositiveOrderedType.lt_trans [lemma, in sets]
SetOfPairsOfPositiveOrderedType.lt_antiref [lemma, in sets]
SetOfPairsOfPositiveOrderedType.lt_irrefl [lemma, in sets]
SetOfPairsOfPositiveOrderedType.t [definition, in sets]
SetOfSetsOfPositiveOrderedType [module, in sets]
SetOfSetsOfPositiveOrderedType.compare [definition, in sets]
SetOfSetsOfPositiveOrderedType.compare_spec [definition, in sets]
SetOfSetsOfPositiveOrderedType.eq [definition, in sets]
SetOfSetsOfPositiveOrderedType.eqb [definition, in sets]
SetOfSetsOfPositiveOrderedType.eqb_eq [definition, in sets]
SetOfSetsOfPositiveOrderedType.lt [definition, in sets]
SetOfSetsOfPositiveOrderedType.lt_strorder [instance, in sets]
SetOfSetsOfPositiveOrderedType.lt_compat [instance, in sets]
SetOfSetsOfPositiveOrderedType.t [definition, in sets]
SetOfTuplesOfPositiveOrderedType [module, in sets]
SetOfTuplesOfPositiveOrderedType.compare [definition, in sets]
SetOfTuplesOfPositiveOrderedType.compareList [definition, in sets]
SetOfTuplesOfPositiveOrderedType.compareListSpec [lemma, in sets]
SetOfTuplesOfPositiveOrderedType.compare_spec [lemma, in sets]
SetOfTuplesOfPositiveOrderedType.eq [definition, in sets]
SetOfTuplesOfPositiveOrderedType.eqb [definition, in sets]
SetOfTuplesOfPositiveOrderedType.eqbList [definition, in sets]
SetOfTuplesOfPositiveOrderedType.eqbListEqList [lemma, in sets]
SetOfTuplesOfPositiveOrderedType.eqb_eq [lemma, in sets]
SetOfTuplesOfPositiveOrderedType.eqList [definition, in sets]
SetOfTuplesOfPositiveOrderedType.eqListOK [lemma, in sets]
SetOfTuplesOfPositiveOrderedType.eqListRefl [lemma, in sets]
SetOfTuplesOfPositiveOrderedType.eqListSortOCP [lemma, in sets]
SetOfTuplesOfPositiveOrderedType.eqListSym [lemma, in sets]
SetOfTuplesOfPositiveOrderedType.eqListTrans [lemma, in sets]
SetOfTuplesOfPositiveOrderedType.lengthAtLeastOne [lemma, in sets]
SetOfTuplesOfPositiveOrderedType.lengthOne [lemma, in sets]
SetOfTuplesOfPositiveOrderedType.lt [definition, in sets]
SetOfTuplesOfPositiveOrderedType.ltAntiref [lemma, in sets]
SetOfTuplesOfPositiveOrderedType.ltIrrefl [lemma, in sets]
SetOfTuplesOfPositiveOrderedType.ltList [definition, in sets]
SetOfTuplesOfPositiveOrderedType.ltListIrrefl [lemma, in sets]
SetOfTuplesOfPositiveOrderedType.ltListTrans [lemma, in sets]
SetOfTuplesOfPositiveOrderedType.ltTrans [lemma, in sets]
SetOfTuplesOfPositiveOrderedType.lt_compat [instance, in sets]
SetOfTuplesOfPositiveOrderedType.lt_strorder [instance, in sets]
SetOfTuplesOfPositiveOrderedType.sortOK [lemma, in sets]
SetOfTuplesOfPositiveOrderedType.t [definition, in sets]
sets [library]
sndpp [definition, in sets]
snd_sp [definition, in ColR]
snd_ss [definition, in ColR]
some_fun_ind [lemma, in Epsilon]
some_fun_e [lemma, in Epsilon]
some_fun [definition, in Epsilon]
SP [module, in sets]
SPWEqP [module, in ColR]
sp_ok_empty [lemma, in ColR]
sp_ok [definition, in ColR]
Square [definition, in quadrilaterals]
Square_Rhombus [lemma, in quadrilaterals_inter_dec]
square_perp_rectangle [lemma, in quadrilaterals_inter_dec]
Square_Parallelogram [lemma, in quadrilaterals]
Square_Rectangle [lemma, in quadrilaterals]
Square_not_triv_3 [lemma, in quadrilaterals]
Square_not_triv_2 [lemma, in quadrilaterals]
Square_not_triv [lemma, in quadrilaterals]
SS [module, in sets]
SSWEqP [module, in ColR]
SSWP [module, in ColR]
ss_ok_empty [lemma, in ColR]
ss_ok [definition, in ColR]
ST [module, in sets]
subst_sp_ok [lemma, in ColR]
subst_in_sp [definition, in ColR]
subst_in_sp_aux_2 [definition, in ColR]
subst_in_sp_aux_1 [definition, in ColR]
subst_ss_ok [lemma, in ColR]
subst_in_ss [definition, in ColR]
subst_in_ss_aux [definition, in ColR]
subst_in_set [definition, in ColR]
sum_unicity [lemma, in vectors]
sum_exists [lemma, in vectors]
sum_sym [lemma, in vectors]
swap_diff [lemma, in Ch07_midpoint]
SWP [module, in sets]
symmetric_point [definition, in construction_functions]
symmetric_point_ex_unicity [lemma, in construction_functions]
symmetric_point_unicity [lemma, in Ch07_midpoint]
symmetric_point_construction [lemma, in Ch07_midpoint]
symmetry_preserves_bet [lemma, in orientation]
symmetry_preseves_bet2 [lemma, in orientation]
symmetry_preseves_bet1 [lemma, in orientation]
symmetry_preserves_conga [lemma, in project]
symmetry_preserves_one_side [lemma, in quadrilaterals]
symmetry_preserves_two_sides [lemma, in quadrilaterals]
symmetry_preserves_bet [lemma, in quadrilaterals]
symmetry_preseves_bet2 [lemma, in quadrilaterals]
symmetry_preseves_bet1 [lemma, in quadrilaterals]
symmetry_preserves_midpoint [lemma, in Ch07_midpoint]
sym_preserve_diff [lemma, in Ch09_plane]
sym_sym [lemma, in Ch09_plane]
sym_par [lemma, in quadrilaterals]
T
T [section, in construction_functions]T [section, in tarski_to_hilbert]
T [definition, in tarski_to_beeson]
tactics_axioms [library]
Tagged_predicates [section, in Tagged_predicates]
Tagged_predicates [library]
tailCP [definition, in arity]
tailCPbis [definition, in arity]
tailDefaultCP [definition, in arity]
Tarski_is_a_Coapp_theory [instance, in tarski_to_coapp_theory]
Tarski_is_a_Coapp_theory [section, in tarski_to_coapp_theory]
Tarski_is_a_Col_theory [instance, in tarski_to_col_theory]
Tarski_is_a_Col_theory [section, in tarski_to_col_theory]
Tarski_follows_from_Makarios_Variant [instance, in tarski_to_makarios]
Tarski_neutral_dimensionless_variant [record, in tarski_axioms]
Tarski_2D_euclidean [record, in tarski_axioms]
Tarski_2D [record, in tarski_axioms]
Tarski_neutral_dimensionless [record, in tarski_axioms]
Tarski_to_intuitionistic_Tarski [section, in tarski_to_beeson]
tarski_to_col_theory [library]
tarski_axioms [library]
tarski_to_coapp_theory [library]
tarski_to_hilbert [library]
tarski_to_makarios [library]
tarski_to_beeson [library]
Tarski83_to_Makarios_variant [section, in tarski_to_makarios]
tau [definition, in Epsilon]
test_col_ok [lemma, in ColR]
test_col [definition, in ColR]
the_fun_ind [lemma, in Epsilon]
the_fun_rw [lemma, in Epsilon]
the_fun_e [lemma, in Epsilon]
the_fun [definition, in Epsilon]
third_point [lemma, in Ch05_bet_le]
three_medians_intersect [lemma, in gravityCenter]
Tpoint [projection, in tarski_axioms]
TriangleMidpointsTheorems [section, in triangle_midpoints_theorems]
Triangles [section, in triangles]
triangles [library]
Triangles.ABC [section, in triangles]
Triangles.ABC.A [variable, in triangles]
Triangles.ABC.B [variable, in triangles]
Triangles.ABC.C [variable, in triangles]
triangle_par [lemma, in project]
triangle_par_mid [lemma, in triangle_midpoints_theorems]
triangle_mid_par_cong [lemma, in triangle_midpoints_theorems]
triangle_mid_par [lemma, in triangle_midpoints_theorems]
triangle_mid_par_flat [lemma, in triangle_midpoints_theorems]
triangle_mid_par_flat_cong [lemma, in triangle_midpoints_theorems]
triangle_mid_par_flat_cong_2 [lemma, in triangle_midpoints_theorems]
triangle_mid_par_flat_cong_1 [lemma, in triangle_midpoints_theorems]
triangle_mid_par_flat_cong_aux [lemma, in triangle_midpoints_theorems]
triangle_mid_par_strict [lemma, in triangle_midpoints_theorems]
triangle_mid_par_strict_cong [lemma, in triangle_midpoints_theorems]
triangle_mid_par_strict_cong_simp [lemma, in triangle_midpoints_theorems]
triangle_mid_par_strict_cong_2 [lemma, in triangle_midpoints_theorems]
triangle_mid_par_strict_cong_1 [lemma, in triangle_midpoints_theorems]
triangle_mid_par_strict_cong_aux [lemma, in triangle_midpoints_theorems]
triangle_circumscription_implies_inter_dec [lemma, in perp_bisect]
triangle_mid_par [lemma, in Ch13_1]
triangle_midpoints_theorems [library]
Triple [record, in aux]
ts_cong_par_cong_par [lemma, in quadrilaterals_inter_dec]
ts_per_per_ts [lemma, in Ch13_1]
ts_ts_os [lemma, in Ch13_1]
two_distinct_points [lemma, in Ch03_bet]
two_sides [definition, in Ch09_plane]
two_sides_dec [lemma, in Ch12_parallel_inter_dec]
two_sides_in_angle [lemma, in Ch11_angles]
two_sides_not_col [lemma, in Ch11_angles]
two_points_on_line [projection, in hilbert_axioms]
T_dec [lemma, in tarski_to_beeson]
T_Bet [lemma, in tarski_to_beeson]
T_42 [section, in midpoint_thales]
_ =h= _ (type_scope) [notation, in tarski_to_hilbert]
_ =l= _ (type_scope) [notation, in tarski_to_hilbert]
T1_3 [section, in Ch02_cong]
T1_2 [section, in Ch02_cong]
T1_1 [section, in Ch02_cong]
T10 [section, in Ch10_line_reflexivity_2D]
T10 [section, in Ch10_line_reflexivity]
T11 [section, in Ch11_angles]
T12_3 [section, in Ch12_parallel]
T12_2 [section, in Ch12_parallel]
T12_1 [section, in Ch12_parallel]
T13 [section, in Ch12_parallel_inter_dec]
t2_8 [lemma, in Ch06_out_lines]
T2_5 [section, in Ch03_bet]
T2_4 [section, in Ch03_bet]
T2_3 [section, in Ch03_bet]
T2_2 [section, in Ch03_bet]
T2_1 [section, in Ch03_bet]
T3 [section, in Ch04_cong_bet]
T4_4 [section, in Ch04_col]
T4_3 [section, in Ch04_col]
T4_2 [section, in Ch04_col]
T4_1 [section, in Ch04_col]
T5 [section, in Ch05_bet_le]
T6_2 [section, in Ch06_out_lines]
T6_1 [section, in Ch06_out_lines]
T7_2 [section, in Ch07_midpoint]
T7_1 [section, in Ch07_midpoint]
T8_5 [section, in Ch08_orthogonality]
T8_4 [section, in Ch08_orthogonality]
T8_3 [section, in Ch08_orthogonality]
T8_2 [section, in Ch08_orthogonality]
T8_1 [section, in Ch08_orthogonality]
T9 [section, in Ch09_plane]
U
UnitTests [section, in unit_tests]unit_tests [library]
unspec [definition, in Epsilon]
upper_dim [projection, in tarski_axioms]
V
V [projection, in aux]Vectors [section, in vectors]
vectors [library]
vector_same_dir_cong [lemma, in vectors]
vector_unicity [lemma, in vectors]
vector_construction_unicity [lemma, in vectors]
vector_construction [lemma, in vectors]
V1 [projection, in aux]
V2 [projection, in aux]
W
wd [projection, in tactics_axioms]wd_perm_2 [projection, in tactics_axioms]
wd_perm_1 [projection, in tactics_axioms]
other
Something [notation, in general_tactics]Instance Index
B
Beeson_follows_from_Tarski [in tarski_to_beeson]E
Eq_Equiv [in tarski_to_hilbert]H
hconga_Equiv [in tarski_to_hilbert]hEq_Equiv [in tarski_to_hilbert]
Hilbert_follow_from_Tarski [in tarski_to_hilbert]
I
incident_Proper [in tarski_to_hilbert]IT_to_T [in tarski_to_beeson]
M
Makarios_Variant_follows_from_Tarski [in tarski_to_makarios]S
SetOfPairsOfPositiveOrderedType.lt_strorder [in sets]SetOfPairsOfPositiveOrderedType.lt_compat [in sets]
SetOfSetsOfPositiveOrderedType.lt_strorder [in sets]
SetOfSetsOfPositiveOrderedType.lt_compat [in sets]
SetOfTuplesOfPositiveOrderedType.lt_compat [in sets]
SetOfTuplesOfPositiveOrderedType.lt_strorder [in sets]
T
Tarski_is_a_Coapp_theory [in tarski_to_coapp_theory]Tarski_is_a_Col_theory [in tarski_to_col_theory]
Tarski_follows_from_Makarios_Variant [in tarski_to_makarios]
Projection Index
A
addition [in hilbert_axioms]aux [in hilbert_axioms]
B
Bet [in tarski_axioms]BetH [in hilbert_axioms]
BetM [in tarski_axioms]
between_identity [in tarski_axioms]
between_one [in hilbert_axioms]
between_only_one [in hilbert_axioms]
between_out [in hilbert_axioms]
between_comm [in hilbert_axioms]
between_col [in hilbert_axioms]
Bet_stability [in tarski_axioms]
C
coapp [in tactics_axioms]coapp_perm_2 [in tactics_axioms]
coapp_perm_1 [in tactics_axioms]
COATpoint [in tactics_axioms]
Cond [in aux]
Cong [in tarski_axioms]
CongaH [in hilbert_axioms]
CongH [in hilbert_axioms]
CongM [in tarski_axioms]
Cong_stability [in tarski_axioms]
cong_inner_transitivity [in tarski_axioms]
cong_identity [in tarski_axioms]
cong_pseudo_reflexivity [in tarski_axioms]
cong_5 [in hilbert_axioms]
cong_unicity [in hilbert_axioms]
cong_existence [in hilbert_axioms]
cong_refl [in hilbert_axioms]
cong_pseudo_transitivity [in hilbert_axioms]
CTcol_permutation_2 [in tactics_axioms]
CTcol_permutation_1 [in tactics_axioms]
CTcol_trivial [in tactics_axioms]
CTcol3 [in tactics_axioms]
E
EqL [in hilbert_axioms]EqL_Equiv [in hilbert_axioms]
eq_dec_points [in tarski_axioms]
euclid [in tarski_axioms]
euclid_unicity [in hilbert_axioms]
euclid_existence [in hilbert_axioms]
F
five_segments [in tarski_axioms]H
hcong_4_unicity [in hilbert_axioms]hcong_4_existence [in hilbert_axioms]
I
IBet [in tarski_axioms]Ibetween_inner_transitivity [in tarski_axioms]
Ibetween_symmetry [in tarski_axioms]
Ibetween_identity [in tarski_axioms]
ICong [in tarski_axioms]
Icong_inner_transitivity [in tarski_axioms]
Icong_pseudo_reflexivity [in tarski_axioms]
Icong_identity [in tarski_axioms]
Ifive_segments [in tarski_axioms]
Iinner_pasch [in tarski_axioms]
Ilower_dim [in tarski_axioms]
Incid [in hilbert_axioms]
inner_pasch [in tarski_axioms]
inter_dec [in tarski_axioms]
Isegment_construction [in tarski_axioms]
ITpoint [in tarski_axioms]
L
Line [in hilbert_axioms]line_of_hline [in hilbert_axioms]
line_unicity [in hilbert_axioms]
line_existence [in hilbert_axioms]
link_betwenn_wd_and_coapp [in tactics_axioms]
lower_dim [in tarski_axioms]
M
Mbetween_identity [in tarski_axioms]Mcong_inner_transitivity [in tarski_axioms]
Mcong_identity [in tarski_axioms]
Mfive_segments [in tarski_axioms]
Minner_pasch [in tarski_axioms]
Mlower_dim [in tarski_axioms]
Msegment_construction [in tarski_axioms]
MTpoint [in tarski_axioms]
N
n [in tactics_axioms]P
pasch [in hilbert_axioms]plan [in hilbert_axioms]
Point [in hilbert_axioms]
Pred [in aux]
pseudo_trans_of_coapp [in tactics_axioms]
P1 [in aux]
P2 [in aux]
S
segment_construction [in tarski_axioms]T
Tpoint [in tarski_axioms]two_points_on_line [in hilbert_axioms]
U
upper_dim [in tarski_axioms]V
V [in aux]V1 [in aux]
V2 [in aux]
W
wd [in tactics_axioms]wd_perm_2 [in tactics_axioms]
wd_perm_1 [in tactics_axioms]
Record Index
A
Arity [in tactics_axioms]C
Coapp_theory [in tactics_axioms]Coapp_predicates [in tactics_axioms]
Col_theory [in tactics_axioms]
Couple [in aux]
E
EqDecidability [in tarski_axioms]H
Hilbert [in hilbert_axioms]I
InterDecidability [in tarski_axioms]intuitionistic_Tarski_neutral_dimensionless [in tarski_axioms]
T
Tarski_neutral_dimensionless_variant [in tarski_axioms]Tarski_2D_euclidean [in tarski_axioms]
Tarski_2D [in tarski_axioms]
Tarski_neutral_dimensionless [in tarski_axioms]
Triple [in aux]
Lemma Index
A
acute_comp_not_acute [in Ch13_4_cos]acute_not_obtuse [in Ch13_4_cos]
acute_col_out [in Ch13_3_angles]
acute_not_bet [in Ch13_3_angles]
acute_not_per [in Ch13_5_Pappus_Pascal]
acute_trivial [in Ch13_5_Pappus_Pascal]
acute_distinct [in Ch11_angles]
acute_lea_acute [in Ch11_angles]
acute_sym [in Ch11_angles]
allButLastCPTl [in arity]
all_eqaa [in Ch13_3_angles]
all_eqa [in Ch13_3_angles]
all_eql [in Ch13_2_length]
all_one_side_par_strict [in Ch12_parallel]
altitude_intersect [in orthocenter]
altitude_is_perp_bisect [in orthocenter]
anga_col_null [in Ch13_4_cos]
anga_not_lg_null [in Ch13_4_cos]
anga_out_anga [in Ch13_4_cos]
anga_conga_anga [in Ch13_4_cos]
anga_col_out [in Ch13_4_cos]
anga_const_o [in Ch13_3_angles]
anga_not_flat [in Ch13_3_angles]
anga_acute [in Ch13_3_angles]
anga_const [in Ch13_3_angles]
anga_distincts [in Ch13_3_angles]
anga_not_null_lg [in Ch13_3_angles]
anga_sym [in Ch13_3_angles]
anga_distinct [in Ch13_3_angles]
anga_conga [in Ch13_3_angles]
anga_is_ang [in Ch13_3_angles]
anga_exists [in Ch13_3_angles]
angle_construction_3 [in Ch11_angles]
angle_construction_2 [in Ch11_angles]
angle_construction_1 [in Ch11_angles]
ang_not_lg_null [in Ch13_4_cos]
ang_cong_ang [in Ch13_3_angles]
ang_const_o [in Ch13_3_angles]
ang_distincts [in Ch13_3_angles]
ang_not_null_lg [in Ch13_3_angles]
ang_sym [in Ch13_3_angles]
ang_const [in Ch13_3_angles]
ang_distinct [in Ch13_3_angles]
ang_conga [in Ch13_3_angles]
ang_exists [in Ch13_3_angles]
another_point [in Ch03_bet]
another_point [in tarski_to_beeson]
app_2_n_app_eq [in arity]
app_app_2_n_default [in arity]
app_app_2_n [in arity]
app_2_n_app_default [in arity]
app_2_n_app [in arity]
app_1_n_app_eq [in arity]
app_app_1_n [in arity]
app_1_n_app [in arity]
app_n_1_app_eq [in arity]
app_app_n_1 [in arity]
app_n_1_app [in arity]
aux [in tarski_to_hilbert]
axiom_cong_5' [in tarski_to_hilbert]
axiom_hcong_4_unicity [in tarski_to_hilbert]
axiom_hcong_4_existence [in tarski_to_hilbert]
axiom_hcong_3 [in tarski_to_hilbert]
axiom_hcong_refl [in tarski_to_hilbert]
axiom_hcong_trans [in tarski_to_hilbert]
axiom_hcong_scott [in tarski_to_hilbert]
axiom_hcong_1_unicity [in tarski_to_hilbert]
axiom_hcong_1_existence [in tarski_to_hilbert]
axiom_euclid_unicity [in tarski_to_hilbert]
axiom_euclid_existence [in tarski_to_hilbert]
axiom_pasch [in tarski_to_hilbert]
axiom_between_one [in tarski_to_hilbert]
axiom_between_only_one [in tarski_to_hilbert]
axiom_between_out [in tarski_to_hilbert]
axiom_between_comm [in tarski_to_hilbert]
axiom_between_col [in tarski_to_hilbert]
axiom_plan [in tarski_to_hilbert]
axiom_two_points_on_line [in tarski_to_hilbert]
axiom_line_unicity [in tarski_to_hilbert]
axiom_line_existence [in tarski_to_hilbert]
B
BetH_Bet [in tarski_to_beeson]BetT_id [in tarski_to_beeson]
BetT_symmetry [in tarski_to_beeson]
between_exchange4 [in Ch03_bet]
between_exchange2 [in Ch03_bet]
between_exchange3 [in Ch03_bet]
between_inner_transitivity [in Ch03_bet]
between_egality [in Ch03_bet]
between_trivial2 [in Ch03_bet]
between_symmetry [in Ch03_bet]
between_trivial [in Ch03_bet]
between_one [in tarski_to_hilbert]
between_symmetry [in tarski_to_makarios]
between_trivial [in tarski_to_makarios]
between_symmetry_B [in tarski_to_beeson]
between_inner_transitivity_B [in tarski_to_beeson]
between_identity_B [in tarski_to_beeson]
between_symmetric [in Ch11_angles]
between_cong_3 [in Ch05_bet_le]
between_cong_2 [in Ch05_bet_le]
between_cong [in Ch05_bet_le]
bet_half_bet [in orientation]
bet_double_bet [in orientation]
bet_le_le [in orientation]
bet_out_out_bet [in Ch06_out_lines]
bet_dec_eq_dec_b [in Ch03_bet]
Bet_perm [in Ch03_bet]
Bet_cases [in Ch03_bet]
bet_dec_eq_dec [in Ch03_bet]
bet_col [in Ch03_bet]
Bet_tagged_Bet [in Tagged_predicates]
Bet_Bet_tagged [in Tagged_predicates]
Bet_Between_H [in tarski_to_hilbert]
bet_flat_ang [in Ch13_3_angles]
bet_cong3 [in Ch08_orthogonality]
bet_cong_bet [in quadrilaterals]
bet_half_bet [in quadrilaterals]
bet_double_bet [in quadrilaterals]
bet_le_le [in quadrilaterals]
bet_col2 [in Ch07_midpoint]
bet_col1 [in Ch07_midpoint]
bet_id [in tarski_to_beeson]
Bet_T [in tarski_to_beeson]
bet_stability [in tarski_to_beeson]
bet_le_eq [in Ch11_angles]
bet_in_angle_bet [in Ch11_angles]
bet_conga_bet [in Ch11_angles]
bet_out [in Ch11_angles]
bet_same_dir2 [in vectors]
bet_same_dir1 [in vectors]
bet_cong_eq [in Ch05_bet_le]
Bet_dec [in Ch05_bet_le]
bet2_cong_bet [in quadrilaterals]
bet2_out_out [in Ch11_angles]
bet3_cong3_bet [in quadrilaterals]
C
chasles [in vectors]choice_fun_ind [in Epsilon]
choice_fun_e [in Epsilon]
circPermNConsOK [in arity]
circPermNConsTlOK [in arity]
circPermNCPOK [in arity]
circPermNCP0 [in arity]
circPermNId [in arity]
circPermNIdAux [in arity]
circPermNIdFirst [in arity]
circPermPerm [in arity]
circumcenter_intersect [in circumcenter]
circumcenter_perp [in circumcenter]
circumcenter_cong [in circumcenter]
ColB_Col [in tarski_to_beeson]
collect_diffs [in ColR]
collect_cols [in ColR]
cols_coincide_2 [in tarski_to_hilbert]
cols_coincide_1 [in tarski_to_hilbert]
colx [in Ch09_plane]
col_proj_proj [in orientation]
col_proj_col [in orientation]
col_transitivity_2 [in Ch06_out_lines]
col_transitivity_1 [in Ch06_out_lines]
col_cong_cong [in quadrilaterals_inter_dec]
Col_tagged_Col [in ColR]
Col_Col_tagged [in ColR]
Col_tagged_Col [in Tagged_predicates]
Col_Col_tagged [in Tagged_predicates]
col_incident [in tarski_to_hilbert]
col_disjoint_bet [in tarski_to_hilbert]
col_perm_2 [in tarski_to_coapp_theory]
col_perm_1 [in tarski_to_coapp_theory]
col_eq [in Ch09_plane]
col_preserves_two_sides [in Ch09_plane]
col_col_per_per [in Ch08_orthogonality]
col_cong_mid2 [in quadrilaterals]
col_cong_mid1 [in quadrilaterals]
col_bet2_cong2 [in quadrilaterals]
col_bet2_cong1 [in quadrilaterals]
col_cong2_bet4 [in quadrilaterals]
col_cong2_bet3 [in quadrilaterals]
col_cong2_bet2 [in quadrilaterals]
col_cong2_bet1 [in quadrilaterals]
col_cong_bet [in quadrilaterals]
col_not_plgs [in quadrilaterals]
col_cong_mid [in quadrilaterals]
col_trivial_3 [in Ch04_col]
col_trivial_2 [in Ch04_col]
col_trivial_1 [in Ch04_col]
Col_perm [in Ch04_col]
Col_cases [in Ch04_col]
col_permutation_5 [in Ch04_col]
col_permutation_4 [in Ch04_col]
col_permutation_3 [in Ch04_col]
col_permutation_2 [in Ch04_col]
col_permutation_1 [in Ch04_col]
col_par_par_col [in Ch12_parallel_inter_dec]
col_per_perp [in Ch10_line_reflexivity]
Col_dec [in tarski_to_beeson]
col_perp_perp_col [in Ch11_angles]
col_two_sides_bet [in Ch11_angles]
col_one_side_out [in Ch11_angles]
col_conga_col [in Ch11_angles]
col_out2_col [in Ch11_angles]
col_in_angle_out [in Ch11_angles]
col_in_angle [in Ch11_angles]
col_one_side [in Ch11_angles]
col_two_sides [in Ch11_angles]
Col_dec [in Ch05_bet_le]
col_par [in Ch12_parallel]
col_not_col_not_par [in Ch12_parallel]
col3 [in Ch06_out_lines]
compute_new_set_of_sets_of_collinear_points_ok [in ColR]
conga_to_par_os [in quadrilaterals_inter_dec]
conga_to_par_ts [in quadrilaterals_inter_dec]
conga_distinct [in Ch11_angles]
Conga_dec [in Ch11_angles]
conga_sym_equiv [in Ch11_angles]
conga_preserves_gta [in Ch11_angles]
conga_preserves_lta [in Ch11_angles]
conga_preserves_in_angle [in Ch11_angles]
conga_ex_cong3 [in Ch11_angles]
conga_line [in Ch11_angles]
conga_comm [in Ch11_angles]
conga_left_comm [in Ch11_angles]
conga_right_comm [in Ch11_angles]
conga_trivial_1 [in Ch11_angles]
conga_pseudo_refl [in Ch11_angles]
conga_trans [in Ch11_angles]
conga_diff2 [in Ch11_angles]
conga_diff1 [in Ch11_angles]
conga_sym [in Ch11_angles]
conga_refl [in Ch11_angles]
cong_le_le [in orientation]
cong_identity_inv [in orientation]
cong_dec_eq_dec_b [in Ch03_bet]
Cong_tagged_Cong [in Tagged_predicates]
Cong_Cong_tagged [in Tagged_predicates]
cong_conga3_cong3 [in project]
cong_pseudo_reflexivity [in tarski_to_makarios]
cong_left_commutativity [in tarski_to_makarios]
cong_symmetry [in tarski_to_makarios]
cong_reflexivity [in tarski_to_makarios]
cong_le_le [in quadrilaterals]
cong_identity_inv [in quadrilaterals]
Cong_perm [in Ch02_cong]
Cong_cases [in Ch02_cong]
cong_3_swap_2 [in Ch02_cong]
cong_3_swap [in Ch02_cong]
cong_3_sym [in Ch02_cong]
cong_diff_4 [in Ch02_cong]
cong_diff_3 [in Ch02_cong]
cong_diff_2 [in Ch02_cong]
cong_diff [in Ch02_cong]
cong_dec_eq_dec [in Ch02_cong]
cong_commutativity [in Ch02_cong]
cong_reverse_identity [in Ch02_cong]
cong_trivial_identity [in Ch02_cong]
cong_right_commutativity [in Ch02_cong]
cong_left_commutativity [in Ch02_cong]
cong_transitivity [in Ch02_cong]
cong_symmetry [in Ch02_cong]
cong_reflexivity [in Ch02_cong]
cong_cong_half_2 [in Ch07_midpoint]
cong_cong_half_1 [in Ch07_midpoint]
cong_col_mid [in Ch07_midpoint]
cong_conga_perp [in Ch12_parallel_inter_dec]
cong_stability_eq_stability [in tarski_to_beeson]
cong_stability [in tarski_to_beeson]
cong_perp_bisect [in perp_bisect]
cong_perp_conga [in Ch13_1]
cong_preserves_bet [in Ch11_angles]
Cong_dec [in Ch05_bet_le]
cong2_conga_cong [in Ch11_angles]
cong3_par2_par [in quadrilaterals_inter_dec]
cong3_id [in quadrilaterals]
cong3_transitivity [in Ch02_cong]
cong3_bet_eq [in Ch04_cong_bet]
cong3_preserves_out [in Ch11_angles]
cong3_conga2 [in Ch11_angles]
cong3_conga [in Ch11_angles]
cong3_symmetry [in Ch05_bet_le]
consHdTlTlHd [in arity]
consHeadCPHd [in arity]
consHeadCPOK [in arity]
consHeadCPTl [in arity]
consTailCPAbl [in arity]
consTailCPLast [in arity]
consTailCPOK [in arity]
consTailCPTl [in arity]
consTailCPTlD [in arity]
consTailOK [in arity]
consTailPerm [in arity]
consTlHdHdTl [in arity]
construction_unicity [in Ch02_cong]
construct_triangle [in orthocenter]
construct_intersection [in orthocenter]
coplanar_perm_11 [in Ch10_line_reflexivity]
coplanar_perm_10 [in Ch10_line_reflexivity]
coplanar_perm_9 [in Ch10_line_reflexivity]
coplanar_perm_8 [in Ch10_line_reflexivity]
coplanar_perm_7 [in Ch10_line_reflexivity]
coplanar_perm_6 [in Ch10_line_reflexivity]
coplanar_perm_5 [in Ch10_line_reflexivity]
coplanar_perm_4 [in Ch10_line_reflexivity]
coplanar_perm_3 [in Ch10_line_reflexivity]
coplanar_perm_2 [in Ch10_line_reflexivity]
coplanar_perm_1 [in Ch10_line_reflexivity]
CPCPL [in arity]
CPLCP [in arity]
CPLHd [in arity]
CPLHdTlOK [in arity]
CPLOCPTlOK [in sets]
CPLOK [in arity]
CPLRec [in arity]
CPToListOK [in arity]
CPToListTl1 [in arity]
CPToListTl2 [in arity]
CP_ind [in arity]
CTcol_trivial_2 [in ColR]
CTcol_trivial_1 [in ColR]
CTcol_permutation_4 [in ColR]
CTcol_permutation_3 [in ColR]
CTcol_permutation_2 [in ColR]
CTcol_permutation_5 [in ColR]
cut_two_sides [in tarski_to_hilbert]
D
dd' [in Epsilon]dd'' [in Epsilon]
Diff_tagged_Diff [in ColR]
Diff_Diff_tagged [in ColR]
Diff_perm [in Tagged_predicates]
Diff_tagged_Diff [in Tagged_predicates]
Diff_Diff_tagged [in Tagged_predicates]
diff_or_col [in tarski_to_coapp_theory]
diff_perm_2 [in tarski_to_coapp_theory]
diff_perm_1 [in tarski_to_coapp_theory]
diff_col_ex3 [in Ch09_plane]
diff_bet_ex3 [in Ch09_plane]
diff_col_ex [in Ch09_plane]
diff_per_diff [in Ch08_orthogonality]
diff_bet [in Ch07_midpoint]
diff_not_col_col_par4_mid [in orthocenter]
Diff_Col_ColB [in tarski_to_beeson]
diff_out [in Ch11_angles]
distinct [in Ch09_plane]
distinct [in Ch08_orthogonality]
E
epsilon_equiv [in Epsilon]epsilon_ind [in Epsilon]
eqA_preserves_anga [in Ch13_4_cos]
eql_lg [in Ch13_4_cos]
eql_lcos_null [in Ch13_4_cos]
eql_trans [in Ch13_2_length]
eql_sym [in Ch13_2_length]
eql_refl [in Ch13_2_length]
eqo_refl [in orientation]
eqo_one_side [in orientation]
eqo_eq_o [in orientation]
equilateral_strict_conga_3 [in triangles]
equilateral_strict_conga_2 [in triangles]
equilateral_strict_conga_1 [in triangles]
equilateral_strict_swap_5 [in triangles]
equilateral_strict_swap_4 [in triangles]
equilateral_strict_swap_3 [in triangles]
equilateral_strict_swap_2 [in triangles]
equilateral_strict_swap_1 [in triangles]
equilateral_strict_neq [in triangles]
equilateral_isosceles_3 [in triangles]
equilateral_isosceles_2 [in triangles]
equilateral_isosceles_1 [in triangles]
equilateral_swap_rot [in triangles]
equilateral_swap_2 [in triangles]
equilateral_rot_2 [in triangles]
equilateral_swap [in triangles]
equilateral_rot [in triangles]
equilateral_cong [in triangles]
equilateral_strict_equilateral [in triangles]
eqv_cong [in project]
eqv_eq_project [in project]
eqv_project_eq_eq [in project]
eqv_mid [in vectors]
eqv_sum [in vectors]
eqv_opp_null [in vectors]
eqv_par [in vectors]
eqv_permut [in vectors]
eqv_trivial [in vectors]
eqv_comm [in vectors]
eqv_trans [in vectors]
eqv_sym [in vectors]
eqv_refl [in vectors]
eq_o_refl [in orientation]
eq_o_one_side [in orientation]
eq_o_eqo [in orientation]
eq_eq_tagged [in ColR]
eq_incident [in tarski_to_hilbert]
eq_symmetry [in tarski_to_hilbert]
eq_reflexivity [in tarski_to_hilbert]
eq_transitivity [in tarski_to_hilbert]
eq_dec [in tarski_to_beeson]
eq_conga_out [in Ch11_angles]
exists_witness_ok [in ColR]
exists_not_incident [in tarski_to_hilbert]
ex_col1 [in orientation]
ex_col [in orientation]
ex_unique_introduction [in Epsilon]
ex_anga [in Ch13_3_angles]
ex_eqaa [in Ch13_3_angles]
ex_points_anga [in Ch13_3_angles]
ex_ang [in Ch13_3_angles]
ex_eqa [in Ch13_3_angles]
ex_points_ang [in Ch13_3_angles]
ex_lg [in Ch13_2_length]
ex_eql [in Ch13_2_length]
ex_points_lg_not_col [in Ch13_2_length]
ex_point_lg_bet [in Ch13_2_length]
ex_point_lg_out [in Ch13_2_length]
ex_point_lg [in Ch13_2_length]
ex_points_lg [in Ch13_2_length]
ex_col2 [in Ch08_orthogonality]
ex_col3 [in quadrilaterals]
ex_sym1 [in Ch10_line_reflexivity]
ex_sym [in Ch10_line_reflexivity]
ex_per_cong [in Ch11_angles]
F
five_segments [in tarski_to_makarios]five_segments' [in tarski_to_makarios]
five_segments_with_def [in Ch02_cong]
five_segments [in tarski_to_beeson]
five_segments_B [in tarski_to_beeson]
fixLastCPOK [in arity]
flat_not_acute [in Ch13_4_cos]
flat_ang [in Ch13_3_angles]
forall_def [in Epsilon]
fourth_point [in Ch05_bet_le]
G
get_suitable_pair_of_sets_ok_2 [in ColR]get_suitable_pair_of_sets_ok_1 [in ColR]
ge_comm [in Ch11_angles]
ge_right_comm [in Ch11_angles]
ge_left_comm [in Ch11_angles]
gta_trans [in Ch11_angles]
gt_comm [in Ch11_angles]
gt_right_comm [in Ch11_angles]
gt_left_comm [in Ch11_angles]
H
half_plgs [in quadrilaterals_inter_dec]hconga_trans [in tarski_to_hilbert]
hconga_sym [in tarski_to_hilbert]
hconga_refl [in tarski_to_hilbert]
hEq_trans [in tarski_to_hilbert]
hEq_sym [in tarski_to_hilbert]
hEq_refl [in tarski_to_hilbert]
I
image_cong_col [in Ch10_line_reflexivity_2D]image_col [in Ch10_line_reflexivity]
image_preserves_per [in Ch10_line_reflexivity]
image_preserves_midpoint [in Ch10_line_reflexivity]
image_gen_preserves_bet [in Ch10_line_reflexivity]
image_preserves_bet [in Ch10_line_reflexivity]
image_in_col0 [in Ch10_line_reflexivity]
image_in_col [in Ch10_line_reflexivity]
image_image_in [in Ch10_line_reflexivity]
image_in_gen_is_image [in Ch10_line_reflexivity]
image_in_is_image_spec [in Ch10_line_reflexivity]
image_id [in Ch10_line_reflexivity]
inangle_one_side2 [in Ch13_1]
inangle_one_side [in Ch13_1]
incident_col [in tarski_to_hilbert]
incident_eq [in tarski_to_hilbert]
Incid_line [in tarski_to_hilbert]
InCPOCP [in sets]
InCPOK [in arity]
inhabited_bool [in Epsilon]
inner_pasch_B [in tarski_to_beeson]
InNth [in arity]
intersection_two_medians_exist_unique [in gravityCenter]
intersection_two_medians_exist [in gravityCenter]
inter_unicity [in Ch09_plane]
inter_comm [in Ch12_parallel]
inter_right_comm [in Ch12_parallel]
inter_left_comm [in Ch12_parallel]
inter_sym [in Ch12_parallel]
inter_trivial [in Ch12_parallel]
inter_unicity_not_par [in Ch12_parallel]
invert_one_side [in Ch09_plane]
invert_two_sides [in Ch09_plane]
in_angleH_trivial [in tarski_to_hilbert]
in_angleH_in_angle [in tarski_to_hilbert]
in_angle_equiv [in tarski_to_hilbert]
in_angle_reverse [in Ch11_angles]
in_angle_asym [in Ch11_angles]
in_angle_trans [in Ch11_angles]
in_angle_line [in Ch11_angles]
in_angle_trivial_2 [in Ch11_angles]
in_angle_trivial_1 [in Ch11_angles]
in_angle_one_side [in Ch11_angles]
in_angle_out [in Ch11_angles]
in_angle_two_sides [in Ch11_angles]
iota_rw [in Epsilon]
iota_fun_rw [in Epsilon]
iota_fun_ind [in Epsilon]
iota_fun_e [in Epsilon]
iota_parameter_rw [in Epsilon]
iota_ind_weak [in Epsilon]
iota_ind [in Epsilon]
iota_e_weak [in Epsilon]
iota_e [in Epsilon]
ise_to_is [in vectors]
isosceles_conga [in triangles]
isosceles_sym [in triangles]
is_gravity_center_exist_unique [in gravityCenter]
is_null_anga_dec [in Ch13_4_cos]
is_null_all [in Ch13_4_cos]
is_null_ang_out [in Ch13_3_angles]
is_null_anga_out [in Ch13_3_angles]
is_anga_distinct [in Ch13_3_angles]
is_anga_conga_is_anga [in Ch13_3_angles]
is_anga_conga [in Ch13_3_angles]
is_anga_to_is_ang [in Ch13_3_angles]
is_ang_distinct [in Ch13_3_angles]
is_ang_conga_is_ang [in Ch13_3_angles]
is_ang_conga [in Ch13_3_angles]
is_len_cong_is_len [in Ch13_2_length]
is_len_cong [in Ch13_2_length]
is_midpoint_id_2 [in Ch07_midpoint]
is_midpoint_id [in Ch07_midpoint]
is_midpoint_dec [in Ch07_midpoint]
is_image_spec_dec [in Ch10_line_reflexivity]
is_image_spec_triv [in Ch10_line_reflexivity]
is_image_rev [in Ch10_line_reflexivity]
is_image_spec_rev [in Ch10_line_reflexivity]
is_image_spec_col_cong [in Ch10_line_reflexivity]
is_image_col_cong [in Ch10_line_reflexivity]
is_image_is_image_spec [in Ch10_line_reflexivity]
is_to_ise [in vectors]
IT_trivial [in tarski_to_beeson]
IT_chara [in tarski_to_beeson]
K
ker_par [in project]ker_col [in project]
Kite_comm [in quadrilaterals]
L
lastCPIn [in arity]lastCPTl [in arity]
lastTailOK [in arity]
lcos_lg [in Ch13_4_cos]
lcos_per [in Ch13_4_cos]
lcos_const_o [in Ch13_4_cos]
lcos_not_lg_null [in Ch13_4_cos]
lcos_eql_lcos [in Ch13_4_cos]
lcos_lg_anga [in Ch13_4_cos]
lcos_const_cb [in Ch13_4_cos]
lcos_const_ab [in Ch13_4_cos]
lcos_const_a [in Ch13_4_cos]
lcos_lg_distincts [in Ch13_4_cos]
lcos_const [in Ch13_4_cos]
lcos_const1 [in Ch13_4_cos]
lcos_const0 [in Ch13_4_cos]
lcos_lg_not_null [in Ch13_4_cos]
lcos_lcos_col [in Ch13_5_Pappus_Pascal]
lcos_per_anga [in Ch13_5_Pappus_Pascal]
lcos_eq_lcos3_eq [in Ch13_5_Pappus_Pascal]
lcos_eq_lcos2_eq [in Ch13_5_Pappus_Pascal]
lcos_eq_trans [in Ch13_5_Pappus_Pascal]
lcos_eq_sym [in Ch13_5_Pappus_Pascal]
lcos_eq_refl [in Ch13_5_Pappus_Pascal]
lcos_exists [in Ch13_5_Pappus_Pascal]
lcos_eqa_lcos [in Ch13_5_Pappus_Pascal]
lcos2_lcos [in Ch13_5_Pappus_Pascal]
lcos2_eq_lcos3_eq [in Ch13_5_Pappus_Pascal]
lcos2_lg_not_null [in Ch13_5_Pappus_Pascal]
lcos2_eq_trans [in Ch13_5_Pappus_Pascal]
lcos2_lg_anga [in Ch13_5_Pappus_Pascal]
lcos2_eql_lcos2 [in Ch13_5_Pappus_Pascal]
lcos2_unicity [in Ch13_5_Pappus_Pascal]
lcos2_eq_sym [in Ch13_5_Pappus_Pascal]
lcos2_eq_refl [in Ch13_5_Pappus_Pascal]
lcos2_exists' [in Ch13_5_Pappus_Pascal]
lcos2_exists [in Ch13_5_Pappus_Pascal]
lcos2_comm [in Ch13_5_Pappus_Pascal]
lcos3_lcos2 [in Ch13_5_Pappus_Pascal]
lcos3_eq_trans [in Ch13_5_Pappus_Pascal]
lcos3_lg_not_null [in Ch13_5_Pappus_Pascal]
lcos3_lg_anga [in Ch13_5_Pappus_Pascal]
lcos3_eql_lcos3 [in Ch13_5_Pappus_Pascal]
lcos3_unicity [in Ch13_5_Pappus_Pascal]
lcos3_eq_sym [in Ch13_5_Pappus_Pascal]
lcos3_eq_refl [in Ch13_5_Pappus_Pascal]
lcos3_exists [in Ch13_5_Pappus_Pascal]
lcos3_permut2 [in Ch13_5_Pappus_Pascal]
lcos3_permut1 [in Ch13_5_Pappus_Pascal]
lcos3_permut3 [in Ch13_5_Pappus_Pascal]
lcos3_lcos_2_1 [in Ch13_5_Pappus_Pascal]
lcos3_lcos_1_2 [in Ch13_5_Pappus_Pascal]
lea_cases [in Ch12_parallel_inter_dec]
lea_in_angle [in Ch13_1]
lea_acute_obtuse [in Ch11_angles]
lea_comm [in Ch11_angles]
lea_right_comm [in Ch11_angles]
lea_left_comm [in Ch11_angles]
lea_asym [in Ch11_angles]
lea_trans [in Ch11_angles]
lea_refl [in Ch11_angles]
lea_line [in Ch11_angles]
lengthOfCPToList [in arity]
le_cong_le [in orientation]
le_comm [in orientation]
le_right_comm [in orientation]
le_left_comm [in orientation]
le_bet [in Ch08_orthogonality]
le_cong_le [in quadrilaterals]
le_comm [in quadrilaterals]
le_right_comm [in quadrilaterals]
le_left_comm [in quadrilaterals]
le_comm [in Ch11_angles]
le_right_comm [in Ch11_angles]
le_left_comm [in Ch11_angles]
le_zero [in Ch05_bet_le]
le_cases [in Ch05_bet_le]
le_trivial [in Ch05_bet_le]
le_anti_symmetry [in Ch05_bet_le]
le_transitivity [in Ch05_bet_le]
le_reflexivity [in Ch05_bet_le]
lg_null_dec [in Ch13_2_length]
lg_null_trivial [in Ch13_2_length]
lg_null_instance [in Ch13_2_length]
lg_sym [in Ch13_2_length]
lg_cong_lg [in Ch13_2_length]
lg_cong [in Ch13_2_length]
lg_exists [in Ch13_2_length]
line_dec [in Ch12_parallel]
listInd [in arity]
ListToCPTl [in arity]
lower_dim [in tarski_to_beeson]
lower_dim_B [in tarski_to_beeson]
ltac_something_show [in general_tactics]
ltac_something_hide [in general_tactics]
ltac_something_eq [in general_tactics]
lta_diff [in Ch11_angles]
lta_not_conga [in Ch11_angles]
lta_comm [in Ch11_angles]
lta_right_comm [in Ch11_angles]
lta_left_comm [in Ch11_angles]
lta_trans [in Ch11_angles]
lt_comm [in Ch11_angles]
lt_left_comm [in Ch11_angles]
lt_right_comm [in Ch11_angles]
l_3_9_4 [in Ch03_bet]
l10_16 [in Ch10_line_reflexivity]
l10_15 [in Ch10_line_reflexivity]
l10_14 [in Ch10_line_reflexivity]
l10_12 [in Ch10_line_reflexivity]
l10_10 [in Ch10_line_reflexivity]
l10_10_spec [in Ch10_line_reflexivity]
l10_8 [in Ch10_line_reflexivity]
l10_7 [in Ch10_line_reflexivity]
l10_6_existence [in Ch10_line_reflexivity]
l10_6_existence_spec [in Ch10_line_reflexivity]
l10_6_unicity [in Ch10_line_reflexivity]
l10_5 [in Ch10_line_reflexivity]
l10_4 [in Ch10_line_reflexivity]
l10_4_spec [in Ch10_line_reflexivity]
l10_2_existence [in Ch10_line_reflexivity]
l10_2_existence_spec [in Ch10_line_reflexivity]
l10_2_unicity [in Ch10_line_reflexivity]
l11_53 [in Ch11_angles]
l11_52 [in Ch11_angles]
l11_51 [in Ch11_angles]
l11_50_2 [in Ch11_angles]
l11_50_1 [in Ch11_angles]
l11_49 [in Ch11_angles]
l11_47 [in Ch11_angles]
l11_46 [in Ch11_angles]
l11_44_2 [in Ch11_angles]
l11_44_1 [in Ch11_angles]
l11_44_2_b [in Ch11_angles]
l11_44_1_b [in Ch11_angles]
l11_44_2_a [in Ch11_angles]
l11_44_1_a [in Ch11_angles]
l11_43 [in Ch11_angles]
l11_43_aux [in Ch11_angles]
l11_41 [in Ch11_angles]
l11_41_aux [in Ch11_angles]
l11_36 [in Ch11_angles]
l11_31_2 [in Ch11_angles]
l11_31_1 [in Ch11_angles]
l11_30 [in Ch11_angles]
l11_29_b [in Ch11_angles]
l11_29_a [in Ch11_angles]
l11_28 [in Ch11_angles]
l11_25 [in Ch11_angles]
l11_25_aux [in Ch11_angles]
l11_24 [in Ch11_angles]
l11_22 [in Ch11_angles]
l11_22b [in Ch11_angles]
l11_22a [in Ch11_angles]
l11_22_bet [in Ch11_angles]
l11_19 [in Ch11_angles]
l11_15 [in Ch11_angles]
l11_22_aux [in Ch11_angles]
l11_21_b [in Ch11_angles]
l11_21_a [in Ch11_angles]
l11_18_2 [in Ch11_angles]
l11_18_1 [in Ch11_angles]
l11_17 [in Ch11_angles]
l11_16 [in Ch11_angles]
l11_14 [in Ch11_angles]
l11_13 [in Ch11_angles]
l11_10 [in Ch11_angles]
l11_4_2 [in Ch11_angles]
l11_4_1 [in Ch11_angles]
l11_3_bis [in Ch11_angles]
l11_aux [in Ch11_angles]
l11_3 [in Ch11_angles]
l12_23 [in Ch12_parallel_inter_dec]
l12_22 [in Ch12_parallel_inter_dec]
l12_22_a [in Ch12_parallel_inter_dec]
l12_21 [in Ch12_parallel_inter_dec]
l12_21_a [in Ch12_parallel_inter_dec]
l12_20 [in Ch12_parallel_inter_dec]
l12_20_bis [in Ch12_parallel_inter_dec]
l12_19 [in Ch12_parallel_inter_dec]
l12_16 [in Ch12_parallel_inter_dec]
l12_22_b [in Ch12_parallel]
l12_22_aux [in Ch12_parallel]
l12_21_b [in Ch12_parallel]
l12_18 [in Ch12_parallel]
l12_18_d [in Ch12_parallel]
l12_18_c [in Ch12_parallel]
l12_18_b [in Ch12_parallel]
l12_18_a [in Ch12_parallel]
l12_17 [in Ch12_parallel]
l12_9 [in Ch12_parallel]
l12_6 [in Ch12_parallel]
l13_7 [in Ch13_4_cos]
l13_6 [in Ch13_4_cos]
l13_14 [in Ch13_5_Pappus_Pascal]
l13_11 [in Ch13_5_Pappus_Pascal]
l13_10 [in Ch13_5_Pappus_Pascal]
l13_10_aux5 [in Ch13_5_Pappus_Pascal]
l13_10_aux4 [in Ch13_5_Pappus_Pascal]
l13_10_aux3 [in Ch13_5_Pappus_Pascal]
l13_6_bis [in Ch13_5_Pappus_Pascal]
l13_10_aux2 [in Ch13_5_Pappus_Pascal]
l13_10_aux1 [in Ch13_5_Pappus_Pascal]
l13_19_par [in Ch13_6_Desargues_Hessenberg]
l13_19_par_aux [in Ch13_6_Desargues_Hessenberg]
l13_19 [in Ch13_6_Desargues_Hessenberg]
l13_19_aux [in Ch13_6_Desargues_Hessenberg]
l13_18 [in Ch13_6_Desargues_Hessenberg]
l13_18_3 [in Ch13_6_Desargues_Hessenberg]
l13_18_2 [in Ch13_6_Desargues_Hessenberg]
l13_15_par [in Ch13_6_Desargues_Hessenberg]
l13_15 [in Ch13_6_Desargues_Hessenberg]
l13_15_2 [in Ch13_6_Desargues_Hessenberg]
l13_15_2_aux [in Ch13_6_Desargues_Hessenberg]
l13_15_1 [in Ch13_6_Desargues_Hessenberg]
l13_8 [in Ch13_1]
l13_2 [in Ch13_1]
l13_2_1 [in Ch13_1]
l13_1 [in Ch13_1]
l2_11_b [in Ch03_bet]
l2_11 [in Ch02_cong]
l3_17 [in Ch03_bet]
l4_3_1 [in Ch08_orthogonality]
l4_19 [in Ch04_col]
l4_18 [in Ch04_col]
l4_17 [in Ch04_col]
l4_16 [in Ch04_col]
l4_14 [in Ch04_col]
l4_13 [in Ch04_col]
l4_6 [in Ch04_cong_bet]
l4_5 [in Ch04_cong_bet]
l4_3 [in Ch04_cong_bet]
l4_2 [in Ch04_cong_bet]
l5_12_b [in Ch11_angles]
l5_12_a [in Ch11_angles]
l5_6 [in Ch05_bet_le]
l5_5_2 [in Ch05_bet_le]
l5_5_1 [in Ch05_bet_le]
l5_3 [in Ch05_bet_le]
l5_2 [in Ch05_bet_le]
l5_1 [in Ch05_bet_le]
l6_25 [in Ch06_out_lines]
l6_21 [in Ch06_out_lines]
l6_16_1 [in Ch06_out_lines]
l6_13_2 [in Ch06_out_lines]
l6_13_1 [in Ch06_out_lines]
l6_11_existence [in Ch06_out_lines]
l6_11_unicity [in Ch06_out_lines]
l6_7 [in Ch06_out_lines]
l6_6 [in Ch06_out_lines]
l6_4_2 [in Ch06_out_lines]
l6_4_1 [in Ch06_out_lines]
l6_3_2 [in Ch06_out_lines]
l6_3_1 [in Ch06_out_lines]
l6_2 [in Ch06_out_lines]
l6_7_1 [in Ch12_parallel]
l7_25 [in Ch07_midpoint]
l7_22 [in Ch07_midpoint]
l7_22_aux [in Ch07_midpoint]
l7_21 [in Ch07_midpoint]
l7_20 [in Ch07_midpoint]
l7_17_bis [in Ch07_midpoint]
l7_17 [in Ch07_midpoint]
l7_16 [in Ch07_midpoint]
l7_15 [in Ch07_midpoint]
l7_13 [in Ch07_midpoint]
l7_9 [in Ch07_midpoint]
l7_3_2 [in Ch07_midpoint]
l7_3 [in Ch07_midpoint]
l7_2 [in Ch07_midpoint]
l8_24 [in Ch08_orthogonality]
l8_22_bis [in Ch08_orthogonality]
l8_22 [in Ch08_orthogonality]
l8_21 [in Ch08_orthogonality]
l8_21_aux [in Ch08_orthogonality]
l8_18_existence [in Ch08_orthogonality]
l8_20_2 [in Ch08_orthogonality]
l8_20_1 [in Ch08_orthogonality]
l8_18_unicity [in Ch08_orthogonality]
l8_16_2 [in Ch08_orthogonality]
l8_16_1 [in Ch08_orthogonality]
l8_15_2 [in Ch08_orthogonality]
l8_15_1 [in Ch08_orthogonality]
l8_14_3 [in Ch08_orthogonality]
l8_14_2_2 [in Ch08_orthogonality]
l8_14_2_1b_bis [in Ch08_orthogonality]
l8_14_2_1b [in Ch08_orthogonality]
l8_14_2_1a [in Ch08_orthogonality]
l8_14_1 [in Ch08_orthogonality]
l8_13_2 [in Ch08_orthogonality]
l8_12 [in Ch08_orthogonality]
l8_10 [in Ch08_orthogonality]
l8_9 [in Ch08_orthogonality]
l8_8 [in Ch08_orthogonality]
l8_7 [in Ch08_orthogonality]
l8_6 [in Ch08_orthogonality]
l8_5 [in Ch08_orthogonality]
l8_4 [in Ch08_orthogonality]
l8_3 [in Ch08_orthogonality]
l8_2 [in Ch08_orthogonality]
l9_19 [in Ch09_plane]
l9_18 [in Ch09_plane]
l9_17 [in Ch09_plane]
l9_10 [in Ch09_plane]
l9_9_bis [in Ch09_plane]
l9_9 [in Ch09_plane]
l9_8_2 [in Ch09_plane]
l9_8_1 [in Ch09_plane]
l9_5 [in Ch09_plane]
l9_4_2 [in Ch09_plane]
l9_4_2_aux [in Ch09_plane]
l9_4_1 [in Ch09_plane]
l9_4_1_aux [in Ch09_plane]
l9_3 [in Ch09_plane]
l9_2 [in Ch09_plane]
l9_31 [in Ch11_angles]
M
Mcong_left_commutativity [in tarski_to_makarios]Mcong_symmetry [in tarski_to_makarios]
Mcong_reflexivity [in tarski_to_makarios]
midpoint_preserves_bet [in orientation]
midpoint_par_strict [in orientation]
midpoint_par [in orientation]
midpoint_col [in orientation]
midpoint_existence [in Ch08_orthogonality]
midpoint_existence_aux [in Ch08_orthogonality]
midpoint_cong_unicity [in quadrilaterals]
midpoint_preserves_bet [in quadrilaterals]
midpoint_par_strict [in quadrilaterals]
midpoint_par [in quadrilaterals]
midpoint_midpoint_col [in quadrilaterals]
midpoint_not_midpoint [in Ch07_midpoint]
midpoint_cong [in Ch07_midpoint]
midpoint_col [in Ch07_midpoint]
midpoint_bet [in Ch07_midpoint]
midpoint_def [in Ch07_midpoint]
midpoint_distinct_3 [in Ch07_midpoint]
midpoint_distinct_2 [in Ch07_midpoint]
midpoint_distinct_1 [in Ch07_midpoint]
midpoint_preserves_per [in Ch10_line_reflexivity]
midpoint_preserves_image [in Ch10_line_reflexivity]
midpoint_thales_reci [in midpoint_thales]
midpoint_thales [in midpoint_thales]
midpoint_preserves_out [in Ch12_parallel]
Mid_tagged_Mid [in Tagged_predicates]
Mid_Mid_tagged [in Tagged_predicates]
mid_two_sides [in Ch09_plane]
mid_preserves_col [in Ch09_plane]
mid_plg_2 [in quadrilaterals]
mid_plg_1 [in quadrilaterals]
mid_plg [in quadrilaterals]
mid_plgf [in quadrilaterals]
mid_plgf_aux [in quadrilaterals]
mid_plgs [in quadrilaterals]
mid_par_cong [in quadrilaterals]
mid_par_cong2 [in quadrilaterals]
mid_par_cong1 [in quadrilaterals]
Mid_perm [in Ch07_midpoint]
Mid_cases [in Ch07_midpoint]
mid_eqv [in vectors]
minus_n1_n2_0 [in arity]
minus_n_0 [in arity]
N
NColB_NColOrEq [in tarski_to_beeson]NColB_NDiffCol [in tarski_to_beeson]
NCol_tagged_NCol [in Tagged_predicates]
NCol_NCol_tagged [in Tagged_predicates]
NCol_perm [in Ch04_col]
NCol_cases [in Ch04_col]
ncol_conga_ncol [in Ch11_angles]
not_par_pars_not_cong [in quadrilaterals_inter_dec]
not_two_sides_id [in Ch09_plane]
not_null_not_col [in Ch13_3_angles]
not_flat_ang_def_equiv [in Ch13_3_angles]
not_null_ang_def_equiv [in Ch13_3_angles]
not_null_ang_ang [in Ch13_3_angles]
not_cong_is_anga1 [in Ch13_3_angles]
not_conga_is_anga [in Ch13_3_angles]
not_cong_is_ang1 [in Ch13_3_angles]
not_conga_is_ang [in Ch13_3_angles]
not_conga_not_ang [in Ch13_3_angles]
not_cong_is_len1 [in Ch13_2_length]
not_cong_is_len [in Ch13_2_length]
not_col_exists [in quadrilaterals]
not_col_sym_not_col [in quadrilaterals]
not_col_distincts [in Ch04_col]
not_col_permutation_5 [in Ch04_col]
not_col_permutation_4 [in Ch04_col]
not_col_permutation_3 [in Ch04_col]
not_col_permutation_2 [in Ch04_col]
not_col_permutation_1 [in Ch04_col]
not_col_par_col2_diff [in orthocenter]
not_par_one_not_par [in Ch12_parallel_inter_dec]
not_par_inter [in Ch12_parallel_inter_dec]
not_par_strict_inter_exists [in Ch12_parallel_inter_dec]
not_lta_gea [in Ch12_parallel_inter_dec]
not_one_side_two_sides [in Ch12_parallel_inter_dec]
not_par_other_side [in Ch12_parallel_inter_dec]
not_par_two_sides [in Ch12_parallel_inter_dec]
not_par_inter_exists [in Ch12_parallel_inter_dec]
not_col_exists [in Ch10_line_reflexivity]
not_lta_and_gta [in Ch11_angles]
not_gta_and_cong [in Ch11_angles]
not_lta_and_cong [in Ch11_angles]
not_and_lta [in Ch11_angles]
not_conga_sym [in Ch11_angles]
not_conga [in Ch11_angles]
not_two_sides_one_side [in Ch11_angles]
not_two_sides_one_side_aux [in Ch11_angles]
not_bet_and_out [in Ch11_angles]
not_out_bet [in Ch11_angles]
not_two_sides [in Ch11_angles]
not_bet_out [in Ch11_angles]
not_par_inter_unicity [in Ch12_parallel]
not_par_not_col [in Ch12_parallel]
not_strict_par [in Ch12_parallel]
not_strict_par2 [in Ch12_parallel]
not_strict_par1 [in Ch12_parallel]
not_par_strict_id [in Ch12_parallel]
nthCircPermNAny [in arity]
nthCircPerm1 [in arity]
nthCircPerm1Eq [in arity]
nthCircPerm2 [in arity]
nthCircPerm2Eq [in arity]
nthCPTlOK [in arity]
nthCP01 [in arity]
nthEqOK [in arity]
nthFirst [in arity]
nthLast [in arity]
NT_NBet [in tarski_to_beeson]
null_lcos [in Ch13_4_cos]
null_lcos_eql [in Ch13_4_cos]
null_anga_null_anga' [in Ch13_3_angles]
null_anga [in Ch13_3_angles]
null_ang [in Ch13_3_angles]
null_len [in Ch13_2_length]
null_sum_eq [in vectors]
null_sum [in vectors]
null_vector [in vectors]
O
obtuse_not_acute [in Ch13_4_cos]obtuse_gea_obtuse [in Ch11_angles]
obtuse_sym [in Ch11_angles]
OCPALengthOK [in sets]
OCPIdempotent [in sets]
OCPOK [in sets]
OCPPerm [in sets]
OCPSortedAux [in sets]
OCPSortedTl [in sets]
OCPTlOK [in sets]
one_side_eqo [in orientation]
one_side_eq_o [in orientation]
one_side_same_side [in tarski_to_hilbert]
one_side_transitivity [in Ch09_plane]
one_side_symmetry [in Ch09_plane]
one_side_reflexivity [in Ch09_plane]
one_side_chara [in Ch09_plane]
one_side_dec [in Ch12_parallel_inter_dec]
one_or_two_sides [in Ch12_parallel_inter_dec]
one_side_not_col [in Ch11_angles]
one_side_col_out [in vectors]
opposite_sum [in vectors]
opp_not_same_dir [in vectors]
opp_dir_to_null [in vectors]
opp_dir_id [in vectors]
or_to_sumbool [in Epsilon]
or_lta_conga_gta [in Ch12_parallel_inter_dec]
or_lt_cong_gt [in Ch11_angles]
or_bet_out [in Ch11_angles]
osym_not_col [in Ch10_line_reflexivity]
os_cong_par_cong_par [in quadrilaterals_inter_dec]
os_out_os [in Ch13_1]
other_point_exists [in Ch12_parallel]
outer_transitivity_between [in Ch03_bet]
outer_transitivity_between2 [in Ch03_bet]
outer_pasch [in Ch09_plane]
outH_in_angleH_colH [in tarski_to_hilbert]
outH_out [in tarski_to_hilbert]
out_preserves_eqo [in orientation]
out_preserves_eqo1 [in orientation]
out_preserves_eq_o [in orientation]
out_trivial [in Ch06_out_lines]
out_col [in Ch06_out_lines]
out_distinct [in Ch06_out_lines]
out_diff2 [in Ch06_out_lines]
out_diff1 [in Ch06_out_lines]
out_dec [in Ch06_out_lines]
out_outH [in tarski_to_hilbert]
out_acute [in Ch13_4_cos]
out_out_anga [in Ch13_4_cos]
out_out_two_sides [in Ch09_plane]
out_null_anga [in Ch13_3_angles]
out_null_ang [in Ch13_3_angles]
out_len_eq [in Ch13_3_angles]
out_is_len_eq [in Ch13_3_angles]
out_two_sides_two_sides [in Ch11_angles]
out_bet_out_2 [in Ch11_angles]
out_bet_out_1 [in Ch11_angles]
out_one_side [in Ch11_angles]
out_conga_out [in Ch11_angles]
out_out_one_side [in Ch11_angles]
out_in_angle_out [in Ch11_angles]
out_in_angle [in Ch11_angles]
out_to_bet [in Ch11_angles]
out_conga [in Ch11_angles]
out_cong_cong [in Ch11_angles]
out_one_side_1 [in Ch12_parallel]
out2_bet_out [in Ch06_out_lines]
out2_out_2 [in Ch11_angles]
out2_out_1 [in Ch11_angles]
P
parallelogram_strict_midpoint [in quadrilaterals_inter_dec]parallelogram_strict_not_col_4 [in quadrilaterals_inter_dec]
parallelogram_strict_not_col_3 [in quadrilaterals_inter_dec]
parallelogram_strict_not_col_2 [in quadrilaterals_inter_dec]
parallelogram_equiv_plg [in quadrilaterals_inter_dec]
parallelogram_to_plg [in quadrilaterals_inter_dec]
parallelogram_strict_not_col [in quadrilaterals]
Parallelogram_strict_Parallelogram [in quadrilaterals]
parallel_2_plg [in quadrilaterals_inter_dec]
parallel_existence1 [in Ch12_parallel_inter_dec]
parallel_trans [in Ch12_parallel_inter_dec]
parallel_unicity [in Ch12_parallel_inter_dec]
parallel_unicity_aux [in Ch12_parallel_inter_dec]
parallel_existence_spec [in Ch12_parallel]
parallel_existence [in Ch12_parallel]
Para_Par [in tarski_to_hilbert]
pars_par_plg [in quadrilaterals_inter_dec]
pars_par_pars [in quadrilaterals_inter_dec]
par_col [in orientation]
par_cong_mid [in orientation]
par_strict_trans [in quadrilaterals_inter_dec]
par_cong3_rect [in quadrilaterals_inter_dec]
par_cong_plg_2 [in quadrilaterals_inter_dec]
par_cong_plg [in quadrilaterals_inter_dec]
par_cong_cong [in quadrilaterals_inter_dec]
par_perp_perp [in quadrilaterals_inter_dec]
par_2_plg [in quadrilaterals_inter_dec]
par_preserves_conga_os [in quadrilaterals_inter_dec]
par_preserves_conga_ts [in quadrilaterals_inter_dec]
par_cong_mid [in quadrilaterals_inter_dec]
par_strict_cong_mid1 [in quadrilaterals_inter_dec]
par_strict_cong_mid [in quadrilaterals_inter_dec]
par_cong_mid_os [in quadrilaterals_inter_dec]
par_cong_mid_ts [in quadrilaterals_inter_dec]
Par_tagged_Par [in Tagged_predicates]
Par_Par_tagged [in Tagged_predicates]
Par_strict_tagged_Par_strict [in Tagged_predicates]
Par_strict_Par_strict_tagged [in Tagged_predicates]
par_col_project [in project]
par_strict_not_col [in Ch12_parallel_inter_dec]
par_one_or_two_sides [in Ch12_parallel_inter_dec]
par_inter [in Ch12_parallel_inter_dec]
par_not_par [in Ch12_parallel_inter_dec]
Par_dec [in Ch12_parallel_inter_dec]
par_strict_all_one_side [in Ch12_parallel_inter_dec]
par_strict_one_side [in Ch12_parallel_inter_dec]
par_trans [in Ch12_parallel_inter_dec]
par_perp2 [in Ch13_1]
par_ts_same_dir [in vectors]
par_strict_distinct [in Ch12_parallel]
par_strict_par [in Ch12_parallel]
par_two_sides_two_sides [in Ch12_parallel]
par_distinct [in Ch12_parallel]
par_strict_col2_par_strict [in Ch12_parallel]
par_strict_col_par_strict [in Ch12_parallel]
par_col2_par [in Ch12_parallel]
par_col_par_2 [in Ch12_parallel]
par_not_col_strict [in Ch12_parallel]
par_distincts [in Ch12_parallel]
par_not_col [in Ch12_parallel]
par_col_par [in Ch12_parallel]
Par_strict_perm [in Ch12_parallel]
Par_strict_cases [in Ch12_parallel]
Par_perm [in Ch12_parallel]
Par_cases [in Ch12_parallel]
par_strict_comm [in Ch12_parallel]
par_strict_right_comm [in Ch12_parallel]
par_strict_left_comm [in Ch12_parallel]
par_comm [in Ch12_parallel]
par_right_comm [in Ch12_parallel]
par_left_comm [in Ch12_parallel]
par_symmetry [in Ch12_parallel]
par_strict_symmetry [in Ch12_parallel]
par_id_5 [in Ch12_parallel]
par_id_4 [in Ch12_parallel]
par_id_3 [in Ch12_parallel]
par_id_2 [in Ch12_parallel]
par_id_1 [in Ch12_parallel]
par_strict_not_col_4 [in Ch12_parallel]
par_strict_not_col_3 [in Ch12_parallel]
par_strict_not_col_2 [in Ch12_parallel]
par_strict_not_col_1 [in Ch12_parallel]
par_id [in Ch12_parallel]
par_strict_irreflexivity [in Ch12_parallel]
par_reflexivity [in Ch12_parallel]
par3_conga3 [in project]
pasch [in tarski_to_beeson]
pasch_col_case [in tarski_to_beeson]
perBAB [in Ch08_orthogonality]
PermCoappOK [in Permutations]
PermOK [in arity]
PermOKAux [in arity]
PermSorted [in sets]
PermWdOK [in Permutations]
perp_not_eq_3 [in orientation]
perp_3_rect [in quadrilaterals_inter_dec]
perp_3_perp [in quadrilaterals_inter_dec]
perp_rmb [in quadrilaterals_inter_dec]
Perp_tagged_Perp [in Tagged_predicates]
Perp_Perp_tagged [in Tagged_predicates]
Perp_in_tagged_Perp_in [in Tagged_predicates]
Perp_in_Perp_in_tagged [in Tagged_predicates]
perp_projp [in project]
perp_vector [in project]
perp_acute [in Ch13_4_cos]
perp_bet_obtuse [in Ch13_4_cos]
perp_obtuse_bet [in Ch13_4_cos]
perp_out__acute [in Ch13_4_cos]
perp_out_acute [in Ch13_4_cos]
perp_acute_out [in Ch13_4_cos]
perp_col2 [in Ch09_plane]
perp_in_perp [in Ch09_plane]
perp_in_col_perp_in [in Ch08_orthogonality]
perp_not_col2 [in Ch08_orthogonality]
perp_proj [in Ch08_orthogonality]
perp_in_perp [in Ch08_orthogonality]
perp_in_id [in Ch08_orthogonality]
perp_cong [in Ch08_orthogonality]
perp_not_eq_2 [in Ch08_orthogonality]
perp_not_eq_1 [in Ch08_orthogonality]
perp_col2 [in Ch08_orthogonality]
perp_col [in Ch08_orthogonality]
perp_per_2 [in Ch08_orthogonality]
perp_per_1 [in Ch08_orthogonality]
perp_perp_in [in Ch08_orthogonality]
perp_in_col [in Ch08_orthogonality]
perp_col1 [in Ch08_orthogonality]
Perp_in_perm [in Ch08_orthogonality]
Perp_in_cases [in Ch08_orthogonality]
Perp_perm [in Ch08_orthogonality]
Perp_cases [in Ch08_orthogonality]
perp_in_comm [in Ch08_orthogonality]
perp_in_right_comm [in Ch08_orthogonality]
perp_in_left_comm [in Ch08_orthogonality]
perp_in_sym [in Ch08_orthogonality]
perp_comm [in Ch08_orthogonality]
perp_right_comm [in Ch08_orthogonality]
perp_left_comm [in Ch08_orthogonality]
perp_col0 [in Ch08_orthogonality]
perp_sym [in Ch08_orthogonality]
perp_in_per [in Ch08_orthogonality]
perp_in_distinct [in Ch08_orthogonality]
perp_distinct [in Ch08_orthogonality]
Perp_in_dec [in Ch08_orthogonality]
perp_inter_perp_in [in Ch12_parallel_inter_dec]
perp_inter_exists [in Ch12_parallel_inter_dec]
perp_exists [in Ch10_line_reflexivity]
perp_not_col [in Ch10_line_reflexivity]
perp_mid_perp_bisect [in perp_bisect]
perp_bisect_is_on_perp_bisect [in perp_bisect]
perp_bisect_conc [in perp_bisect]
perp_bisect_cong [in perp_bisect]
perp_bisect_cong_2 [in perp_bisect]
perp_bisect_cong_1 [in perp_bisect]
perp_bisect_perp [in perp_bisect]
perp_in_per_4 [in perp_bisect]
perp_in_per_3 [in perp_bisect]
perp_in_per_2 [in perp_bisect]
perp_in_per_1 [in perp_bisect]
perp_bisect_sym_3 [in perp_bisect]
perp_bisect_sym_2 [in perp_bisect]
perp_bisect_sym_1 [in perp_bisect]
perp_vector1 [in Ch13_1]
perp_not_par [in Ch12_parallel]
perp_perp_col_col [in Ch12_parallel]
Perp_dec [in Ch12_parallel]
perp_perp_col [in Ch12_parallel]
perp2_preserves_bet1 [in Ch13_4_cos]
perp2_perp_in [in Ch13_1]
perp2_preserves_bet [in Ch13_1]
perp2_par [in Ch13_1]
perp2_trans [in Ch13_1]
perp2_comm [in Ch13_1]
perp2_right_comm [in Ch13_1]
perp2_left_comm [in Ch13_1]
perp2_sym [in Ch13_1]
perp2_refl [in Ch13_1]
per_one_side [in orientation]
per_preserves_bet [in orientation]
per_diff [in orientation]
per_preserves_bet_aux2 [in orientation]
per_preserves_bet_aux1 [in orientation]
per_id [in orientation]
per_proj [in orientation]
per_rmb [in quadrilaterals_inter_dec]
Per_tagged_Per [in Tagged_predicates]
Per_Per_tagged [in Tagged_predicates]
per_col_eq [in Ch09_plane]
per_mid_per [in Ch09_plane]
per_per_perp [in Ch13_5_Pappus_Pascal]
per_cong [in Ch08_orthogonality]
per_not_col [in Ch08_orthogonality]
per_not_colp [in Ch08_orthogonality]
per_perp [in Ch08_orthogonality]
per_perp_in [in Ch08_orthogonality]
per_col [in Ch08_orthogonality]
Per_perm [in Ch08_orthogonality]
Per_cases [in Ch08_orthogonality]
Per_dec [in Ch08_orthogonality]
per_per_cong_gen [in Ch10_line_reflexivity_2D]
per_per_cong [in Ch10_line_reflexivity_2D]
per_per_cong_1 [in Ch10_line_reflexivity_2D]
Per_mid_rectangle [in exercises]
per_double_cong [in Ch10_line_reflexivity]
per_per_perp [in Ch10_line_reflexivity]
per_per_col [in Ch10_line_reflexivity]
per_lt [in Ch13_1]
per_cong_mid [in Ch11_angles]
plgf_plgf_plgf [in quadrilaterals_inter_dec]
plgf_plgs_trans [in quadrilaterals_inter_dec]
plgf_rect_id [in quadrilaterals_inter_dec]
plgf_comm2 [in quadrilaterals_inter_dec]
plgf_bet [in quadrilaterals]
plgf_trivial [in quadrilaterals]
plgf_trivial_trans [in quadrilaterals]
plgf_trivial_neq [in quadrilaterals]
plgf_not_point [in quadrilaterals]
plgf_trivial2 [in quadrilaterals]
plgf_trivial1 [in quadrilaterals]
plgf_cong [in quadrilaterals]
plgf_not_comm [in quadrilaterals]
plgf_mid [in quadrilaterals]
plgf_irreflexive [in quadrilaterals]
plgf_sym [in quadrilaterals]
plgf_permut [in quadrilaterals]
plgf_out_plgf [in vectors]
plgf_plgf_bet [in vectors]
plgf3_mid [in quadrilaterals]
plgs_in_angle [in quadrilaterals_inter_dec]
plgs_pseudo_trans [in quadrilaterals_inter_dec]
plgs_trans_trivial [in quadrilaterals_inter_dec]
plgs_pars_2 [in quadrilaterals_inter_dec]
plgs_pars_1 [in quadrilaterals_inter_dec]
plgs_cong_2 [in quadrilaterals_inter_dec]
plgs_cong_1 [in quadrilaterals_inter_dec]
plgs_half_plgs [in quadrilaterals_inter_dec]
plgs_comm2 [in quadrilaterals_inter_dec]
plgs_half_plgs_aux [in quadrilaterals_inter_dec]
plgs_par_strict [in quadrilaterals_inter_dec]
plgs_two_sides [in quadrilaterals_inter_dec]
plgs_not_comm [in quadrilaterals_inter_dec]
plgs_mid [in quadrilaterals_inter_dec]
plgs_sym [in quadrilaterals_inter_dec]
plgs_permut [in quadrilaterals_inter_dec]
plgs_cong [in quadrilaterals_inter_dec]
plgs_existence [in quadrilaterals]
plgs_diff [in quadrilaterals]
plgs_not_col [in quadrilaterals]
plgs_one_side [in quadrilaterals]
plgs_irreflexive [in quadrilaterals]
plgs_plgs_bet [in vectors]
plgs_out_plgs [in vectors]
plg_pseudo_trans [in quadrilaterals_inter_dec]
plg_unicity [in quadrilaterals_inter_dec]
plg_par_2 [in quadrilaterals_inter_dec]
plg_par_1 [in quadrilaterals_inter_dec]
plg_par [in quadrilaterals_inter_dec]
plg_per_rect [in quadrilaterals_inter_dec]
plg_per_rect4 [in quadrilaterals_inter_dec]
plg_per_rect3 [in quadrilaterals_inter_dec]
plg_per_rect2 [in quadrilaterals_inter_dec]
plg_per_rect1 [in quadrilaterals_inter_dec]
plg_not_comm_2 [in quadrilaterals_inter_dec]
plg_not_comm_1 [in quadrilaterals_inter_dec]
Plg_perm [in quadrilaterals_inter_dec]
plg_cong_2 [in quadrilaterals_inter_dec]
plg_cong_1 [in quadrilaterals_inter_dec]
plg_comm2 [in quadrilaterals_inter_dec]
plg_conga [in quadrilaterals_inter_dec]
plg_not_comm [in quadrilaterals_inter_dec]
plg_mid [in quadrilaterals_inter_dec]
plg_sym [in quadrilaterals_inter_dec]
plg_permut [in quadrilaterals_inter_dec]
plg_conga1 [in quadrilaterals_inter_dec]
plg_cong [in quadrilaterals_inter_dec]
Plg_tagged_Plg [in Tagged_predicates]
Plg_Plg_tagged [in Tagged_predicates]
plg_existence [in quadrilaterals]
plg_bet1 [in quadrilaterals]
plg_col_plgf [in quadrilaterals]
plg_trivial1 [in quadrilaterals]
plg_trivial [in quadrilaterals]
plg_cong_rectangle [in quadrilaterals]
plg_to_parallelogram [in quadrilaterals]
plg_irreflexive [in quadrilaterals]
plg_opp_dir [in vectors]
plg_out_plg [in vectors]
plg_plg_bet [in vectors]
plus_n_1 [in arity]
plus_n_0 [in arity]
plus_0_n [in arity]
point_construction_different [in Ch03_bet]
positive_dec [in ColR]
PosOrder.leb_dec [in sets]
PosOrder.leb_total [in sets]
project_project_par [in project]
project_par_project [in project]
project_to_projp [in project]
project_preserves_eqv [in project]
project_idem [in project]
project_par_dir [in project]
project_par_eqv [in project]
project_preserves_bet [in project]
project_col_eq [in project]
project_existence [in project]
project_unicity [in project]
project_par [in project]
project_not_col [in project]
project_col [in project]
project_not_id [in project]
project_id [in project]
projp_idem [in project]
projp_preserves_eqv [in project]
projp_preserves_bet [in project]
projp_id [in project]
projp_project_to_perp [in project]
projp_to_project [in project]
projp_is_project_perp [in project]
projp_is_project [in project]
proj_preserves_bet [in orientation]
proj_preserves_bet1 [in orientation]
proj_diff_not_col_inv [in orientation]
proj_diff_not_col [in orientation]
proj_perp_id [in orientation]
proj_inv_exists [in orientation]
proj_diff [in orientation]
proj_id [in orientation]
proj_par_strict [in orientation]
proj_not_eq_not_col [in orientation]
proj_not_eq [in orientation]
proj_comm [in orientation]
proj_not_col [in orientation]
proj_par [in orientation]
proj_eq_col [in orientation]
proj_one_side [in orientation]
proj_col_proj [in orientation]
proj_col [in orientation]
proj_unicity [in orientation]
proj_per [in orientation]
proj_exists [in orientation]
proj_distinct [in project]
proj3_id [in orientation]
proj3_col [in orientation]
proper_9 [in ColR]
proper_8 [in ColR]
proper_7 [in ColR]
proper_6 [in ColR]
proper_5 [in ColR]
proper_4 [in ColR]
proper_3 [in ColR]
proper_2 [in ColR]
proper_1 [in ColR]
proper_0 [in ColR]
proper_00 [in ColR]
pseudo_trans [in tarski_to_coapp_theory]
Q
quasi_classic [in Epsilon]R
Rectangle_not_triv_2 [in quadrilaterals]Rectangle_triv [in quadrilaterals]
Rectangle_not_triv [in quadrilaterals]
Rectangle_Parallelogram [in quadrilaterals]
Rectangle_Plg [in quadrilaterals]
rect_per [in quadrilaterals_inter_dec]
rect_per4 [in quadrilaterals_inter_dec]
rect_per3 [in quadrilaterals_inter_dec]
rect_per2 [in quadrilaterals_inter_dec]
rect_per1 [in quadrilaterals_inter_dec]
rect_comm2 [in quadrilaterals_inter_dec]
rect_permut [in quadrilaterals_inter_dec]
rhombus_cong_square [in quadrilaterals]
Rhombus_Rectangle_Square [in quadrilaterals]
Rhombus_Plg [in quadrilaterals]
rmb_perp [in quadrilaterals_inter_dec]
rmb_per [in quadrilaterals_inter_dec]
rmb_cong [in quadrilaterals_inter_dec]
S
same_side_sym [in tarski_to_hilbert]same_side_trans [in tarski_to_hilbert]
same_side_one_side [in tarski_to_hilbert]
same_not_opp_dir [in vectors]
same_dir_to_null [in vectors]
same_dir_id [in vectors]
same_or_opp_dir [in vectors]
same_dir_dec [in vectors]
same_dir_comm [in vectors]
same_dir_trans [in vectors]
same_dir_sym [in vectors]
same_dir_null [in vectors]
same_dir_out1 [in vectors]
same_dir_out [in vectors]
same_dir_ts [in vectors]
same_dir_refl [in vectors]
segment_construction [in tarski_to_beeson]
segment_construction_B [in tarski_to_beeson]
segment_construction_0 [in Ch11_angles]
segment_construction_3 [in Ch11_angles]
segment_construction_2 [in Ch05_bet_le]
select_the_rw [in Epsilon]
select_the_ind [in Epsilon]
select_the_e [in Epsilon]
select_ind [in Epsilon]
select_e [in Epsilon]
SetOfPairsOfPositiveOrderedType.compare_spec [in sets]
SetOfPairsOfPositiveOrderedType.eqb_eq [in sets]
SetOfPairsOfPositiveOrderedType.lt_trans [in sets]
SetOfPairsOfPositiveOrderedType.lt_antiref [in sets]
SetOfPairsOfPositiveOrderedType.lt_irrefl [in sets]
SetOfTuplesOfPositiveOrderedType.compareListSpec [in sets]
SetOfTuplesOfPositiveOrderedType.compare_spec [in sets]
SetOfTuplesOfPositiveOrderedType.eqbListEqList [in sets]
SetOfTuplesOfPositiveOrderedType.eqb_eq [in sets]
SetOfTuplesOfPositiveOrderedType.eqListOK [in sets]
SetOfTuplesOfPositiveOrderedType.eqListRefl [in sets]
SetOfTuplesOfPositiveOrderedType.eqListSortOCP [in sets]
SetOfTuplesOfPositiveOrderedType.eqListSym [in sets]
SetOfTuplesOfPositiveOrderedType.eqListTrans [in sets]
SetOfTuplesOfPositiveOrderedType.lengthAtLeastOne [in sets]
SetOfTuplesOfPositiveOrderedType.lengthOne [in sets]
SetOfTuplesOfPositiveOrderedType.ltAntiref [in sets]
SetOfTuplesOfPositiveOrderedType.ltIrrefl [in sets]
SetOfTuplesOfPositiveOrderedType.ltListIrrefl [in sets]
SetOfTuplesOfPositiveOrderedType.ltListTrans [in sets]
SetOfTuplesOfPositiveOrderedType.ltTrans [in sets]
SetOfTuplesOfPositiveOrderedType.sortOK [in sets]
some_fun_ind [in Epsilon]
some_fun_e [in Epsilon]
sp_ok_empty [in ColR]
Square_Rhombus [in quadrilaterals_inter_dec]
square_perp_rectangle [in quadrilaterals_inter_dec]
Square_Parallelogram [in quadrilaterals]
Square_Rectangle [in quadrilaterals]
Square_not_triv_3 [in quadrilaterals]
Square_not_triv_2 [in quadrilaterals]
Square_not_triv [in quadrilaterals]
ss_ok_empty [in ColR]
subst_sp_ok [in ColR]
subst_ss_ok [in ColR]
sum_unicity [in vectors]
sum_exists [in vectors]
sum_sym [in vectors]
swap_diff [in Ch07_midpoint]
symmetric_point_ex_unicity [in construction_functions]
symmetric_point_unicity [in Ch07_midpoint]
symmetric_point_construction [in Ch07_midpoint]
symmetry_preserves_bet [in orientation]
symmetry_preseves_bet2 [in orientation]
symmetry_preseves_bet1 [in orientation]
symmetry_preserves_conga [in project]
symmetry_preserves_one_side [in quadrilaterals]
symmetry_preserves_two_sides [in quadrilaterals]
symmetry_preserves_bet [in quadrilaterals]
symmetry_preseves_bet2 [in quadrilaterals]
symmetry_preseves_bet1 [in quadrilaterals]
symmetry_preserves_midpoint [in Ch07_midpoint]
sym_preserve_diff [in Ch09_plane]
sym_sym [in Ch09_plane]
sym_par [in quadrilaterals]
T
test_col_ok [in ColR]the_fun_ind [in Epsilon]
the_fun_rw [in Epsilon]
the_fun_e [in Epsilon]
third_point [in Ch05_bet_le]
three_medians_intersect [in gravityCenter]
triangle_par [in project]
triangle_par_mid [in triangle_midpoints_theorems]
triangle_mid_par_cong [in triangle_midpoints_theorems]
triangle_mid_par [in triangle_midpoints_theorems]
triangle_mid_par_flat [in triangle_midpoints_theorems]
triangle_mid_par_flat_cong [in triangle_midpoints_theorems]
triangle_mid_par_flat_cong_2 [in triangle_midpoints_theorems]
triangle_mid_par_flat_cong_1 [in triangle_midpoints_theorems]
triangle_mid_par_flat_cong_aux [in triangle_midpoints_theorems]
triangle_mid_par_strict [in triangle_midpoints_theorems]
triangle_mid_par_strict_cong [in triangle_midpoints_theorems]
triangle_mid_par_strict_cong_simp [in triangle_midpoints_theorems]
triangle_mid_par_strict_cong_2 [in triangle_midpoints_theorems]
triangle_mid_par_strict_cong_1 [in triangle_midpoints_theorems]
triangle_mid_par_strict_cong_aux [in triangle_midpoints_theorems]
triangle_circumscription_implies_inter_dec [in perp_bisect]
triangle_mid_par [in Ch13_1]
ts_cong_par_cong_par [in quadrilaterals_inter_dec]
ts_per_per_ts [in Ch13_1]
ts_ts_os [in Ch13_1]
two_distinct_points [in Ch03_bet]
two_sides_dec [in Ch12_parallel_inter_dec]
two_sides_in_angle [in Ch11_angles]
two_sides_not_col [in Ch11_angles]
T_dec [in tarski_to_beeson]
T_Bet [in tarski_to_beeson]
t2_8 [in Ch06_out_lines]
V
vector_same_dir_cong [in vectors]vector_unicity [in vectors]
vector_construction_unicity [in vectors]
vector_construction [in vectors]
Section Index
A
AB_fixed [in Epsilon]Angles_5 [in Ch13_3_angles]
Angles_4 [in Ch13_3_angles]
Angles_3 [in Ch13_3_angles]
Angles_2 [in Ch13_3_angles]
Angles_1 [in Ch13_3_angles]
B
Beeson_2 [in Ch03_bet]Beeson_1 [in Ch03_bet]
C
Ch12 [in orientation]Circumcenter [in circumcenter]
Col_refl [in ColR]
Cosinus [in Ch13_4_cos]
D
definite_description [in Epsilon]Desargues_Hessenberg [in Ch13_6_Desargues_Hessenberg]
E
Euclid [in perp_bisect]Exercises [in exercises]
G
GravityCenter [in gravityCenter]H
Hilbert_to_Tarski [in tarski_to_hilbert]I
Intuitionistic_Tarski_to_Tarski [in tarski_to_beeson]L
Length_4 [in Ch13_2_length]Length_3 [in Ch13_2_length]
Length_2 [in Ch13_2_length]
Length_1 [in Ch13_2_length]
L13 [in Ch13_1]
M
Makarios_variant_to_Tarski83 [in tarski_to_makarios]O
Orthocenter [in orthocenter]P
Pappus_Pascal [in Ch13_5_Pappus_Pascal]Permutations [in Permutations]
PerpBisect_3 [in perp_bisect]
PerpBisect_2 [in perp_bisect]
PerpBisect_1 [in perp_bisect]
Projections [in project]
Proof_of_eq_stability_in_IT [in tarski_to_beeson]
Q
Quadrilateral [in quadrilaterals]Quadrilateral_inter_dec_3 [in quadrilaterals_inter_dec]
Quadrilateral_inter_dec_2 [in quadrilaterals_inter_dec]
Quadrilateral_inter_dec_1 [in quadrilaterals_inter_dec]
T
T [in construction_functions]T [in tarski_to_hilbert]
Tagged_predicates [in Tagged_predicates]
Tarski_is_a_Coapp_theory [in tarski_to_coapp_theory]
Tarski_is_a_Col_theory [in tarski_to_col_theory]
Tarski_to_intuitionistic_Tarski [in tarski_to_beeson]
Tarski83_to_Makarios_variant [in tarski_to_makarios]
TriangleMidpointsTheorems [in triangle_midpoints_theorems]
Triangles [in triangles]
Triangles.ABC [in triangles]
T_42 [in midpoint_thales]
T1_3 [in Ch02_cong]
T1_2 [in Ch02_cong]
T1_1 [in Ch02_cong]
T10 [in Ch10_line_reflexivity_2D]
T10 [in Ch10_line_reflexivity]
T11 [in Ch11_angles]
T12_3 [in Ch12_parallel]
T12_2 [in Ch12_parallel]
T12_1 [in Ch12_parallel]
T13 [in Ch12_parallel_inter_dec]
T2_5 [in Ch03_bet]
T2_4 [in Ch03_bet]
T2_3 [in Ch03_bet]
T2_2 [in Ch03_bet]
T2_1 [in Ch03_bet]
T3 [in Ch04_cong_bet]
T4_4 [in Ch04_col]
T4_3 [in Ch04_col]
T4_2 [in Ch04_col]
T4_1 [in Ch04_col]
T5 [in Ch05_bet_le]
T6_2 [in Ch06_out_lines]
T6_1 [in Ch06_out_lines]
T7_2 [in Ch07_midpoint]
T7_1 [in Ch07_midpoint]
T8_5 [in Ch08_orthogonality]
T8_4 [in Ch08_orthogonality]
T8_3 [in Ch08_orthogonality]
T8_2 [in Ch08_orthogonality]
T8_1 [in Ch08_orthogonality]
T9 [in Ch09_plane]
U
UnitTests [in unit_tests]V
Vectors [in vectors]Notation Index
L
_ =l= _ [in Ch13_2_length]T
_ =h= _ (type_scope) [in tarski_to_hilbert]_ =l= _ (type_scope) [in tarski_to_hilbert]
other
Something [in general_tactics]Constructor Index
B
build_couple [in aux]build_triple [in aux]
Definition Index
A
acute [in Ch11_angles]allButLastCP [in arity]
ang [in Ch13_3_angles]
anga [in Ch13_3_angles]
angle [in tarski_to_hilbert]
Angle [in tarski_to_hilbert]
angle [in Ch13_3_angles]
anglea [in Ch13_3_angles]
app [in arity]
app_2_n [in arity]
app_1_n [in arity]
app_n_1 [in arity]
arity [in arity]
B
BetH [in tarski_to_beeson]BetT [in tarski_to_beeson]
Between_H [in tarski_to_hilbert]
Bet_4 [in Ch03_bet]
Bet_tagged [in Tagged_predicates]
C
cartesianPower [in arity]cartesianPowerAux [in arity]
choice_fun [in Epsilon]
circPermNCP [in arity]
Col [in Ch03_bet]
col [in tarski_to_coapp_theory]
ColB [in tarski_to_beeson]
Col_tagged [in ColR]
Col_tagged [in Tagged_predicates]
Col_H [in tarski_to_hilbert]
Conga [in Ch11_angles]
Conga_3 [in project]
Cong_tagged [in Tagged_predicates]
Cong_3 [in Ch02_cong]
cong_preserves_le [in Ch11_angles]
consHeadCP [in arity]
consTailCP [in arity]
coplanar [in Ch10_line_reflexivity]
coplanar [in Ch12_parallel]
CPPair [in arity]
CPToList [in arity]
cut [in tarski_to_hilbert]
D
diff [in tarski_to_coapp_theory]Diff_tagged [in ColR]
Diff_tagged [in Tagged_predicates]
disjoint [in tarski_to_hilbert]
Distincts [in Ch11_angles]
DistLn [in Ch08_orthogonality]
E
epsilon_extensionality [in Epsilon]Eq [in tarski_to_hilbert]
eqA [in Ch13_3_angles]
eqA' [in Ch13_3_angles]
eqL [in Ch13_2_length]
eqo [in orientation]
eqop [in ColR]
eqopp [in ColR]
equilateral [in triangles]
equilateral_strict [in triangles]
eqV [in vectors]
eq_o [in orientation]
eq_tagged [in ColR]
exists_witness [in ColR]
F
fixLastCP [in arity]FSC [in Ch04_col]
fstpp [in sets]
fst_sp [in ColR]
fst_ss [in ColR]
functional [in Epsilon]
G
ge [in Ch05_bet_le]gea [in Ch11_angles]
get_suitable_pair_of_sets [in ColR]
get_suitable_pair_of_sets_aux [in ColR]
gravity_center [in construction_functions]
gt [in Ch05_bet_le]
gta [in Ch11_angles]
H
have_pair_distinct_points [in ColR]Hcong [in tarski_to_hilbert]
Hconga [in tarski_to_hilbert]
headCP [in arity]
hEq [in tarski_to_hilbert]
hlin [in tarski_to_hilbert]
HLine [in tarski_to_hilbert]
hline_construction [in tarski_to_hilbert]
I
IFSC [in Ch04_cong_bet]InAngle [in Ch11_angles]
InAngleH [in tarski_to_hilbert]
Incident [in tarski_to_hilbert]
IncidentH [in tarski_to_hilbert]
InCP [in arity]
inter [in Ch12_parallel]
interp [in ColR]
iota [in Epsilon]
iota_fun [in Epsilon]
isosceles [in triangles]
is_gravity_center [in gravityCenter]
is_symmetric [in Ch09_plane]
is_null_anga' [in Ch13_3_angles]
is_null_anga [in Ch13_3_angles]
is_flat_ang' [in Ch13_3_angles]
is_null_ang' [in Ch13_3_angles]
is_flat_ang [in Ch13_3_angles]
is_null_ang [in Ch13_3_angles]
is_anga [in Ch13_3_angles]
is_ang [in Ch13_3_angles]
is_len [in Ch13_2_length]
is_circumcenter [in circumcenter]
is_midpoint [in Ch07_midpoint]
is_orthocenter [in orthocenter]
is_image_spec_in_gen [in Ch10_line_reflexivity]
is_image_spec_in [in Ch10_line_reflexivity]
is_image [in Ch10_line_reflexivity]
is_image_spec [in Ch10_line_reflexivity]
is_on_perp_bisect [in perp_bisect]
is_sum_exists [in vectors]
is_sum [in vectors]
K
Kite [in quadrilaterals]L
lastCP [in arity]lcos [in Ch13_4_cos]
lcos_eq [in Ch13_5_Pappus_Pascal]
lcos2 [in Ch13_5_Pappus_Pascal]
lcos2_eq [in Ch13_5_Pappus_Pascal]
lcos3 [in Ch13_5_Pappus_Pascal]
lcos3_eq [in Ch13_5_Pappus_Pascal]
le [in Ch05_bet_le]
lea [in Ch11_angles]
lg [in Ch13_2_length]
lg_null [in Ch13_2_length]
Lin [in tarski_to_hilbert]
Line [in tarski_to_hilbert]
line_of_hline [in tarski_to_hilbert]
ListToCP [in arity]
list_assoc_inv [in ColR]
long [in Ch13_2_length]
lt [in Ch05_bet_le]
lta [in Ch11_angles]
ltac_something [in general_tactics]
M
Mid_tagged [in Tagged_predicates]N
NCol_tagged [in Tagged_predicates]new_pair_2 [in ColR]
new_pair_1 [in ColR]
not_null_anga [in Ch13_3_angles]
not_flat_ang' [in Ch13_3_angles]
not_null_ang' [in Ch13_3_angles]
not_flat_ang [in Ch13_3_angles]
not_null_ang [in Ch13_3_angles]
nthCP [in arity]
O
obtuse [in Ch11_angles]OCP [in sets]
OCPAux [in sets]
OFSC [in Ch02_cong]
one_side [in Ch09_plane]
opp_dir [in vectors]
out [in Ch06_out_lines]
outH [in tarski_to_hilbert]
P
Par [in Ch12_parallel]Para [in tarski_to_hilbert]
Parallelogram [in quadrilaterals]
Parallelogram_flat [in quadrilaterals]
Parallelogram_strict [in quadrilaterals]
partition_sp_2 [in ColR]
partition_sp_1 [in ColR]
partition_ss [in ColR]
Par_tagged [in Tagged_predicates]
Par_strict_tagged [in Tagged_predicates]
Par_strict [in Ch12_parallel]
Per [in Ch08_orthogonality]
Perp [in Ch08_orthogonality]
Perp_tagged [in Tagged_predicates]
Perp_in_tagged [in Tagged_predicates]
Perp_in [in Ch08_orthogonality]
perp_bisect [in perp_bisect]
Perp2 [in Ch13_1]
Per_tagged [in Tagged_predicates]
Plg [in quadrilaterals]
Plg_tagged [in Tagged_predicates]
PosOrder.leb [in sets]
PosOrder.t [in sets]
proj [in orientation]
project [in project]
projp [in project]
R
Rectangle [in quadrilaterals]restricted_epsilon_extensionality [in Epsilon]
Rhombus [in quadrilaterals]
S
same_side [in tarski_to_hilbert]same_side_scott [in tarski_to_hilbert]
same_dir [in vectors]
select [in Epsilon]
select_the [in Epsilon]
SetOfPairsOfPositiveOrderedType.compare [in sets]
SetOfPairsOfPositiveOrderedType.eq [in sets]
SetOfPairsOfPositiveOrderedType.eqb [in sets]
SetOfPairsOfPositiveOrderedType.lt [in sets]
SetOfPairsOfPositiveOrderedType.t [in sets]
SetOfSetsOfPositiveOrderedType.compare [in sets]
SetOfSetsOfPositiveOrderedType.compare_spec [in sets]
SetOfSetsOfPositiveOrderedType.eq [in sets]
SetOfSetsOfPositiveOrderedType.eqb [in sets]
SetOfSetsOfPositiveOrderedType.eqb_eq [in sets]
SetOfSetsOfPositiveOrderedType.lt [in sets]
SetOfSetsOfPositiveOrderedType.t [in sets]
SetOfTuplesOfPositiveOrderedType.compare [in sets]
SetOfTuplesOfPositiveOrderedType.compareList [in sets]
SetOfTuplesOfPositiveOrderedType.eq [in sets]
SetOfTuplesOfPositiveOrderedType.eqb [in sets]
SetOfTuplesOfPositiveOrderedType.eqbList [in sets]
SetOfTuplesOfPositiveOrderedType.eqList [in sets]
SetOfTuplesOfPositiveOrderedType.lt [in sets]
SetOfTuplesOfPositiveOrderedType.ltList [in sets]
SetOfTuplesOfPositiveOrderedType.t [in sets]
sndpp [in sets]
snd_sp [in ColR]
snd_ss [in ColR]
some_fun [in Epsilon]
sp_ok [in ColR]
Square [in quadrilaterals]
ss_ok [in ColR]
subst_in_sp [in ColR]
subst_in_sp_aux_2 [in ColR]
subst_in_sp_aux_1 [in ColR]
subst_in_ss [in ColR]
subst_in_ss_aux [in ColR]
subst_in_set [in ColR]
symmetric_point [in construction_functions]
T
T [in tarski_to_beeson]tailCP [in arity]
tailCPbis [in arity]
tailDefaultCP [in arity]
tau [in Epsilon]
test_col [in ColR]
the_fun [in Epsilon]
two_sides [in Ch09_plane]
U
unspec [in Epsilon]Module Index
P
PosOrder [in sets]PosSort [in sets]
S
S [in sets]SetOfPairsOfPositiveOrderedType [in sets]
SetOfSetsOfPositiveOrderedType [in sets]
SetOfTuplesOfPositiveOrderedType [in sets]
SP [in sets]
SPWEqP [in ColR]
SS [in sets]
SSWEqP [in ColR]
SSWP [in ColR]
ST [in sets]
SWP [in sets]
Variable Index
A
AB_fixed.B [in Epsilon]AB_fixed.A [in Epsilon]
B
Beeson_2.Bet_stability [in Ch03_bet]Beeson_1.Cong_stability [in Ch03_bet]
T
Triangles.ABC.A [in triangles]Triangles.ABC.B [in triangles]
Triangles.ABC.C [in triangles]
Library Index
A
arityaux
C
Ch02_congCh03_bet
Ch04_cong_bet
Ch04_col
Ch05_bet_le
Ch06_out_lines
Ch07_midpoint
Ch08_orthogonality
Ch09_plane
Ch10_line_reflexivity
Ch10_line_reflexivity_2D
Ch11_angles
Ch12_parallel_inter_dec
Ch12_parallel
Ch13_3_angles
Ch13_2_length
Ch13_6_Desargues_Hessenberg
Ch13_4_cos
Ch13_1
Ch13_5_Pappus_Pascal
circumcenter
ColR
construction_functions
E
Epsilonexercises
G
general_tacticsgravityCenter
H
hilbert_axiomsM
midpoint_thalesO
orientationorthocenter
P
Permutationsperp_bisect
project
Q
quadrilateralsquadrilaterals_inter_dec
S
setsT
tactics_axiomsTagged_predicates
tarski_to_col_theory
tarski_axioms
tarski_to_coapp_theory
tarski_to_hilbert
tarski_to_makarios
tarski_to_beeson
triangles
triangle_midpoints_theorems
U
unit_testsV
vectors| 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 | (2040 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 | (17 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 | (91 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 | (14 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 | (1530 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 | (81 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 | (4 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 | (2 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 | (230 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 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 | (7 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 | (51 entries) |
This page has been generated by coqdoc