Quadrilateral

In this file we define general quadrilaterals as four points on the plane and convex quadrilaterals.

Important Definitions

• Quadrilateral P : general quadrilaterals on the plane P, i.e. four points on P
• QuadrilateralND P : quadrilaterals on the plane P s.t. the points that adjacent is not same
• Quadrilateral_cvx P : convex quadrilaterals on the plane P

Notation

• QDR A B C D : notation for quadrilateral A B C D

Implementation Notes

Currently, we just defines general quadrilaterals, non-degenerate quadrilateral (adjacent points are not the same, or cyclic-non-degenerate) and convex quadrilaterals. There are classes in between. For example, quadrilateral without self-intersection, quadrilateral of stronger non-degenerate (any two points are not same, we call it alternatively-non-degenerate temporarily). Of course many definitions work on these classes already, but without necessarity in application, we will not formalize these class for present.

theorem EuclidGeom.Quadrilateral.ext {P : Type u_1} : ∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.Quadrilateral P), x.point₁ = y.point₁ → x.point₂ = y.point₂ → x.point₃ = y.point₃ → x.point₄ = y.point₄ → x = y

theorem EuclidGeom.Quadrilateral.ext_iff {P : Type u_1} : ∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.Quadrilateral P), x = y ↔ x.point₁ = y.point₁ ∧ x.point₂ = y.point₂ ∧ x.point₃ = y.point₃ ∧ x.point₄ = y.point₄

structure EuclidGeom.Quadrilateral (P : Type u_1) [EuclidGeom.EuclideanPlane P] : Type u_1

Class of Quadrilateral: A quadrilateral consists of four points; it is the generalized quadrilateral formed by these four points

• point₁ : P
• point₂ : P
• point₃ : P
• point₄ : P

def EuclidGeom.termQDR : Lean.ParserDescr

For four points $A$ $B$ $C$ $D$ on a plane, instead of writing Quadrilateral.mk $A$ $B$ $C$ $D$ for the quadrilateral formed by $A$ $B$ $C$ $D$, we use QDR $A$ $B$ $C$ $D$ to denote such a quadrilateral.

Equations

• EuclidGeom.termQDR = Lean.ParserDescr.node `EuclidGeom.termQDR 1024 (Lean.ParserDescr.symbol "QDR")

def EuclidGeom.Quadrilateral.edge₁₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {qdr : EuclidGeom.Quadrilateral P} : EuclidGeom.Seg P

Given a quadrilateral qdr, qdr.edge₁₂ is the edge from the first point to the second point of a quadrilateral.

Equations

• EuclidGeom.Quadrilateral.edge₁₂ = { source := qdr.point₁, target := qdr.point₂ }

def EuclidGeom.Quadrilateral.edge₂₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {qdr : EuclidGeom.Quadrilateral P} : EuclidGeom.Seg P

The edge from the second point to the third point of a quadrilateral

Equations

• EuclidGeom.Quadrilateral.edge₂₃ = { source := qdr.point₂, target := qdr.point₃ }

def EuclidGeom.Quadrilateral.edge₃₄ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {qdr : EuclidGeom.Quadrilateral P} : EuclidGeom.Seg P

The edge from the third point to the fourth point of a quadrilateral

Equations

• EuclidGeom.Quadrilateral.edge₃₄ = { source := qdr.point₃, target := qdr.point₄ }

def EuclidGeom.Quadrilateral.edge₁₄ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {qdr : EuclidGeom.Quadrilateral P} : EuclidGeom.Seg P

The edge from the 1st point to the 4th point of a quadrilateral

Equations

• EuclidGeom.Quadrilateral.edge₁₄ = { source := qdr.point₁, target := qdr.point₄ }

def EuclidGeom.Quadrilateral.diag₁₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {qdr : EuclidGeom.Quadrilateral P} : EuclidGeom.Seg P

The diagonal from the first point to the third point of a quadrilateral

Equations

• EuclidGeom.Quadrilateral.diag₁₃ = { source := qdr.point₁, target := qdr.point₃ }

def EuclidGeom.Quadrilateral.diag₂₄ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {qdr : EuclidGeom.Quadrilateral P} : EuclidGeom.Seg P

The diagonal from the second point to the fourth point of a quadrilateral

Equations

• EuclidGeom.Quadrilateral.diag₂₄ = { source := qdr.point₂, target := qdr.point₄ }

def EuclidGeom.Quadrilateral.perm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {qdr : EuclidGeom.Quadrilateral P} : EuclidGeom.Quadrilateral P

The perm quadrilateral, the first point of the perm is the second point of the origin, etc.

Equations

• EuclidGeom.Quadrilateral.perm = { point₁ := qdr.point₂, point₂ := qdr.point₃, point₃ := qdr.point₄, point₄ := qdr.point₁ }

def EuclidGeom.Quadrilateral.flip {P : Type u_1} [EuclidGeom.EuclideanPlane P] {qdr : EuclidGeom.Quadrilateral P} : EuclidGeom.Quadrilateral P

The flip quadrilateral, exchanged the second point and the fourth.

Equations

• EuclidGeom.Quadrilateral.flip = { point₁ := qdr.point₁, point₂ := qdr.point₄, point₃ := qdr.point₃, point₄ := qdr.point₂ }

@[simp]

theorem EuclidGeom.Quadrilateral.edge₁₂_simp {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) : EuclidGeom.Quadrilateral.edge₁₂ = { source := A, target := B }

@[simp]

theorem EuclidGeom.Quadrilateral.edge₂₃_simp {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) : EuclidGeom.Quadrilateral.edge₂₃ = { source := B, target := C }

@[simp]

theorem EuclidGeom.Quadrilateral.edge₃₄_simp {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) : EuclidGeom.Quadrilateral.edge₃₄ = { source := C, target := D }

@[simp]

theorem EuclidGeom.Quadrilateral.edge₁₄_simp {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) : EuclidGeom.Quadrilateral.edge₁₄ = { source := A, target := D }

@[simp]

theorem EuclidGeom.Quadrilateral.diag₁₃_simp {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) : EuclidGeom.Quadrilateral.diag₁₃ = { source := A, target := C }

@[simp]

theorem EuclidGeom.Quadrilateral.diag₂₄_simp {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) : EuclidGeom.Quadrilateral.diag₂₄ = { source := B, target := D }

@[simp]

theorem EuclidGeom.Quadrilateral.perm_simp {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) : EuclidGeom.Quadrilateral.perm = { point₁ := B, point₂ := C, point₃ := D, point₄ := A }

@[simp]

theorem EuclidGeom.Quadrilateral.flip_simp {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) : EuclidGeom.Quadrilateral.flip = { point₁ := A, point₂ := D, point₃ := C, point₄ := B }

structure EuclidGeom.Quadrilateral.IsND {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr : EuclidGeom.Quadrilateral P) : Prop

A quadrilateral is called non-degenerate if the points that adjacent is not same

• nd₁₂ : qdr.point₂ ≠ qdr.point₁
• nd₂₃ : qdr.point₃ ≠ qdr.point₂
• nd₃₄ : qdr.point₄ ≠ qdr.point₃
• nd₁₄ : qdr.point₄ ≠ qdr.point₁

theorem EuclidGeom.QuadrilateralND.ext {P : Type u_1} : ∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.QuadrilateralND P), x.point₁ = y.point₁ → x.point₂ = y.point₂ → x.point₃ = y.point₃ → x.point₄ = y.point₄ → x = y

theorem EuclidGeom.QuadrilateralND.ext_iff {P : Type u_1} : ∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.QuadrilateralND P), x = y ↔ x.point₁ = y.point₁ ∧ x.point₂ = y.point₂ ∧ x.point₃ = y.point₃ ∧ x.point₄ = y.point₄

structure EuclidGeom.QuadrilateralND (P : Type u_1) [EuclidGeom.EuclideanPlane P] extends EuclidGeom.Quadrilateral : Type u_1

Class of nd Quadrilateral: A nd quadrilateral is quadrilateral with the property of nd.

• point₁ : P
• point₂ : P
• point₃ : P
• point₄ : P
• nd : s.IsND

def EuclidGeom.QuadrilateralND.mk_pt_pt_pt_pt_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) (h : { point₁ := A, point₂ := B, point₃ := C, point₄ := D }.IsND) : EuclidGeom.QuadrilateralND P

Equations

• EuclidGeom.QuadrilateralND.mk_pt_pt_pt_pt_nd A B C D h = { toQuadrilateral := { point₁ := A, point₂ := B, point₃ := C, point₄ := D }, nd := h }

def EuclidGeom.termQDR_nd : Lean.ParserDescr

Equations

• EuclidGeom.termQDR_nd = Lean.ParserDescr.node `EuclidGeom.termQDR_nd 1024 (Lean.ParserDescr.symbol "QDR_nd")

def EuclidGeom.QuadrilateralND.mk_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] {qdr : EuclidGeom.Quadrilateral P} (h : qdr.IsND) : EuclidGeom.QuadrilateralND P

Given a property that a quadrilateral qdr is nd, this function returns qdr itself as an object in the class of nd quadrilateral

Equations

• EuclidGeom.QuadrilateralND.mk_nd h = { toQuadrilateral := qdr, nd := h }

def EuclidGeom.termQDR_nd' : Lean.ParserDescr

Equations

• EuclidGeom.termQDR_nd' = Lean.ParserDescr.node `EuclidGeom.termQDR_nd' 1024 (Lean.ParserDescr.symbol "QDR_nd'")

structure EuclidGeom.Quadrilateral.InGPos {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr : EuclidGeom.Quadrilateral P) : Prop

A quadrilateral satisfies InGPos if every 3 vertices are not collinear.

• not_collinear₁₂₃ : ¬EuclidGeom.Collinear qdr.point₁ qdr.point₂ qdr.point₃
• not_collinear₂₃₄ : ¬EuclidGeom.Collinear qdr.point₂ qdr.point₃ qdr.point₄
• not_collinear₃₄₁ : ¬EuclidGeom.Collinear qdr.point₃ qdr.point₄ qdr.point₁
• not_collinear₄₁₂ : ¬EuclidGeom.Collinear qdr.point₄ qdr.point₁ qdr.point₂

instance EuclidGeom.QuadrilateralND.nd₁₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : EuclidGeom.PtNe qdr_nd.point₂ qdr_nd.point₁

The edge from the first point to the second point of a QuadrilateralND is non-degenerate.

Equations

• (_ : EuclidGeom.PtNe qdr_nd.point₂ qdr_nd.point₁) = (_ : Fact (qdr_nd.point₂ ≠ qdr_nd.point₁))

instance EuclidGeom.QuadrilateralND.nd₂₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : EuclidGeom.PtNe qdr_nd.point₃ qdr_nd.point₂

The edge from the first point to the second point of a QuadrilateralND is non-degenerate.

Equations

• (_ : EuclidGeom.PtNe qdr_nd.point₃ qdr_nd.point₂) = (_ : Fact (qdr_nd.point₃ ≠ qdr_nd.point₂))

instance EuclidGeom.QuadrilateralND.nd₃₄ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : EuclidGeom.PtNe qdr_nd.point₄ qdr_nd.point₃

The edge from the first point to the second point of a QuadrilateralND is non-degenerate.

Equations

• (_ : EuclidGeom.PtNe qdr_nd.point₄ qdr_nd.point₃) = (_ : Fact (qdr_nd.point₄ ≠ qdr_nd.point₃))

instance EuclidGeom.QuadrilateralND.nd₁₄ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : EuclidGeom.PtNe qdr_nd.point₄ qdr_nd.point₁

The edge from the first point to the second point of a QuadrilateralND is non-degenerate.

Equations

• (_ : EuclidGeom.PtNe qdr_nd.point₄ qdr_nd.point₁) = (_ : Fact (qdr_nd.point₄ ≠ qdr_nd.point₁))

def EuclidGeom.QuadrilateralND.edgeND₁₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : EuclidGeom.SegND P

The edge from the first point to the second point of a quadrilateral

Equations

• qdr_nd.edgeND₁₂ = SEG_nd qdr_nd.point₁ qdr_nd.point₂ (_ : qdr_nd.point₂ ≠ qdr_nd.point₁)

def EuclidGeom.QuadrilateralND.edgeND₂₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : EuclidGeom.SegND P

The edge from the second point to the third point of a quadrilateral

Equations

• qdr_nd.edgeND₂₃ = SEG_nd qdr_nd.point₂ qdr_nd.point₃ (_ : qdr_nd.point₃ ≠ qdr_nd.point₂)

def EuclidGeom.QuadrilateralND.edgeND₃₄ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : EuclidGeom.SegND P

The edge from the third point to the fourth point of a quadrilateral

Equations

• qdr_nd.edgeND₃₄ = SEG_nd qdr_nd.point₃ qdr_nd.point₄ (_ : qdr_nd.point₄ ≠ qdr_nd.point₃)

def EuclidGeom.QuadrilateralND.edgeND₄₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : EuclidGeom.SegND P

The edge from the fourth point to the first point of a quadrilateral

Equations

• qdr_nd.edgeND₄₁ = SEG_nd qdr_nd.point₄ qdr_nd.point₁ (_ : qdr_nd.point₁ ≠ qdr_nd.point₄)

def EuclidGeom.QuadrilateralND.angle₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : EuclidGeom.Angle P

angle at point₁ of qdr_nd

Equations

• qdr_nd.angle₁ = ANG qdr_nd.point₄ qdr_nd.point₁ qdr_nd.point₂ (_ : qdr_nd.point₄ ≠ qdr_nd.point₁) (_ : qdr_nd.point₂ ≠ qdr_nd.point₁)

def EuclidGeom.QuadrilateralND.angle₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : EuclidGeom.Angle P

angle at point₂ of qdr_nd

Equations

• qdr_nd.angle₂ = ANG qdr_nd.point₁ qdr_nd.point₂ qdr_nd.point₃ (_ : qdr_nd.point₁ ≠ qdr_nd.point₂) (_ : qdr_nd.point₃ ≠ qdr_nd.point₂)

def EuclidGeom.QuadrilateralND.angle₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : EuclidGeom.Angle P

angle at point₃ of qdr_nd

Equations

• qdr_nd.angle₃ = ANG qdr_nd.point₂ qdr_nd.point₃ qdr_nd.point₄ (_ : qdr_nd.point₂ ≠ qdr_nd.point₃) (_ : qdr_nd.point₄ ≠ qdr_nd.point₃)

def EuclidGeom.QuadrilateralND.angle₄ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : EuclidGeom.Angle P

angle at point₄ of qdr_nd

Equations

• qdr_nd.angle₄ = ANG qdr_nd.point₃ qdr_nd.point₄ qdr_nd.point₁ (_ : qdr_nd.point₃ ≠ qdr_nd.point₄) (_ : qdr_nd.point₁ ≠ qdr_nd.point₄)

def EuclidGeom.QuadrilateralND.triangle₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : EuclidGeom.Triangle P

triangle point₄ point₁ point₂, which includes angle₁

Equations

• qdr_nd.triangle₁ = { point₁ := qdr_nd.point₄, point₂ := qdr_nd.point₁, point₃ := qdr_nd.point₂ }

def EuclidGeom.QuadrilateralND.triangle₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : EuclidGeom.Triangle P

triangle point₁ point₂ point₃, which includes angle₂

Equations

• qdr_nd.triangle₂ = { point₁ := qdr_nd.point₁, point₂ := qdr_nd.point₂, point₃ := qdr_nd.point₃ }

def EuclidGeom.QuadrilateralND.triangle₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : EuclidGeom.Triangle P

triangle point₂ point₃ point₄, which includes angle₃

Equations

• qdr_nd.triangle₃ = { point₁ := qdr_nd.point₂, point₂ := qdr_nd.point₃, point₃ := qdr_nd.point₄ }

def EuclidGeom.QuadrilateralND.triangle₄ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : EuclidGeom.Triangle P

triangle point₃ point₄ point₁, which includes angle₄

Equations

• qdr_nd.triangle₄ = { point₁ := qdr_nd.point₃, point₂ := qdr_nd.point₄, point₃ := qdr_nd.point₁ }

theorem EuclidGeom.QuadrilateralND.perm_is_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : EuclidGeom.Quadrilateral.perm.IsND

The perm of QuadrilateralND is also QuadrilateralND.

def EuclidGeom.QuadrilateralND.perm {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : EuclidGeom.QuadrilateralND P

The perm QuadrilateralND, the first point of the perm is the second point of the origin, etc.

Equations

• qdr_nd.perm = EuclidGeom.QuadrilateralND.mk_nd (_ : EuclidGeom.Quadrilateral.perm.IsND)

theorem EuclidGeom.QuadrilateralND.flip_is_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : EuclidGeom.Quadrilateral.flip.IsND

The flip of QuadrilateralND is also QuadrilateralND.

def EuclidGeom.QuadrilateralND.flip {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : EuclidGeom.QuadrilateralND P

The flip QuadrilateralND, exchanged the second point and the fourth.

Equations

• qdr_nd.flip = EuclidGeom.QuadrilateralND.mk_nd (_ : EuclidGeom.Quadrilateral.flip.IsND)

theorem EuclidGeom.QuadrilateralND.flip_angle₁_value_eq_neg_angle₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : qdr_nd.flip.angle₁.value = -qdr_nd.angle₁.value

theorem EuclidGeom.QuadrilateralND.flip_angle₂_value_eq_neg_angle₄ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : qdr_nd.flip.angle₂.value = -qdr_nd.angle₄.value

theorem EuclidGeom.QuadrilateralND.flip_angle₃_value_eq_neg_angle₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : qdr_nd.flip.angle₃.value = -qdr_nd.angle₃.value

theorem EuclidGeom.QuadrilateralND.flip_angle₄_value_eq_neg_angle₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : qdr_nd.flip.angle₄.value = -qdr_nd.angle₂.value

theorem EuclidGeom.QuadrilateralND.nd_of_gpos {P : Type u_1} [EuclidGeom.EuclideanPlane P] {qdr : EuclidGeom.Quadrilateral P} (InGPos : qdr.InGPos) : qdr.IsND

A Quadrilateral which satisfies InGPos satisfies IsND.

instance EuclidGeom.QuadrilateralND.instCoeInGPosIsND {P : Type u_1} [EuclidGeom.EuclideanPlane P] {qdr : EuclidGeom.Quadrilateral P} : Coe qdr.InGPos qdr.IsND

Equations

• EuclidGeom.QuadrilateralND.instCoeInGPosIsND = { coe := (_ : qdr.InGPos → qdr.IsND) }

def EuclidGeom.Quadrilateral.IsConvex {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr : EuclidGeom.Quadrilateral P) : Prop

A Quadrilateral is called convex if it's ND and four angles have the same sign.

Equations

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

def EuclidGeom.term_IsConvex : Lean.TrailingParserDescr

Equations

• EuclidGeom.term_IsConvex = Lean.ParserDescr.trailingNode `EuclidGeom.term_IsConvex 50 50 (Lean.ParserDescr.symbol "IsConvex")

theorem EuclidGeom.Quadrilateral.isND_of_is_convex {P : Type u_1} [EuclidGeom.EuclideanPlane P] {qdr : EuclidGeom.Quadrilateral P} (h : qdr.IsConvex) : qdr.IsND

instance EuclidGeom.instCoeIsConvexIsND {P : Type u_1} [EuclidGeom.EuclideanPlane P] {qdr : EuclidGeom.Quadrilateral P} : Coe qdr.IsConvex qdr.IsND

Equations

• EuclidGeom.instCoeIsConvexIsND = { coe := (_ : qdr.IsConvex → qdr.IsND) }

theorem EuclidGeom.Quadrilateral.nd_cvx_iff_cvx {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : qdr_nd.IsConvex ↔ qdr_nd.angle₁.value.IsPos ∧ qdr_nd.angle₂.value.IsPos ∧ qdr_nd.angle₃.value.IsPos ∧ qdr_nd.angle₄.value.IsPos ∨ qdr_nd.angle₁.value.IsNeg ∧ qdr_nd.angle₂.value.IsNeg ∧ qdr_nd.angle₃.value.IsNeg ∧ qdr_nd.angle₄.value.IsNeg

theorem EuclidGeom.Quadrilateral_cvx.nd_is_convex_iff_is_convex {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : qdr_nd.IsConvex ↔ qdr_nd.IsConvex

instance EuclidGeom.instCoeIsConvexToQuadrilateral {P : Type u_1} [EuclidGeom.EuclideanPlane P] {qdr_nd : EuclidGeom.QuadrilateralND P} : Coe qdr_nd.IsConvex qdr_nd.IsConvex

Equations

• EuclidGeom.instCoeIsConvexToQuadrilateral = { coe := (_ : qdr_nd.IsConvex → qdr_nd.IsConvex) }

instance EuclidGeom.instCoeIsConvexToQuadrilateral_1 {P : Type u_1} [EuclidGeom.EuclideanPlane P] {qdr_nd : EuclidGeom.QuadrilateralND P} : Coe qdr_nd.IsConvex qdr_nd.IsConvex

Equations

• EuclidGeom.instCoeIsConvexToQuadrilateral_1 = { coe := (_ : qdr_nd.IsConvex → qdr_nd.IsConvex) }

theorem EuclidGeom.Quadrilateral_cvx.ext_iff {P : Type u_1} : ∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.Quadrilateral_cvx P), x = y ↔ x.point₁ = y.point₁ ∧ x.point₂ = y.point₂ ∧ x.point₃ = y.point₃ ∧ x.point₄ = y.point₄

theorem EuclidGeom.Quadrilateral_cvx.ext {P : Type u_1} : ∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.Quadrilateral_cvx P), x.point₁ = y.point₁ → x.point₂ = y.point₂ → x.point₃ = y.point₃ → x.point₄ = y.point₄ → x = y

structure EuclidGeom.Quadrilateral_cvx (P : Type u_1) [EuclidGeom.EuclideanPlane P] extends EuclidGeom.QuadrilateralND : Type u_1

Class of Convex Quadrilateral: A convex quadrilateral is quadrilateral with the property of convex.

• point₁ : P
• point₂ : P
• point₃ : P
• point₄ : P
• nd : s.IsND
• convex : s.IsConvex

def EuclidGeom.Quadrilateral_cvx.mk_pt_pt_pt_pt_convex {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) (h : { point₁ := A, point₂ := B, point₃ := C, point₄ := D }.IsConvex) : EuclidGeom.Quadrilateral_cvx P

Equations

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

def EuclidGeom.termQDR_cvx : Lean.ParserDescr

Equations

• EuclidGeom.termQDR_cvx = Lean.ParserDescr.node `EuclidGeom.termQDR_cvx 1024 (Lean.ParserDescr.symbol "QDR_cvx")

def EuclidGeom.Quadrilateral_cvx.mk_cvx {P : Type u_1} [EuclidGeom.EuclideanPlane P] {qdr : EuclidGeom.Quadrilateral P} (h : qdr.IsConvex) : EuclidGeom.Quadrilateral_cvx P

Equations

• EuclidGeom.Quadrilateral_cvx.mk_cvx h = { toQuadrilateralND := EuclidGeom.QuadrilateralND.mk_nd (_ : qdr.IsND), convex := h }

def EuclidGeom.termQDR_cvx' : Lean.ParserDescr

Equations

• EuclidGeom.termQDR_cvx' = Lean.ParserDescr.node `EuclidGeom.termQDR_cvx' 1024 (Lean.ParserDescr.symbol "QDR_cvx'")

structure EuclidGeom.Quadrilateral_cvx.is_convex_of_three_sides_of_same_side' {P : Type u_1} [EuclidGeom.EuclideanPlane P] : Type u_1

• qdr_nd : EuclidGeom.QuadrilateralND P
• same_side₁ : EuclidGeom.odist_sign s.qdr_nd.point₁ s.qdr_nd.edgeND₃₄ = EuclidGeom.odist_sign s.qdr_nd.point₂ s.qdr_nd.edgeND₃₄
• same_side₂ : EuclidGeom.odist_sign s.qdr_nd.point₂ s.qdr_nd.edgeND₄₁ = EuclidGeom.odist_sign s.qdr_nd.point₃ s.qdr_nd.edgeND₄₁
• same_side₃ : EuclidGeom.odist_sign s.qdr_nd.point₃ s.qdr_nd.edgeND₁₂ = EuclidGeom.odist_sign s.qdr_nd.point₄ s.qdr_nd.edgeND₁₂

theorem EuclidGeom.Quadrilateral_cvx.is_convex_of_three_sides_of_same_side {P : Type u_1} [EuclidGeom.EuclideanPlane P] (p : EuclidGeom.Quadrilateral_cvx.is_convex_of_three_sides_of_same_side') : p.qdr_nd.IsConvex

structure EuclidGeom.Quadrilateral_cvx.is_convex_of_diag_inx_lies_int' {P : Type u_1} [EuclidGeom.EuclideanPlane P] : Type u_1

• qdr : EuclidGeom.Quadrilateral P
• ne₁ : s.qdr.point₁ ≠ s.qdr.point₃
• ne₂ : s.qdr.point₂ ≠ s.qdr.point₄
• diag₁₃ : EuclidGeom.SegND P
• diag₂₄ : EuclidGeom.SegND P
• not_para : ¬EuclidGeom.Parallel s.diag₁₃ s.diag₂₄
• inx_lies_int₁ : EuclidGeom.lies_int (EuclidGeom.Line.inx s.diag₁₃.toLine s.diag₂₄.toLine (_ : ¬EuclidGeom.Parallel s.diag₁₃ s.diag₂₄)) s.diag₁₃
• inx_lies_int₂ : EuclidGeom.lies_int (EuclidGeom.Line.inx s.diag₁₃.toLine s.diag₂₄.toLine (_ : ¬EuclidGeom.Parallel s.diag₁₃ s.diag₂₄)) s.diag₂₄

theorem EuclidGeom.Quadrilateral_cvx.is_convex_of_diag_inx_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] (p : EuclidGeom.Quadrilateral_cvx.is_convex_of_diag_inx_lies_int') : p.qdr.IsConvex

theorem EuclidGeom.Quadrilateral_cvx.perm_is_convex {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : qdr_cvx.perm.IsConvex

The perm of quadrilateral_cvx is also quadrilateral_cvx.

def EuclidGeom.Quadrilateral_cvx.perm {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : EuclidGeom.Quadrilateral_cvx P

The perm quadrilateral_cvx, the first point of the perm is the second point of the origin, etc.

Equations

• EuclidGeom.Quadrilateral_cvx.perm qdr_cvx = EuclidGeom.Quadrilateral_cvx.mk_cvx (_ : qdr_cvx.perm.IsConvex)

theorem EuclidGeom.Quadrilateral_cvx.perm_is_convex' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : { point₁ := qdr_cvx.point₂, point₂ := qdr_cvx.point₃, point₃ := qdr_cvx.point₄, point₄ := qdr_cvx.point₁ }.IsConvex

Given a convex quadrilateral qdr_cvx ABCD, quadrilateral QDR BCDA is also convex.

theorem EuclidGeom.Quadrilateral_cvx.is_convex_iff_perm_is_convex {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : qdr_nd.IsConvex ↔ qdr_nd.perm.IsConvex

theorem EuclidGeom.Quadrilateral_cvx.flip_is_convex {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : qdr_cvx.flip.IsConvex

The flip of quadrilateral_cvx is also quadrilateral_cvx.

def EuclidGeom.Quadrilateral_cvx.flip {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : EuclidGeom.Quadrilateral_cvx P

Equations

• EuclidGeom.Quadrilateral_cvx.flip qdr_cvx = EuclidGeom.Quadrilateral_cvx.mk_cvx (_ : qdr_cvx.flip.IsConvex)

theorem EuclidGeom.Quadrilateral_cvx.is_convex_iff_flip_is_convex {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : qdr_nd.IsConvex ↔ qdr_nd.flip.IsConvex

instance EuclidGeom.Quadrilateral_cvx.nd₁₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : EuclidGeom.PtNe qdr_cvx.point₃ qdr_cvx.point₁

Given a convex quadrilateral qdr_cvx, diagonal from the first point to the second point is not degenerate, i.e. the second point is not equal to the first point.

Equations

• (_ : EuclidGeom.PtNe qdr_cvx.point₃ qdr_cvx.point₁) = (_ : Fact (qdr_cvx.point₃ ≠ qdr_cvx.point₁))

instance EuclidGeom.Quadrilateral_cvx.nd₂₄ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : EuclidGeom.PtNe qdr_cvx.point₄ qdr_cvx.point₂

Given a convex quadrilateral qdr_cvx, diagonal from the first point to the second point is not degenerate, i.e. the second point is not equal to the first point.

Equations

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

def EuclidGeom.Quadrilateral_cvx.diag_nd₁₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : EuclidGeom.SegND P

The non-degenerate diagonal from the first point and third point of a convex quadrilateral

Equations

• EuclidGeom.Quadrilateral_cvx.diag_nd₁₃ qdr_cvx = SEG_nd qdr_cvx.point₁ qdr_cvx.point₃ (_ : qdr_cvx.point₃ ≠ qdr_cvx.point₁)

def EuclidGeom.Quadrilateral_cvx.diag_nd₂₄ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : EuclidGeom.SegND P

The non-degenerate diagonal from the second point and fourth point of a convex quadrilateral

Equations

• EuclidGeom.Quadrilateral_cvx.diag_nd₂₄ qdr_cvx = SEG_nd qdr_cvx.point₂ qdr_cvx.point₄ (_ : qdr_cvx.point₄ ≠ qdr_cvx.point₂)

theorem EuclidGeom.Quadrilateral_cvx.diag_not_para {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : ¬EuclidGeom.Parallel (EuclidGeom.Quadrilateral_cvx.diag_nd₁₃ qdr_cvx) (EuclidGeom.Quadrilateral_cvx.diag_nd₂₄ qdr_cvx)

Two diagonals are not parallel to each other

def EuclidGeom.Quadrilateral_cvx.diag_inx {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : P

The intersection point of two diagonals

Equations

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

theorem EuclidGeom.Quadrilateral_cvx.diag_inx_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : EuclidGeom.lies_int qdr_cvx.diag_inx (EuclidGeom.Quadrilateral_cvx.diag_nd₁₃ qdr_cvx) ∧ EuclidGeom.lies_int qdr_cvx.diag_inx (EuclidGeom.Quadrilateral_cvx.diag_nd₂₄ qdr_cvx)

The interior of two diagonals intersect at one point, i.e. the intersection point of the underlying lines of the diagonals lies in the interior of both diagonals.

theorem EuclidGeom.Quadrilateral_cvx.not_collinear₁₂₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : ¬EuclidGeom.Collinear qdr_cvx.point₁ qdr_cvx.point₂ qdr_cvx.point₃

Given a convex quadrilateral qdr_cvx, its 1st, 2nd and 3rd points are not collinear, i.e. the projective direction of the vector $\overrightarrow{point₁ point₂}$ is not the same as the projective direction of the vector $\overrightarrow{point₁ point₃}$.

theorem EuclidGeom.Quadrilateral_cvx.not_collinear₂₃₄ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : ¬EuclidGeom.Collinear qdr_cvx.point₂ qdr_cvx.point₃ qdr_cvx.point₄

Given a convex quadrilateral qdr_cvx, its 2nd, 3rd and 4th points are not collinear, i.e. the projective direction of the vector $\overrightarrow{point₂ point₃}$ is not the same as the projective direction of the vector $\overrightarrow{point₂ point₄}$.

theorem EuclidGeom.Quadrilateral_cvx.not_collinear₃₄₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : ¬EuclidGeom.Collinear qdr_cvx.point₃ qdr_cvx.point₄ qdr_cvx.point₁

Given a convex quadrilateral qdr_cvx, its 3rd, 4th and 1st points are not collinear, i.e. the projective direction of the vector $\overrightarrow{point₃ point₄}$ is not the same as the projective direction of the vector $\overrightarrow{point₃ point₁}$.

theorem EuclidGeom.Quadrilateral_cvx.not_collinear₄₁₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : ¬EuclidGeom.Collinear qdr_cvx.point₄ qdr_cvx.point₁ qdr_cvx.point₃

Given a convex quadrilateral qdr_cvx, its 4th, 1st and 3rd points are not collinear, i.e. the projective direction of the vector $\overrightarrow{point₃ point₄}$ is not the same as the projective direction of the vector $\overrightarrow{point₃ point₁}$.

theorem EuclidGeom.Quadrilateral_cvx.not_collinear₄₃₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : ¬EuclidGeom.Collinear qdr_cvx.point₄ qdr_cvx.point₃ qdr_cvx.point₁

Given a convex quadrilateral qdr_cvx, its 4th, 3rd and 1st points are not collinear, i.e. the projective direction of the vector $\overrightarrow{point₃ point₄}$ is not the same as the projective direction of the vector $\overrightarrow{point₃ point₁}$.

theorem EuclidGeom.Quadrilateral_cvx.not_collinear₁₄₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : ¬EuclidGeom.Collinear qdr_cvx.point₁ qdr_cvx.point₄ qdr_cvx.point₃

Given a convex quadrilateral qdr_cvx, its 1st, 4th and 3rd points are not collinear, i.e. the projective direction of the vector $\overrightarrow{point₃ point₄}$ is not the same as the projective direction of the vector $\overrightarrow{point₃ point₁}$.

theorem EuclidGeom.Quadrilateral_cvx.not_collinear₄₁₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : ¬EuclidGeom.Collinear qdr_cvx.point₄ qdr_cvx.point₁ qdr_cvx.point₂

Given a convex quadrilateral qdr_cvx, its 4th, 1st and 2nd points are not collinear, i.e. the projective direction of the vector $\overrightarrow{point₄ point₁}$ is not the same as the projective direction of the vector $\overrightarrow{point₄ point₂}$.

theorem EuclidGeom.Quadrilateral_cvx.not_collinear₂₁₄ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : ¬EuclidGeom.Collinear qdr_cvx.point₂ qdr_cvx.point₁ qdr_cvx.point₄

Given a convex quadrilateral qdr_cvx, its 2nd, 1st and 4th points are not collinear, i.e. the projective direction of the vector $\overrightarrow{point₄ point₁}$ is not the same as the projective direction of the vector $\overrightarrow{point₄ point₂}$.

theorem EuclidGeom.Quadrilateral_cvx.not_collinear₁₄₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : ¬EuclidGeom.Collinear qdr_cvx.point₁ qdr_cvx.point₄ qdr_cvx.point₂

Given a convex quadrilateral qdr_cvx, its 1st, 4th and 2nd points are not collinear, i.e. the projective direction of the vector $\overrightarrow{point₄ point₁}$ is not the same as the projective direction of the vector $\overrightarrow{point₄ point₂}$.

theorem EuclidGeom.Quadrilateral_cvx.not_collinear₁₂₄ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : ¬EuclidGeom.Collinear qdr_cvx.point₁ qdr_cvx.point₂ qdr_cvx.point₄

Given a convex quadrilateral qdr_cvx, its 1st, 2nd and 4th points are not collinear, i.e. the projective direction of the vector $\overrightarrow{point₄ point₁}$ is not the same as the projective direction of the vector $\overrightarrow{point₄ point₂}$.

def EuclidGeom.Quadrilateral_cvx.triangle_nd₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : EuclidGeom.TriangleND P

triangle point₄ point₁ point₂, which includes angle₁

Equations

• qdr_cvx.triangle_nd₁ = { val := qdr_cvx.triangle₁, property := (_ : ¬EuclidGeom.Collinear qdr_cvx.point₄ qdr_cvx.point₁ qdr_cvx.point₂) }

def EuclidGeom.Quadrilateral_cvx.triangle_nd₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : EuclidGeom.TriangleND P

triangle point₁ point₂ point₃, which includes angle₂

Equations

• qdr_cvx.triangle_nd₂ = { val := qdr_cvx.triangle₂, property := (_ : ¬EuclidGeom.Collinear qdr_cvx.point₁ qdr_cvx.point₂ qdr_cvx.point₃) }

def EuclidGeom.Quadrilateral_cvx.triangle_nd₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : EuclidGeom.TriangleND P

triangle point₂ point₃ point₄, which includes angle₃

Equations

• qdr_cvx.triangle_nd₃ = { val := qdr_cvx.triangle₃, property := (_ : ¬EuclidGeom.Collinear qdr_cvx.point₂ qdr_cvx.point₃ qdr_cvx.point₄) }

def EuclidGeom.Quadrilateral_cvx.triangle_nd₄ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : EuclidGeom.TriangleND P

triangle point₃ point₄ point₁, which includes angle₄

Equations

• qdr_cvx.triangle_nd₄ = { val := qdr_cvx.triangle₄, property := (_ : ¬EuclidGeom.Collinear qdr_cvx.point₃ qdr_cvx.point₄ qdr_cvx.point₁) }

theorem EuclidGeom.Quadrilateral_cvx.cclock_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : qdr_cvx.triangle_nd₁.is_cclock ↔ qdr_cvx.triangle_nd₃.is_cclock

theorem EuclidGeom.Quadrilateral_cvx.cclock_eq' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) : qdr_cvx.triangle_nd₂.is_cclock ↔ qdr_cvx.triangle_nd₄.is_cclock