List of theorems

List of theorems in general/Line_segment_inequality.gh:

(→ (∧ (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D)) (between A C D)) (between B C D))
(→ (∧ (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D)) (between A D C)) (between B D C))
(→ (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D)) (∨ (between B C D) (between B D C)))
(→ (∧ (between A B D) (between A C D)) (∃ e (∧ (∧ (between A B D) (between A C D)) (∧ (between D A e) (¬ (= A e))))))
(→ (∧ (∧ (between A B D) (between A C D)) (∧ (between D A E) (¬ (= A E)))) (between E A B))
(→ (∧ (∧ (between A B D) (between A C D)) (∧ (between D A E) (¬ (= A E)))) (between E A C))
(→ (∧ (∧ (between A B D) (between A C D)) (∧ (between D A E) (¬ (= A E)))) (∨ (between A B C) (between A C B)))
(→ (∧ (between A B D) (between A C D)) (∨ (between A B C) (between A C B)))
(↔ (≤ A B C D) (∃ e (∧ (between C e D) (≡ A B C e))))
(↔ (≥ A B C D) (≤ C D A B))
(→ (∧ (between C E D) (≡ A B C E)) (∃ f (≅ C E D A B f)))
(→ (∧ (between C E D) (≡ A B C E)) (∃ f (∧ (between C E D) (≅ C E D A B f))))
(→ (∧ (between C E D) (≅ C E D A B F)) (∧ (between A B F) (≡ A F C D)))
(→ (≤ A B C D) (∃ f (∧ (between A B f) (≡ A f C D))))
(→ (∃ f (∧ (between A B f) (≡ A f C D))) (≤ A B C D))
(↔ (≤ A B C D) (∃ f (∧ (between A B f) (≡ A f C D))))
(→ (∧ (∧ (≤ A B C D) (≡ A B A′ B′)) (≡ C D C′ D′)) (∃ e (∧ (∧ (∧ (between C e D) (≡ A B C e)) (≡ A B A′ B′)) (≡ C D C′ D′))))
(→ (∧ (∧ (∧ (between C E D) (≡ A B C E)) (≡ A B A′ B′)) (≡ C D C′ D′)) (∃ e′ (∧ (∧ (between C′ e′ D′) (≅ C E D C′ e′ D′)) (≡ A′ B′ C E))))
(→ (∧ (∧ (between C′ E′ D′) (≅ C E D C′ E′ D′)) (≡ A′ B′ C E)) (∧ (between C′ E′ D′) (≡ A′ B′ C′ E′)))
(→ (∧ (∧ (≤ A B C D) (≡ A B A′ B′)) (≡ C D C′ D′)) (≤ A′ B′ C′ D′))
(≤ A B A B)
(→ (∧ (≤ A0 A1 B0 B1) (≤ B0 B1 C0 C1)) (≤ A0 A1 C0 C1))
(→ (∧ (between A B C) (≡ A B A C)) (≅ A B C A C B))
(→ (∧ (between A B C) (≡ A B A C)) (= B C))
(→ (∧ (∧ (between A D B) (between A E B)) (≡ A D A E)) (= D E))
(→ (∧ (between A B C) (between A C B)) (= B C))
(→ (∧ (≤ A0 A1 B0 B1) (≤ B0 B1 A0 A1)) (∃ c (∃ d (∧ (∧ (between B0 B1 c) (≡ B0 c A0 A1)) (∧ (between B0 d B1) (≡ B0 d A0 A1))))))
(→ (∧ (∧ (between B0 B1 C) (≡ B0 C A0 A1)) (∧ (between B0 D B1) (≡ B0 D A0 A1))) (= D C))
(→ (∧ (∧ (between B0 B1 C) (≡ B0 C A0 A1)) (∧ (between B0 D B1) (≡ B0 D A0 A1))) (= B1 C))
(→ (∧ (∧ (between B0 B1 C) (≡ B0 C A0 A1)) (∧ (between B0 D B1) (≡ B0 D A0 A1))) (≡ A0 A1 B0 B1))
(→ (∧ (≤ A0 A1 B0 B1) (≤ B0 B1 A0 A1)) (≡ A0 A1 B0 B1))
(∃ p (∧ (∨ (between Q A p) (between Q p A)) (≡ Q p B C)))
(≤ A A B C)
(→ (∧ (∧ (∧ (= x0 y0) (= x1 y1)) (= x2 y2)) (= x3 y3)) (↔ (≤ x0 x1 x2 x3) (≤ y0 y1 y2 y3)))
(∨ (≤ A0 A1 B0 B1) (≤ B0 B1 A0 A1))
(→ (≤ A B C C) (= A B))
(↔ (< A B C D) (∧ (≤ A B C D) (¬ (≡ A B C D))))
(↔ (> A B C D) (< C D A B))
(→ (∧ (= x y) (≡ x y z w)) (= z w))