Basic Classes in Euclidean Geometry

In this file, we define classes that will be used in Euclidean geometry. In this file, classes for carriers and classes for notations will be defined.

Main Definitions

• Fig : The class of plane figures equipped with a carrier set.
• Interior : The class of plane figures with interior, further equipped with a interior set.
• HasCongr : The carrying class of the equivalent relation congruence.
• HasACongr : The carrying class of the symmetric relation anti-congruence.
• HasSim : The carrying class of the equivalent relation similarity.
• HasASimr : The carrying class of the symmetric relation anti-similarity.

Notations

• LiesOn : A point belongs to the carrier of a specific figure.
• LiesInt : A point belongs to the interior of a specific figure.
• IsInx : A point belongs to both carrier of two specific figures.
• InxWith : The carriers of two figures have a common point.
• IsCongrTo, ≅ : the notation for congruence relation
• IsACongrTo, ≅ₐ : the notation for anti-congruence relation
• IsSimTo, ∼ : the notation for similarity relation
• IsASimTo, ∼ₐ : the notation for anti-similarity relation

Further Works

1. The property concurrent (maybe we should extend to an arbitary number of figures version), the class Convex_2D is defined, but not actually in use.
2. Make HasACongr extends HasCongr, and requires transitivity relations between them in the class.

@[inline, reducible]

abbrev EuclidGeom.PtNe {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) : Prop

Equations

• EuclidGeom.PtNe A B = Fact (A ≠ B)

instance EuclidGeom.PtNe.symm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [h : EuclidGeom.PtNe A B] : EuclidGeom.PtNe B A

Equations

• (_ : EuclidGeom.PtNe B A) = (_ : Fact (B ≠ A))

@[simp]

theorem EuclidGeom.pt_ne {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [h : EuclidGeom.PtNe A B] : A ≠ B

class EuclidGeom.Fig (α : Type u_2) (P : outParam (Type u_3)) : Type (max u_2 u_3)

The class of plane figures. We say α is a plane figure, if for every given Euclidean plane P, α P is a collection of specific figures on P, each equipped with a carrier set of type Set P.

• carrier : α → Set P

class EuclidGeom.Interior (α : Type u_2) (P : outParam (Type u_3)) : Type (max u_2 u_3)

The class of plane figures with interior. We say α is with interior, if for every given Euclidean plane P, each element in the collection α P is equipped with an interior set of type Set P

• interior : α → Set P

class EuclidGeom.IntFig (α : Type u_2) (P : outParam (Type u_3)) extends EuclidGeom.Fig , EuclidGeom.Interior : Type (max u_2 u_3)

The class of plane figures with both carrier and interior. We say a plane figure α is with interior, if for every given Euclidean plane P, each element in the collection α P is equipped with bith a carrier set and an interior set of type Set P, and the interior set is contained in the carrier set.

• carrier : α → Set P
• interior : α → Set P
• interior_subset_carrier : ∀ (F : α), EuclidGeom.Interior.interior F ⊆ EuclidGeom.Fig.carrier F

def EuclidGeom.lies_on {P : Type u_1} {α : Type u_2} [EuclidGeom.Fig α P] (A : P) (F : α) : Prop

Equations

• EuclidGeom.lies_on A F = (A ∈ EuclidGeom.Fig.carrier F)

def EuclidGeom.lies_int {P : Type u_1} {α : Type u_2} [EuclidGeom.Interior α P] (A : P) (F : α) : Prop

Equations

• EuclidGeom.lies_int A F = (A ∈ EuclidGeom.Interior.interior F)

def EuclidGeom.term_LiesOn_ : Lean.TrailingParserDescr

Equations

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

def EuclidGeom.term_LiesInt_ : Lean.TrailingParserDescr

Equations

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

instance EuclidGeom.instCoeLies_intToInteriorLies_onToFig {α : Type u_3} {P : Type u_2} [EuclidGeom.IntFig α P] (A : P) (F : α) : Coe (EuclidGeom.lies_int A F) (EuclidGeom.lies_on A F)

Equations

• EuclidGeom.instCoeLies_intToInteriorLies_onToFig A F = { coe := (_ : EuclidGeom.lies_int A F → A ∈ EuclidGeom.Fig.carrier F) }

def EuclidGeom.is_inx {α : Type u_3} {β : Type u_4} {P : Type u_2} [EuclidGeom.Fig α P] [EuclidGeom.Fig β P] (A : P) (F : α) (G : β) : Prop

Equations

• EuclidGeom.is_inx A F G = (EuclidGeom.lies_on A F ∧ EuclidGeom.lies_on A G)

def EuclidGeom.term_IsInxOf__ : Lean.TrailingParserDescr

Equations

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

theorem EuclidGeom.is_inx.symm {α : Type u_3} {β : Type u_4} {P : Type u_2} [EuclidGeom.Fig α P] [EuclidGeom.Fig β P] {A : P} {F : α} {G : β} (h : EuclidGeom.is_inx A F G) : EuclidGeom.is_inx A G F

def EuclidGeom.intersect {α : Type u_3} {β : Type u_4} {P : Type u_2} [EuclidGeom.Fig α P] [EuclidGeom.Fig β P] (F : α) (G : β) : Prop

Equations

• EuclidGeom.intersect F G = ∃ (A : P), EuclidGeom.lies_on A F ∧ EuclidGeom.lies_on A G

def EuclidGeom.term_InxWith_ : Lean.TrailingParserDescr

Equations

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

theorem EuclidGeom.intersect.symm {α : Type u_3} {β : Type u_4} {P : Type u_2} [EuclidGeom.Fig α P] [EuclidGeom.Fig β P] {F : α} {G : β} (h : EuclidGeom.intersect F G) : EuclidGeom.intersect G F

theorem EuclidGeom.ne_of_lieson_and_not_lieson {α : Type u_3} {P : Type u_2} [EuclidGeom.Fig α P] {F : α} {X : P} {Y : P} (hx : EuclidGeom.lies_on X F) (hy : ¬EuclidGeom.lies_on Y F) : X ≠ Y

theorem EuclidGeom.ne_of_liesint_and_not_liesint {α : Type u_3} {P : Type u_2} [EuclidGeom.Interior α P] {F : α} {X : P} {Y : P} (hx : EuclidGeom.lies_int X F) (hy : ¬EuclidGeom.lies_int Y F) : X ≠ Y

def EuclidGeom.concurrent {α : Type u_3} {β : Type u_4} {γ : Type u_5} {P : Type u_2} [EuclidGeom.EuclideanPlane P] [EuclidGeom.Fig α P] [EuclidGeom.Fig β P] [EuclidGeom.Fig γ P] (A : P) (F : α) (G : β) (H : γ) : Prop

Equations

• EuclidGeom.concurrent A F G H = (EuclidGeom.lies_on A F ∧ EuclidGeom.lies_on A G ∧ EuclidGeom.lies_on A H)

class EuclidGeom.Convex2D (α : Type u_2) (P : outParam (Type u_3)) [outParam (EuclidGeom.EuclideanPlane P)] extends EuclidGeom.IntFig : Type (max u_2 u_3)

• carrier : α → Set P
• interior : α → Set P
• interior_subset_carrier : ∀ (F : α), EuclidGeom.Interior.interior F ⊆ EuclidGeom.Fig.carrier F
• convexity : ∀ (F : α) (A B : P), EuclidGeom.lies_on A F → EuclidGeom.lies_on B F → ∃ (t : ℝ), EuclidGeom.lies_on (t • (B -ᵥ A) +ᵥ A) F
• int_of_carrier : ∀ (F : α) (A : P), EuclidGeom.lies_int A F → ∃ (B₁ : P) (B₂ : P) (B₃ : P) (t₁ : ℝ) (t₂ : ℝ) (t₃ : ℝ), EuclidGeom.lies_on B₁ F ∧ EuclidGeom.lies_on B₂ F ∧ EuclidGeom.lies_on B₃ F ∧ 0 < t₁ ∧ 0 < t₂ ∧ 0 < t₃ ∧ t₁ • EuclidGeom.Vec.mkPtPt A B₁ + t₂ • EuclidGeom.Vec.mkPtPt A B₂ + t₃ • EuclidGeom.Vec.mkPtPt A B₃ = 0

class EuclidGeom.HasCongr (α : Type u_2) : Type u_2

• congr : α → α → Prop
• refl : ∀ (a : α), EuclidGeom.HasCongr.congr a a
• trans : ∀ {a b c : α}, EuclidGeom.HasCongr.congr a b → EuclidGeom.HasCongr.congr b c → EuclidGeom.HasCongr.congr a c
• symm : ∀ {a b : α}, EuclidGeom.HasCongr.congr a b → EuclidGeom.HasCongr.congr b a

instance EuclidGeom.instIsEquivCongr (α : Type u_2) [EuclidGeom.HasCongr α] : IsEquiv α EuclidGeom.HasCongr.congr

Equations

• (_ : IsEquiv α EuclidGeom.HasCongr.congr) = (_ : IsEquiv α EuclidGeom.HasCongr.congr)

def EuclidGeom.term_IsCongrTo_ : Lean.TrailingParserDescr

Equations

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

def EuclidGeom.«term_≅_» : Lean.TrailingParserDescr

Equations

• EuclidGeom.«term_≅_» = Lean.ParserDescr.trailingNode `EuclidGeom.term_≅_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≅ ") (Lean.ParserDescr.cat `term 51))

class EuclidGeom.HasACongr (α : Type u_2) : Type u_2

• acongr : α → α → Prop
• symm : ∀ {a b : α}, EuclidGeom.HasACongr.acongr a b → EuclidGeom.HasACongr.acongr b a

instance EuclidGeom.instIsSymmAcongr (α : Type u_2) [EuclidGeom.HasACongr α] : IsSymm α EuclidGeom.HasACongr.acongr

Equations

• (_ : IsSymm α EuclidGeom.HasACongr.acongr) = (_ : IsSymm α EuclidGeom.HasACongr.acongr)

def EuclidGeom.term_IsACongrTo_ : Lean.TrailingParserDescr

Equations

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

def EuclidGeom.«term_≅ₐ_» : Lean.TrailingParserDescr

Equations

• EuclidGeom.«term_≅ₐ_» = Lean.ParserDescr.trailingNode `EuclidGeom.term_≅ₐ_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≅ₐ ") (Lean.ParserDescr.cat `term 51))

class EuclidGeom.HasSim (α : Type u_2) : Type u_2

• sim : α → α → Prop
• refl : ∀ (a : α), EuclidGeom.HasSim.sim a a
• trans : ∀ {a b c : α}, EuclidGeom.HasSim.sim a b → EuclidGeom.HasSim.sim b c → EuclidGeom.HasSim.sim a c
• symm : ∀ {a b : α}, EuclidGeom.HasSim.sim a b → EuclidGeom.HasSim.sim b a

instance EuclidGeom.instIsEquivSim (α : Type u_2) [EuclidGeom.HasSim α] : IsEquiv α EuclidGeom.HasSim.sim

Equations

• (_ : IsEquiv α EuclidGeom.HasSim.sim) = (_ : IsEquiv α EuclidGeom.HasSim.sim)

def EuclidGeom.term_IsSimTo_ : Lean.TrailingParserDescr

The similarity relation is denoted by infix "IsSimTo".

Equations

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

def EuclidGeom.«term_∼_» : Lean.TrailingParserDescr

The similarity relation is denoted by infix $\sim$.

Equations

• EuclidGeom.«term_∼_» = Lean.ParserDescr.trailingNode `EuclidGeom.term_∼_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∼ ") (Lean.ParserDescr.cat `term 51))

class EuclidGeom.HasASim (α : Type u_2) : Type u_2

• asim : α → α → Prop
• symm : ∀ {a b : α}, EuclidGeom.HasASim.asim a b → EuclidGeom.HasASim.asim b a

instance EuclidGeom.instIsSymmAcongr_1 (α : Type u_2) [EuclidGeom.HasACongr α] : IsSymm α EuclidGeom.HasACongr.acongr

Equations

• (_ : IsSymm α EuclidGeom.HasACongr.acongr) = (_ : IsSymm α EuclidGeom.HasACongr.acongr)

def EuclidGeom.term_IsASimTo_ : Lean.TrailingParserDescr

The anti-similarity relation is denoted by infix "IsASimTo".

Equations

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

def EuclidGeom.«term_∼ₐ_» : Lean.TrailingParserDescr

The anti-similarity relation is denoted by infix $\sim_a$.

Equations

• EuclidGeom.«term_∼ₐ_» = Lean.ParserDescr.trailingNode `EuclidGeom.term_∼ₐ_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∼ₐ ") (Lean.ParserDescr.cat `term 51))