Toutes les notions utilisées en géométrie peuvent être décrites à l'aide des seuls concepts primitifs de point, de la relation "entre" et la congruence
Col A B C := Bet A B C \/ Bet C A B \/ Bet B C A
(A B C sont colinéaires)
AB ≤ CD := ∃ Y, Bet C Y D /\ A B ≡ C Y
(la longueur du segment AB est inférieure ou égale à celle du segment CD)
Il en découle les définitions de : ≥ < > :
out P A B := A ≠ P /\ B ≠ P /\ (Bet P A B \/ Bet P B A)
(P est strictement extérieur au segment AB sur la droite AB)
B milieu de A C := Bet A B C /\ AB ≡ BC
L'orthogonalité s'articule autour de trois relations :
Δ A B C := exists C', B milieu de C C' /\ A C ≡ A C'
(A B C forment un angle droit dans les cas non dégénérés)
on notera que la définition n'exclut pas le cas A = B ou B = C
Δ A A B et Δ A B B sont toujours vérifiés
AB ⊥XCD := A<>B /\ C<>D /\ Col X A B /\ Col X C D /\
(∀ U V, Col U A B → Col V C D → Δ U X V).
(les droites AB et CD sont perpendiculaires en X)
AB ⊥ CD := ∃ X, AB ⊥XCD
(les droites AB et CD sont perpendiculaires)
two_sides A B P Q := A ≠ B /\ ¬ Col P A B /\ ¬ Col Q A B /\
(∃ T, Col T A B /\ Bet P T Q)
(P et Q sont de part et d'autre de la droite AB)
on en tire une définition de one_side
one_side A B P Q := ∃ C, two_sides A B P C /\ two_sides A B Q C.
(P et Q sont du mème coté de la droite AB)
is_image P' P A B := (∃ X, X milieu de P P' /\ Col A B X) /\ (AB ⊥ PP' \/ P = P')
(P' est le symétrique de P par rapport à ma droite AB)
A B C ∠ D E F := A ≠ B → B ≠ C → D ≠E → F ≠ E →
∃ A', ∃ C', ∃ D', ∃ F',
Bet B A A' /\ AA' ≡ ED /\
Bet B C C' /\ CC' ≡ EF /\
Bet E D D' /\ DD' ≡ BA /\
Bet E F F' /\ FF' ≡ BC /\
A'C' ≡ D'F'
(ABC et DEF reprént le même angle)
Par_strict A B C D := A ≠ B /\ C ≠ D /\ ¬ ∃ X, Col X A B /\ Col X C D
(AB strictement parallèle à CD)
Par A B C D := Par_strict A B C D \/ (A ≠ B /\ C ≠ D /\ Col A C D /\ Col B C D
(AB parallèle à CD)
| retour à l'acceuil | Gabriel Braun - octobre 2011 | statistiques |