Axioms of synthetic geometry

Universes for points lines and circles

class SyntheticEuclid4.IncidenceGeometry : Type (u + 1)

IncidenceGeometry represents geometry in the Euclidean sense, with primitives for points lines and circles

• Point : Type u

  Points in the plane

• Line : Type u

  Lines in the plane

• Circle : Type u

  Circles in the plane

• OnLine : Point → Line → Prop

  A Point being on a line

• SameSide : Point → Point → Line → Prop

  Two points being on the sameside of a line

• B : Point → Point → Point → Prop

  Three points being in a row

• CenterCircle : Point → Circle → Prop

  A point being the center of a center

• OnCircle : Point → Circle → Prop

  A point being on a circle

• InCircle : Point → Circle → Prop

  A point being inside a circle

• LinesInter : Line → Line → Prop

  That two lines intersect

• LineCircleInter : Line → Circle → Prop

  A line and a circle intersect

• CirclesInter : Circle → Circle → Prop

  Two circles intersect

• length : Point → Point → ℝ

  The distance between two points

• angle : Point → Point → Point → ℝ

  The angle made between three points

• rightangle : ℝ

  The constant dedicated to the right angle

• area : Point → Point → Point → ℝ

  The area made by three points

• more_pts (S : Set Point) : S.Finite → ∃ (a : Point), a ∉ S

  From a set of points getting one additional one

• pt_B_of_ne {b c : Point} : b ≠ c → ∃ (a : Point), B b a c

  Interpolating a segment by an arbitrary amount

• pt_extension_of_ne {b c : Point} : b ≠ c → ∃ (a : Point), B b c a

  Extending a segment by an arbitrary amount

• diffside_of_not_online {L : Line} {a : Point} : ¬OnLine a L → ∃ (b : Point), ¬OnLine b L ∧ ¬SameSide a b L

  Obtaining a point opposite a line and point

• line_of_pts (a b : Point) : ∃ (L : Line), OnLine a L ∧ OnLine b L

  Get a line from two points

• circle_of_ne {a b : Point} : a ≠ b → ∃ (α : Circle), CenterCircle a α ∧ OnCircle b α

  Getting a circle with center and point on it

• pt_of_linesinter {L M : Line} : LinesInter L M → ∃ (a : Point), OnLine a L ∧ OnLine a M

  If lines intersect then this gives you the point of intersection

• pts_of_linecircleinter {L : Line} {α : Circle} : LineCircleInter L α → ∃ (a : Point) (b : Point), a ≠ b ∧ OnLine a L ∧ OnLine b L ∧ OnCircle a α ∧ OnCircle b α

  Gives you the points of intersection when a circle and line intersect

• pt_on_circle_of_inside_outside {b c : Point} {α : Circle} : ¬OnCircle c α → InCircle b α → ¬InCircle c α → ∃ (a : Point), B b a c ∧ OnCircle a α

  Getting points on circles

• pt_oncircle_of_inside_ne {a b : Point} {α : Circle} : a ≠ b → InCircle b α → ∃ (c : Point), B a b c ∧ OnCircle c α

  Getting points on circles

• pts_of_circlesinter {α β : Circle} : CirclesInter α β → ∃ (a : Point) (b : Point), a ≠ b ∧ OnCircle a α ∧ OnCircle a β ∧ OnCircle b α ∧ OnCircle b β

  Getting points of intersection of two circles

• pt_sameside_of_circlesinter {b c d : Point} {L : Line} {α β : Circle} : OnLine c L → OnLine d L → ¬OnLine b L → CenterCircle c α → CenterCircle d β → CirclesInter α β → ∃ (a : Point), SameSide a b L ∧ OnCircle a α ∧ OnCircle a β

  Obtaining a specific point of intersection between a line and a circle

• line_unique_of_pts {a b : Point} {L M : Line} : a ≠ b → OnLine a L → OnLine b L → OnLine a M → OnLine b M → L = M

  Condition to remark that two points uniquely determine a line

• centercircle_unique {a b : Point} {α : Circle} : CenterCircle a α → CenterCircle b α → a = b

  The center of a circle is unique

• inside_circle_of_center {a : Point} {α : Circle} : CenterCircle a α → InCircle a α

  The center of a circle is inside the circle

• not_on_circle_of_inside {a : Point} {α : Circle} : InCircle a α → ¬OnCircle a α

  If a point is on a circle then it is not inside

• B_symm {a b c : Point} : B a b c → B c b a

  Symmetry of Betweeness

• ne_12_of_B {a b c : Point} : B a b c → a ≠ b

  B is strict

• ne_13_of_B {a b c : Point} : B a b c → a ≠ c

  B is strict

• ne_23_of_B {a b c : Point} : B a b c → b ≠ c

  B is strict

• not_B_of_B {a b c : Point} : B a b c → ¬B b a c

  If you are between then the other configurations are impossible

• online_3_of_B {a b c : Point} {L : Line} : B a b c → OnLine a L → OnLine b L → OnLine c L

  From two points being on a line the B forces the third point

• online_2_of_B {a b c : Point} {L : Line} : B a b c → OnLine a L → OnLine c L → OnLine b L

  From two points being on a line the B forces the third point

• B124_of_B134_B123 {a b c d : Point} : B a b c → B a d b → B a d c

  Deducing betweeness from four points on a line

• B124_of_B123_B234 {a b c d : Point} : B a b c → B b c d → B a b d

  Deducing betweeness from four points on a line

• B_of_three_online_ne {a b c : Point} {L : Line} : a ≠ b → a ≠ c → b ≠ c → OnLine a L → OnLine b L → OnLine c L → B a b c ∨ B b a c ∨ B a c b

  If three distict points are on a line then they are between in some way

• not_B324_of_B123_B124 {a b c d : Point} : B a b c → B a b d → ¬B c b d

  Conditions for not B given four points on a line

• sameside_rfl_of_not_online {a : Point} {L : Line} : ¬OnLine a L → SameSide a a L

  Sameside is reflective

• sameside_symm {a b : Point} {L : Line} : SameSide a b L → SameSide b a L

  Sameside is symmetric

• not_online_of_sameside {a b : Point} {L : Line} : SameSide a b L → ¬OnLine a L

  Being on the sameside of a line implies you are not on the line

• sameside_trans {a b c : Point} {L : Line} : SameSide a b L → SameSide a c L → SameSide b c L

  Sameside is transitive

• sameside_or_of_diffside {a b c : Point} {L : Line} : ¬OnLine a L → ¬OnLine b L → ¬OnLine c L → ¬SameSide a b L → SameSide a c L ∨ SameSide b c L

  If you are not on a line and two points are on opposite sides then you are on the same side as one of the points

• sameside12_of_B123_sameside13 {a b c : Point} {L : Line} : B a b c → SameSide a c L → SameSide a b L

  Relations between sidedness and betweeness

• sameside_of_B_not_online_2 {a b c : Point} {L : Line} : B a b c → OnLine a L → ¬OnLine b L → SameSide b c L

  Relations between sidedness and betweeness

• not_sameside13_of_B123_online2 {a b c : Point} {L : Line} : B a b c → OnLine b L → ¬SameSide a c L

  Relations between sidedness and betweeness

• B_of_online_inter {a b c : Point} {L M : Line} : a ≠ b → b ≠ c → a ≠ c → L ≠ M → OnLine a L → OnLine b L → OnLine c L → OnLine b M → ¬SameSide a c M → B a b c

  Relations between sidedness and betweeness

• not_sameside_of_sameside_sameside {a b c d : Point} {L M N : Line} : OnLine a L → OnLine a M → OnLine a N → OnLine b L → OnLine c M → OnLine d N → SameSide c d L → SameSide b c N → ¬SameSide b d M

  Deducing sidedness from three lines intersecting

• sameside_of_sameside_not_sameside {a b c d : Point} {L M N : Line} : a ≠ b → OnLine a L → OnLine a M → OnLine a N → OnLine b L → OnLine c M → OnLine d N → ¬OnLine d M → SameSide c d L → ¬SameSide b d M → SameSide b c N

  Deducing sidedness from three lines intersecting

• B_of_linecircleinter {a b c : Point} {L : Line} {α : Circle} : b ≠ c → OnLine a L → OnLine b L → OnLine c L → OnCircle b α → OnCircle c α → InCircle a α → B b a c

  Points of intersection of a line and circle

• not_sameside_of_circle_inter {a b c d : Point} {L : Line} {α β : Circle} : c ≠ d → α ≠ β → OnLine a L → OnLine b L → OnCircle c α → OnCircle c β → OnCircle d α → OnCircle d β → CenterCircle a α → CenterCircle b β → CirclesInter α β → ¬SameSide c d L

  The points of intersection of circles are on opposite sides the line that joins the centers

• lines_inter_of_not_sameside {a b : Point} {L M : Line} : OnLine a M → OnLine b M → ¬SameSide a b L → LinesInter L M

  Condition for lines intersecting

• linecircleinter_of_not_sameside {a b : Point} {L : Line} {α : Circle} : ¬SameSide a b L → OnCircle a α ∨ InCircle a α → OnCircle b α ∨ InCircle b α → LineCircleInter L α

  Condition for line circle intersection

• linecircleinter_of_inside_online {a : Point} {L : Line} {α : Circle} : OnLine a L → InCircle a α → LineCircleInter L α

  Condition for line circle intersection

• circlesinter_of_inside_on_circle {a b : Point} {α β : Circle} : OnCircle b α → OnCircle a β → InCircle a α → InCircle b β → CirclesInter α β

  Condition for circle circle intersection

• length_eq_zero_iff {a b : Point} : length a b = 0 ↔ a = b

  A length is zero iff the points are equal

• length_symm (a b : Point) : length a b = length b a

  Length is symmetric

• angle_symm (a b c : Point) : angle a b c = angle c b a

  Angles are symmetric across the middle point

• angle_nonneg (a b c : Point) : 0 ≤ angle a b c

  Angles are nonnegative

• length_nonneg (a b : Point) : 0 ≤ length a b

  Lengths are nonnegative

• area_nonneg (a b c : Point) : 0 ≤ area a b c

  Areas are nonnegative

• degenerate_area (a b : Point) : area a a b = 0

  Degenerate areas are zero

• area_invariant (a b c : Point) : area a b c = area c a b ∧ area a b c = area a c b

  Area is completely symmetric

• area_eq_of_SSS {a b c a1 b1 c1 : Point} : length a b = length a1 b1 → length a c = length a1 c1 → length b c = length b1 c1 → area a b c = area a1 b1 c1

  If SSS is satisfied then triangles have equal area

• length_sum_of_B {a b c : Point} : B a b c → length a b + length b c = length a c

  Given betweeness the lengths of segments add as expected

• on_circle_iff_length_eq {a b c : Point} {α : Circle} : CenterCircle a α → OnCircle b α → (length a b = length a c ↔ OnCircle c α)

  Points on a circle have the same distance from the radius

• in_circle_iff_length_lt {a b c : Point} {α : Circle} : CenterCircle a α → OnCircle b α → (length a c < length a b ↔ InCircle c α)

  A point on a circle has a greater distance from the center than a point inside the circle

• angle_zero_iff_online {a b c : Point} {L : Line} : a ≠ b → a ≠ c → OnLine a L → OnLine b L → (OnLine c L ∧ ¬B b a c ↔ angle b a c = 0)

  One kind of degenerate angle is zero

• angle_add_iff_sameside {a b c d : Point} {L M : Line} : a ≠ b → a ≠ c → OnLine a L → OnLine b L → OnLine a M → OnLine c M → ¬OnLine d M → ¬OnLine d L → L ≠ M → (angle b a c = angle b a d + angle d a c ↔ SameSide b d M ∧ SameSide c d L)

  Conditions for a split angle to add as expected

• angle_eq_iff_rightangle {a b c d : Point} {L : Line} : OnLine a L → OnLine b L → ¬OnLine d L → B a c b → (angle a c d = angle d c b ↔ angle a c d = rightangle)

  Betweeness forces equal angles across the middle to be right angles

• angle_extension {a b c b1 c1 : Point} {L M : Line} : b ≠ a → b1 ≠ a → c ≠ a → c1 ≠ a → OnLine a L → OnLine b L → OnLine b1 L → OnLine a M → OnLine c M → OnLine c1 M → ¬B b a b1 → ¬B c a c1 → angle b a c = angle b1 a c1

  A condition to extend angles in a predictable way

• unparallel_postulate {a b c d : Point} {L M N : Line} : b ≠ c → OnLine a L → OnLine b L → OnLine b M → OnLine c M → OnLine c N → OnLine d N → SameSide a d M → angle a b c + angle b c d < 2 * rightangle → ∃ (e : Point), OnLine e L ∧ OnLine e N ∧ SameSide e a M

  The unparallel postulate

• area_zero_iff_online {a b c : Point} {L : Line} : a ≠ b → OnLine a L → OnLine b L → (area a b c = 0 ↔ OnLine c L)

  Areas of degenerate triangles equal zero

• area_add_iff_B {a b c d : Point} {L : Line} : a ≠ b → b ≠ c → c ≠ a → OnLine a L → OnLine b L → OnLine c L → ¬OnLine d L → (B a b c ↔ area d a b + area d c b = area d a c)

  Areas adding on a triangle given a betweeness condition

• SAS_iff_SSS {a b c d e f : Point} : length a b = length d e → length a c = length d f → (angle b a c = angle e d f ↔ length b c = length e f)

  SAS is equivalent to SSS

def SyntheticEuclid4.diffside [i : IncidenceGeometry] (a b : IncidenceGeometry.Point) (L : IncidenceGeometry.Line) : Prop

Points being on different sides of a line

Equations

• SyntheticEuclid4.diffside a b L = (¬SyntheticEuclid4.IncidenceGeometry.OnLine a L ∧ ¬SyntheticEuclid4.IncidenceGeometry.OnLine b L ∧ ¬SyntheticEuclid4.IncidenceGeometry.SameSide a b L)

def SyntheticEuclid4.outCircle [i : IncidenceGeometry] (a : IncidenceGeometry.Point) (α : IncidenceGeometry.Circle) : Prop

A point being outside a circle

Equations

• SyntheticEuclid4.outCircle a α = (¬SyntheticEuclid4.IncidenceGeometry.OnCircle a α ∧ ¬SyntheticEuclid4.IncidenceGeometry.InCircle a α)

def SyntheticEuclid4.colinear [i : IncidenceGeometry] (a b c : IncidenceGeometry.Point) : Prop

Points being colinear

Equations

• One or more equations did not get rendered due to their size.

def SyntheticEuclid4.triangle [i : IncidenceGeometry] (a b c : IncidenceGeometry.Point) : Prop

Definition of a triangle

Equations

• SyntheticEuclid4.triangle a b c = ¬SyntheticEuclid4.colinear a b c

def SyntheticEuclid4.eqTri [i : IncidenceGeometry] (a b c : IncidenceGeometry.Point) : Prop

Definition of an equilateral triangle

Equations

• One or more equations did not get rendered due to their size.

def SyntheticEuclid4.isoTri [i : IncidenceGeometry] (a b c : IncidenceGeometry.Point) : Prop

Definition of an isosoles triangle

Equations

• SyntheticEuclid4.isoTri a b c = (SyntheticEuclid4.triangle a b c ∧ SyntheticEuclid4.IncidenceGeometry.length a b = SyntheticEuclid4.IncidenceGeometry.length a c)

def SyntheticEuclid4.para [i : IncidenceGeometry] (M N : IncidenceGeometry.Line) : Prop

Definition of parallel

Equations

• SyntheticEuclid4.para M N = ∀ (e : SyntheticEuclid4.IncidenceGeometry.Point), ¬SyntheticEuclid4.IncidenceGeometry.OnLine e M ∨ ¬SyntheticEuclid4.IncidenceGeometry.OnLine e N

def SyntheticEuclid4.paragram [i : IncidenceGeometry] (a b c d : IncidenceGeometry.Point) (L M N O : IncidenceGeometry.Line) : Prop

Definition of parallelogram

Equations

• One or more equations did not get rendered due to their size.

def SyntheticEuclid4.square [i : IncidenceGeometry] (a b c d : IncidenceGeometry.Point) : Prop

Definition of a square

Equations

• One or more equations did not get rendered due to their size.