Global Index

H

J

K

M

N

Q

R

V

W

X

Y

Z

_

other

(176 entries)

Library Index

A

B

D

E

F

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(9 entries)

Lemma Index

D

G

H

I

J

K

M

N

Q

R

U

V

W

X

Y

Z

_

other

(136 entries)

Axiom Index

A

D

G

H

J

K

M

N

O

Q

R

T

V

W

X

Y

Z

_

other

(14 entries)

Definition Index

A

E

H

J

K

M

N

Q

R

S

T

U

V

W

X

Y

Z

_

other

(17 entries)

Global Index

A

another_point [lemma, in TarskiGeometry.Ch03_between_properties]

B

beetween_trivial2 [lemma, in TarskiGeometry.Ch03_between_properties]
beetween_trivial [lemma, in TarskiGeometry.Ch03_between_properties]
Bet [axiom, in TarskiGeometry.Ch01_tarski_axioms]
between_cong_2 [lemma, in TarskiGeometry.Ch05_between_transitivity_le]
between_cong [lemma, in TarskiGeometry.Ch05_between_transitivity_le]
between_identity [axiom, in TarskiGeometry.Ch01_tarski_axioms]
between_exchange4 [lemma, in TarskiGeometry.Ch03_between_properties]
between_exchange2 [lemma, in TarskiGeometry.Ch03_between_properties]
between_exchange3 [lemma, in TarskiGeometry.Ch03_between_properties]
between_inner_transitivity [lemma, in TarskiGeometry.Ch03_between_properties]
between_egality [lemma, in TarskiGeometry.Ch03_between_properties]
between_symmetry [lemma, in TarskiGeometry.Ch03_between_properties]
Bet_4 [definition, in TarskiGeometry.Ch03_between_properties]

C

Ch01_tarski_axioms [library]
Ch02_congruence_properties [library]
Ch03_between_properties [library]
Ch04_congruence_between_properties [library]
Ch05_between_transitivity_le [library]
Ch06_out_lines [library]
Ch07_midpoint [library]
Ch08_orthogonality [library]
Col [definition, in TarskiGeometry.Ch01_tarski_axioms]
col_trivial_3 [lemma, in TarskiGeometry.Ch04_congruence_between_properties]
col_trivial_2 [lemma, in TarskiGeometry.Ch04_congruence_between_properties]
col_trivial_1 [lemma, in TarskiGeometry.Ch04_congruence_between_properties]
col_permutation_5 [lemma, in TarskiGeometry.Ch04_congruence_between_properties]
col_permutation_4 [lemma, in TarskiGeometry.Ch04_congruence_between_properties]
col_permutation_3 [lemma, in TarskiGeometry.Ch04_congruence_between_properties]
col_permutation_2 [lemma, in TarskiGeometry.Ch04_congruence_between_properties]
col_permutation_1 [lemma, in TarskiGeometry.Ch04_congruence_between_properties]
col_transitivity_2 [lemma, in TarskiGeometry.Ch06_out_lines]
col_transitivity_1 [lemma, in TarskiGeometry.Ch06_out_lines]
Cong [axiom, in TarskiGeometry.Ch01_tarski_axioms]
cong_commutativity [lemma, in TarskiGeometry.Ch02_congruence_properties]
cong_reverse_identity [lemma, in TarskiGeometry.Ch02_congruence_properties]
cong_trivial_identity [lemma, in TarskiGeometry.Ch02_congruence_properties]
cong_right_commutativity [lemma, in TarskiGeometry.Ch02_congruence_properties]
cong_left_commutativity [lemma, in TarskiGeometry.Ch02_congruence_properties]
cong_transitivity [lemma, in TarskiGeometry.Ch02_congruence_properties]
cong_symmetry [lemma, in TarskiGeometry.Ch02_congruence_properties]
cong_reflexivity [lemma, in TarskiGeometry.Ch02_congruence_properties]
cong_inner_transitivity [axiom, in TarskiGeometry.Ch01_tarski_axioms]
cong_identity [axiom, in TarskiGeometry.Ch01_tarski_axioms]
cong_pseudo_reflexivity [axiom, in TarskiGeometry.Ch01_tarski_axioms]
Cong_3 [definition, in TarskiGeometry.Ch04_congruence_between_properties]
construction_unicity [lemma, in TarskiGeometry.Ch02_congruence_properties]
continuity [axiom, in TarskiGeometry.Ch01_tarski_axioms]

D

DistLn [definition, in TarskiGeometry.Ch08_orthogonality]

E

eq_dec_points [lemma, in TarskiGeometry.Ch01_tarski_axioms]
euclid [axiom, in TarskiGeometry.Ch01_tarski_axioms]

F

five_segments_with_def [lemma, in TarskiGeometry.Ch02_congruence_properties]
five_segments [axiom, in TarskiGeometry.Ch01_tarski_axioms]
FSC [definition, in TarskiGeometry.Ch04_congruence_between_properties]

G

ge [definition, in TarskiGeometry.Ch05_between_transitivity_le]
general_tactics [library]
gt [definition, in TarskiGeometry.Ch05_between_transitivity_le]

I

IFSC [definition, in TarskiGeometry.Ch03_between_properties]
inner_pasch [axiom, in TarskiGeometry.Ch01_tarski_axioms]
Inter [definition, in TarskiGeometry.Ch06_out_lines]
is_midpoint [definition, in TarskiGeometry.Ch07_midpoint]

L

le [definition, in TarskiGeometry.Ch05_between_transitivity_le]
le_zero [lemma, in TarskiGeometry.Ch05_between_transitivity_le]
le_cases [lemma, in TarskiGeometry.Ch05_between_transitivity_le]
le_trivial [lemma, in TarskiGeometry.Ch05_between_transitivity_le]
le_anti_symmetry [lemma, in TarskiGeometry.Ch05_between_transitivity_le]
le_transitivity [lemma, in TarskiGeometry.Ch05_between_transitivity_le]
le_reflexivity [lemma, in TarskiGeometry.Ch05_between_transitivity_le]
lower_dim [axiom, in TarskiGeometry.Ch01_tarski_axioms]
lt [definition, in TarskiGeometry.Ch05_between_transitivity_le]
l_3_9_4 [lemma, in TarskiGeometry.Ch03_between_properties]
l2_11 [lemma, in TarskiGeometry.Ch02_congruence_properties]
l3_17 [lemma, in TarskiGeometry.Ch03_between_properties]
l4_19 [lemma, in TarskiGeometry.Ch04_congruence_between_properties]
l4_18 [lemma, in TarskiGeometry.Ch04_congruence_between_properties]
l4_17 [lemma, in TarskiGeometry.Ch04_congruence_between_properties]
l4_16 [lemma, in TarskiGeometry.Ch04_congruence_between_properties]
l4_14 [lemma, in TarskiGeometry.Ch04_congruence_between_properties]
l4_13 [lemma, in TarskiGeometry.Ch04_congruence_between_properties]
l4_6 [lemma, in TarskiGeometry.Ch04_congruence_between_properties]
l4_5 [lemma, in TarskiGeometry.Ch04_congruence_between_properties]
l4_3 [lemma, in TarskiGeometry.Ch04_congruence_between_properties]
l4_2 [lemma, in TarskiGeometry.Ch04_congruence_between_properties]
l5_6 [lemma, in TarskiGeometry.Ch05_between_transitivity_le]
l5_5_2 [lemma, in TarskiGeometry.Ch05_between_transitivity_le]
l5_5_1 [lemma, in TarskiGeometry.Ch05_between_transitivity_le]
l5_3 [lemma, in TarskiGeometry.Ch05_between_transitivity_le]
l5_2 [lemma, in TarskiGeometry.Ch05_between_transitivity_le]
l5_1 [lemma, in TarskiGeometry.Ch05_between_transitivity_le]
l6_25 [lemma, in TarskiGeometry.Ch06_out_lines]
l6_21 [lemma, in TarskiGeometry.Ch06_out_lines]
l6_16_2 [lemma, in TarskiGeometry.Ch06_out_lines]
l6_16_1 [lemma, in TarskiGeometry.Ch06_out_lines]
l6_13_2 [lemma, in TarskiGeometry.Ch06_out_lines]
l6_13_1 [lemma, in TarskiGeometry.Ch06_out_lines]
l6_11_existence [lemma, in TarskiGeometry.Ch06_out_lines]
l6_11_unicity [lemma, in TarskiGeometry.Ch06_out_lines]
l6_7 [lemma, in TarskiGeometry.Ch06_out_lines]
l6_6 [lemma, in TarskiGeometry.Ch06_out_lines]
l6_5 [lemma, in TarskiGeometry.Ch06_out_lines]
l6_4_2 [lemma, in TarskiGeometry.Ch06_out_lines]
l6_4_1 [lemma, in TarskiGeometry.Ch06_out_lines]
l6_3_2 [lemma, in TarskiGeometry.Ch06_out_lines]
l6_3_1 [lemma, in TarskiGeometry.Ch06_out_lines]
l6_2 [lemma, in TarskiGeometry.Ch06_out_lines]
l7_25 [lemma, in TarskiGeometry.Ch07_midpoint]
l7_22 [lemma, in TarskiGeometry.Ch07_midpoint]
l7_22_aux [lemma, in TarskiGeometry.Ch07_midpoint]
l7_21 [lemma, in TarskiGeometry.Ch07_midpoint]
l7_20 [lemma, in TarskiGeometry.Ch07_midpoint]
l7_17 [lemma, in TarskiGeometry.Ch07_midpoint]
l7_16 [lemma, in TarskiGeometry.Ch07_midpoint]
l7_15 [lemma, in TarskiGeometry.Ch07_midpoint]
l7_13 [lemma, in TarskiGeometry.Ch07_midpoint]
l7_9 [lemma, in TarskiGeometry.Ch07_midpoint]
l7_3_2 [lemma, in TarskiGeometry.Ch07_midpoint]
l7_3 [lemma, in TarskiGeometry.Ch07_midpoint]
l7_2 [lemma, in TarskiGeometry.Ch07_midpoint]
l8_21 [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_21_aux [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_20_2 [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_20_1 [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_18_existence [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_18_unicity [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_16_2 [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_16_1 [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_15_2 [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_15_1 [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_14_3 [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_14_2_2 [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_14_2_1b_bis [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_14_2_1b [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_14_2_1a [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_14_1 [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_13_2 [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_12 [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_10 [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_9 [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_8 [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_7 [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_6 [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_5 [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_4 [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_3 [lemma, in TarskiGeometry.Ch08_orthogonality]
l8_2 [lemma, in TarskiGeometry.Ch08_orthogonality]

O

OFSC [definition, in TarskiGeometry.Ch02_congruence_properties]
out [definition, in TarskiGeometry.Ch06_out_lines]
outer_transitivity_between [lemma, in TarskiGeometry.Ch03_between_properties]
outer_transitivity_between2 [lemma, in TarskiGeometry.Ch03_between_properties]

P

Per [definition, in TarskiGeometry.Ch08_orthogonality]
Perp [definition, in TarskiGeometry.Ch08_orthogonality]
perp_perp_in [lemma, in TarskiGeometry.Ch08_orthogonality]
perp_not_eq_2 [lemma, in TarskiGeometry.Ch08_orthogonality]
perp_not_eq_1 [lemma, in TarskiGeometry.Ch08_orthogonality]
perp_col [lemma, in TarskiGeometry.Ch08_orthogonality]
perp_per_2 [lemma, in TarskiGeometry.Ch08_orthogonality]
perp_per_1 [lemma, in TarskiGeometry.Ch08_orthogonality]
perp_in_symmetry [lemma, in TarskiGeometry.Ch08_orthogonality]
perp_in_commutativity [lemma, in TarskiGeometry.Ch08_orthogonality]
perp_in_right_commutativity [lemma, in TarskiGeometry.Ch08_orthogonality]
perp_in_left_commutativity [lemma, in TarskiGeometry.Ch08_orthogonality]
perp_right_commutativity [lemma, in TarskiGeometry.Ch08_orthogonality]
perp_left_commutativity [lemma, in TarskiGeometry.Ch08_orthogonality]
perp_commutativity [lemma, in TarskiGeometry.Ch08_orthogonality]
perp_symmetry [lemma, in TarskiGeometry.Ch08_orthogonality]
Perp_in [definition, in TarskiGeometry.Ch08_orthogonality]
Point [axiom, in TarskiGeometry.Ch01_tarski_axioms]
point_construction_different [lemma, in TarskiGeometry.Ch03_between_properties]

S

segment_construction_2 [lemma, in TarskiGeometry.Ch05_between_transitivity_le]
segment_construction [axiom, in TarskiGeometry.Ch01_tarski_axioms]
symmetric_point_unicity [lemma, in TarskiGeometry.Ch07_midpoint]
symmetric_point_construction [lemma, in TarskiGeometry.Ch07_midpoint]
symmetry_preserves_midpoint [lemma, in TarskiGeometry.Ch07_midpoint]

T

two_distinct_points [lemma, in TarskiGeometry.Ch03_between_properties]
t2_8 [lemma, in TarskiGeometry.Ch06_out_lines]

U

upper_dim [axiom, in TarskiGeometry.Ch01_tarski_axioms]

Library Index

C

Ch01_tarski_axioms
Ch02_congruence_properties
Ch03_between_properties
Ch04_congruence_between_properties
Ch05_between_transitivity_le
Ch06_out_lines
Ch07_midpoint
Ch08_orthogonality

G

general_tactics

Lemma Index

A

another_point [in TarskiGeometry.Ch03_between_properties]

B

beetween_trivial2 [in TarskiGeometry.Ch03_between_properties]
beetween_trivial [in TarskiGeometry.Ch03_between_properties]
between_cong_2 [in TarskiGeometry.Ch05_between_transitivity_le]
between_cong [in TarskiGeometry.Ch05_between_transitivity_le]
between_exchange4 [in TarskiGeometry.Ch03_between_properties]
between_exchange2 [in TarskiGeometry.Ch03_between_properties]
between_exchange3 [in TarskiGeometry.Ch03_between_properties]
between_inner_transitivity [in TarskiGeometry.Ch03_between_properties]
between_egality [in TarskiGeometry.Ch03_between_properties]
between_symmetry [in TarskiGeometry.Ch03_between_properties]

C

col_trivial_3 [in TarskiGeometry.Ch04_congruence_between_properties]
col_trivial_2 [in TarskiGeometry.Ch04_congruence_between_properties]
col_trivial_1 [in TarskiGeometry.Ch04_congruence_between_properties]
col_permutation_5 [in TarskiGeometry.Ch04_congruence_between_properties]
col_permutation_4 [in TarskiGeometry.Ch04_congruence_between_properties]
col_permutation_3 [in TarskiGeometry.Ch04_congruence_between_properties]
col_permutation_2 [in TarskiGeometry.Ch04_congruence_between_properties]
col_permutation_1 [in TarskiGeometry.Ch04_congruence_between_properties]
col_transitivity_2 [in TarskiGeometry.Ch06_out_lines]
col_transitivity_1 [in TarskiGeometry.Ch06_out_lines]
cong_commutativity [in TarskiGeometry.Ch02_congruence_properties]
cong_reverse_identity [in TarskiGeometry.Ch02_congruence_properties]
cong_trivial_identity [in TarskiGeometry.Ch02_congruence_properties]
cong_right_commutativity [in TarskiGeometry.Ch02_congruence_properties]
cong_left_commutativity [in TarskiGeometry.Ch02_congruence_properties]
cong_transitivity [in TarskiGeometry.Ch02_congruence_properties]
cong_symmetry [in TarskiGeometry.Ch02_congruence_properties]
cong_reflexivity [in TarskiGeometry.Ch02_congruence_properties]
construction_unicity [in TarskiGeometry.Ch02_congruence_properties]

E

eq_dec_points [in TarskiGeometry.Ch01_tarski_axioms]

F

five_segments_with_def [in TarskiGeometry.Ch02_congruence_properties]

L

le_zero [in TarskiGeometry.Ch05_between_transitivity_le]
le_cases [in TarskiGeometry.Ch05_between_transitivity_le]
le_trivial [in TarskiGeometry.Ch05_between_transitivity_le]
le_anti_symmetry [in TarskiGeometry.Ch05_between_transitivity_le]
le_transitivity [in TarskiGeometry.Ch05_between_transitivity_le]
le_reflexivity [in TarskiGeometry.Ch05_between_transitivity_le]
l_3_9_4 [in TarskiGeometry.Ch03_between_properties]
l2_11 [in TarskiGeometry.Ch02_congruence_properties]
l3_17 [in TarskiGeometry.Ch03_between_properties]
l4_19 [in TarskiGeometry.Ch04_congruence_between_properties]
l4_18 [in TarskiGeometry.Ch04_congruence_between_properties]
l4_17 [in TarskiGeometry.Ch04_congruence_between_properties]
l4_16 [in TarskiGeometry.Ch04_congruence_between_properties]
l4_14 [in TarskiGeometry.Ch04_congruence_between_properties]
l4_13 [in TarskiGeometry.Ch04_congruence_between_properties]
l4_6 [in TarskiGeometry.Ch04_congruence_between_properties]
l4_5 [in TarskiGeometry.Ch04_congruence_between_properties]
l4_3 [in TarskiGeometry.Ch04_congruence_between_properties]
l4_2 [in TarskiGeometry.Ch04_congruence_between_properties]
l5_6 [in TarskiGeometry.Ch05_between_transitivity_le]
l5_5_2 [in TarskiGeometry.Ch05_between_transitivity_le]
l5_5_1 [in TarskiGeometry.Ch05_between_transitivity_le]
l5_3 [in TarskiGeometry.Ch05_between_transitivity_le]
l5_2 [in TarskiGeometry.Ch05_between_transitivity_le]
l5_1 [in TarskiGeometry.Ch05_between_transitivity_le]
l6_25 [in TarskiGeometry.Ch06_out_lines]
l6_21 [in TarskiGeometry.Ch06_out_lines]
l6_16_2 [in TarskiGeometry.Ch06_out_lines]
l6_16_1 [in TarskiGeometry.Ch06_out_lines]
l6_13_2 [in TarskiGeometry.Ch06_out_lines]
l6_13_1 [in TarskiGeometry.Ch06_out_lines]
l6_11_existence [in TarskiGeometry.Ch06_out_lines]
l6_11_unicity [in TarskiGeometry.Ch06_out_lines]
l6_7 [in TarskiGeometry.Ch06_out_lines]
l6_6 [in TarskiGeometry.Ch06_out_lines]
l6_5 [in TarskiGeometry.Ch06_out_lines]
l6_4_2 [in TarskiGeometry.Ch06_out_lines]
l6_4_1 [in TarskiGeometry.Ch06_out_lines]
l6_3_2 [in TarskiGeometry.Ch06_out_lines]
l6_3_1 [in TarskiGeometry.Ch06_out_lines]
l6_2 [in TarskiGeometry.Ch06_out_lines]
l7_25 [in TarskiGeometry.Ch07_midpoint]
l7_22 [in TarskiGeometry.Ch07_midpoint]
l7_22_aux [in TarskiGeometry.Ch07_midpoint]
l7_21 [in TarskiGeometry.Ch07_midpoint]
l7_20 [in TarskiGeometry.Ch07_midpoint]
l7_17 [in TarskiGeometry.Ch07_midpoint]
l7_16 [in TarskiGeometry.Ch07_midpoint]
l7_15 [in TarskiGeometry.Ch07_midpoint]
l7_13 [in TarskiGeometry.Ch07_midpoint]
l7_9 [in TarskiGeometry.Ch07_midpoint]
l7_3_2 [in TarskiGeometry.Ch07_midpoint]
l7_3 [in TarskiGeometry.Ch07_midpoint]
l7_2 [in TarskiGeometry.Ch07_midpoint]
l8_21 [in TarskiGeometry.Ch08_orthogonality]
l8_21_aux [in TarskiGeometry.Ch08_orthogonality]
l8_20_2 [in TarskiGeometry.Ch08_orthogonality]
l8_20_1 [in TarskiGeometry.Ch08_orthogonality]
l8_18_existence [in TarskiGeometry.Ch08_orthogonality]
l8_18_unicity [in TarskiGeometry.Ch08_orthogonality]
l8_16_2 [in TarskiGeometry.Ch08_orthogonality]
l8_16_1 [in TarskiGeometry.Ch08_orthogonality]
l8_15_2 [in TarskiGeometry.Ch08_orthogonality]
l8_15_1 [in TarskiGeometry.Ch08_orthogonality]
l8_14_3 [in TarskiGeometry.Ch08_orthogonality]
l8_14_2_2 [in TarskiGeometry.Ch08_orthogonality]
l8_14_2_1b_bis [in TarskiGeometry.Ch08_orthogonality]
l8_14_2_1b [in TarskiGeometry.Ch08_orthogonality]
l8_14_2_1a [in TarskiGeometry.Ch08_orthogonality]
l8_14_1 [in TarskiGeometry.Ch08_orthogonality]
l8_13_2 [in TarskiGeometry.Ch08_orthogonality]
l8_12 [in TarskiGeometry.Ch08_orthogonality]
l8_10 [in TarskiGeometry.Ch08_orthogonality]
l8_9 [in TarskiGeometry.Ch08_orthogonality]
l8_8 [in TarskiGeometry.Ch08_orthogonality]
l8_7 [in TarskiGeometry.Ch08_orthogonality]
l8_6 [in TarskiGeometry.Ch08_orthogonality]
l8_5 [in TarskiGeometry.Ch08_orthogonality]
l8_4 [in TarskiGeometry.Ch08_orthogonality]
l8_3 [in TarskiGeometry.Ch08_orthogonality]
l8_2 [in TarskiGeometry.Ch08_orthogonality]

O

outer_transitivity_between [in TarskiGeometry.Ch03_between_properties]
outer_transitivity_between2 [in TarskiGeometry.Ch03_between_properties]

P

perp_perp_in [in TarskiGeometry.Ch08_orthogonality]
perp_not_eq_2 [in TarskiGeometry.Ch08_orthogonality]
perp_not_eq_1 [in TarskiGeometry.Ch08_orthogonality]
perp_col [in TarskiGeometry.Ch08_orthogonality]
perp_per_2 [in TarskiGeometry.Ch08_orthogonality]
perp_per_1 [in TarskiGeometry.Ch08_orthogonality]
perp_in_symmetry [in TarskiGeometry.Ch08_orthogonality]
perp_in_commutativity [in TarskiGeometry.Ch08_orthogonality]
perp_in_right_commutativity [in TarskiGeometry.Ch08_orthogonality]
perp_in_left_commutativity [in TarskiGeometry.Ch08_orthogonality]
perp_right_commutativity [in TarskiGeometry.Ch08_orthogonality]
perp_left_commutativity [in TarskiGeometry.Ch08_orthogonality]
perp_commutativity [in TarskiGeometry.Ch08_orthogonality]
perp_symmetry [in TarskiGeometry.Ch08_orthogonality]
point_construction_different [in TarskiGeometry.Ch03_between_properties]

S

segment_construction_2 [in TarskiGeometry.Ch05_between_transitivity_le]
symmetric_point_unicity [in TarskiGeometry.Ch07_midpoint]
symmetric_point_construction [in TarskiGeometry.Ch07_midpoint]
symmetry_preserves_midpoint [in TarskiGeometry.Ch07_midpoint]

T

two_distinct_points [in TarskiGeometry.Ch03_between_properties]
t2_8 [in TarskiGeometry.Ch06_out_lines]

Axiom Index

B

Bet [in TarskiGeometry.Ch01_tarski_axioms]
between_identity [in TarskiGeometry.Ch01_tarski_axioms]

C

Cong [in TarskiGeometry.Ch01_tarski_axioms]
cong_inner_transitivity [in TarskiGeometry.Ch01_tarski_axioms]
cong_identity [in TarskiGeometry.Ch01_tarski_axioms]
cong_pseudo_reflexivity [in TarskiGeometry.Ch01_tarski_axioms]
continuity [in TarskiGeometry.Ch01_tarski_axioms]

E

euclid [in TarskiGeometry.Ch01_tarski_axioms]

F

five_segments [in TarskiGeometry.Ch01_tarski_axioms]

I

inner_pasch [in TarskiGeometry.Ch01_tarski_axioms]

L

lower_dim [in TarskiGeometry.Ch01_tarski_axioms]

P

Point [in TarskiGeometry.Ch01_tarski_axioms]

S

segment_construction [in TarskiGeometry.Ch01_tarski_axioms]

U

upper_dim [in TarskiGeometry.Ch01_tarski_axioms]

Definition Index

B

Bet_4 [in TarskiGeometry.Ch03_between_properties]

C

Col [in TarskiGeometry.Ch01_tarski_axioms]
Cong_3 [in TarskiGeometry.Ch04_congruence_between_properties]

D

DistLn [in TarskiGeometry.Ch08_orthogonality]

F

FSC [in TarskiGeometry.Ch04_congruence_between_properties]

G

ge [in TarskiGeometry.Ch05_between_transitivity_le]
gt [in TarskiGeometry.Ch05_between_transitivity_le]

I

IFSC [in TarskiGeometry.Ch03_between_properties]
Inter [in TarskiGeometry.Ch06_out_lines]
is_midpoint [in TarskiGeometry.Ch07_midpoint]

L

le [in TarskiGeometry.Ch05_between_transitivity_le]
lt [in TarskiGeometry.Ch05_between_transitivity_le]

O

OFSC [in TarskiGeometry.Ch02_congruence_properties]
out [in TarskiGeometry.Ch06_out_lines]

P

Per [in TarskiGeometry.Ch08_orthogonality]
Perp [in TarskiGeometry.Ch08_orthogonality]
Perp_in [in TarskiGeometry.Ch08_orthogonality]

Global Index

H

J

K

M

N

Q

R

V

W

X

Y

Z

_

other

(176 entries)

Library Index

A

B

D

E

F

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(9 entries)

Lemma Index

D

G

H

I

J

K

M

N

Q

R

U

V

W

X

Y

Z

_

other

(136 entries)

Axiom Index

A

D

G

H

J

K

M

N

O

Q

R

T

V

W

X

Y

Z

_

other

(14 entries)

Definition Index

A

E

H

J

K

M

N

Q

R

S

T

U

V

W

X

Y

Z

_

other

(17 entries)