Propriétés de is_image

Definition is_image

is_image := fun P' P A B => (exists X, is_midpoint X P P' /\ Col A B X) /\ (Perp A B P P' \/ P = P')

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

l10_2_unicity (image unicity)

forall A B P P1 P2, A ≠ B → is_image P1 P A B → is_image P2 P A B → P1 = P2

l10_2_existence (image existence)

forall A B P, exists P', is_image P' P A B

l10_4 (symmetry)

forall A B P P', is_image P P' A B → is_image P' P A B

l10_5 (is_image is involutive)

forall A B P P' P'', A ≠ B → is_image P' P A B → is_image P'' P' A B → P = P''

l10_6_unicity

forall A B P P1 P2, A ≠ B → is_image P P1 A B → is_image P P2 A B → P1 = P2

l10_6_existence

forall A B P', A ≠ B → exists P, is_image P' P A B

l10_7

forall A B P P' Q Q', A ≠ B → is_image P' P A B → is_image Q' Q A B → P'= Q' → P = Q

l10_8

forall A B P, A ≠ B → is_image P P A B → Col P A B

l10_10 (symmetry preserves congruence)

forall A B P Q P' Q', A<>B → is_image P' P A B → is_image Q' Q A B → Cong P Q P' Q'

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now) Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

l10_12

forall A B C A' B' C', Per A B C → Per A' B' C' → Cong A B A' B' → Cong B C B' C' → Cong A C A' C'

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now) Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)