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

A quadrilateral satisfies IsPara if it is a QuadrilateralND and satisfies IsPara as a QuadrilateralND.

Equations

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

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

A quadrilateral is called parallelogram if VEC qdr.point₁ qdr.point₂ = VEC qdr.point₄ qdr.point₃.

Equations

• qdr.IsPrg = (EuclidGeom.Vec.mkPtPt qdr.point₁ qdr.point₂ = EuclidGeom.Vec.mkPtPt qdr.point₄ qdr.point₃)

def EuclidGeom.term_IsPrg : Lean.TrailingParserDescr

Equations

• EuclidGeom.term_IsPrg = Lean.ParserDescr.trailingNode `EuclidGeom.term_IsPrg 50 50 (Lean.ParserDescr.symbol "IsPrg")

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

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

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

We define parallelogram as a structure.

• point₁ : P
• point₂ : P
• point₃ : P
• point₄ : P
• is_parallelogram : s.IsPrg

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

Make a parallelogram with 4 points on a plane, and using condition IsPrg.

Equations

• EuclidGeom.Parallelogram.mk_pt_pt_pt_pt A B C D h = { toQuadrilateral := { point₁ := A, point₂ := B, point₃ := C, point₄ := D }, is_parallelogram := h }

def EuclidGeom.termPRG : Lean.ParserDescr

Equations

• EuclidGeom.termPRG = Lean.ParserDescr.node `EuclidGeom.termPRG 1024 (Lean.ParserDescr.symbol "PRG")

def EuclidGeom.Parallelogram.mk_isPrg {P : Type u_1} [EuclidGeom.EuclideanPlane P] {qdr : EuclidGeom.Quadrilateral P} (h : qdr.IsPrg) : EuclidGeom.Parallelogram P

Make a parallelogram with a quadrilateral, and using condition IsPrg.

Equations

• EuclidGeom.Parallelogram.mk_isPrg h = { toQuadrilateral := qdr, is_parallelogram := h }

def EuclidGeom.termPRG' : Lean.ParserDescr

Equations

• EuclidGeom.termPRG' = Lean.ParserDescr.node `EuclidGeom.termPRG' 1024 (Lean.ParserDescr.symbol "PRG'")

theorem EuclidGeom.Parallelogram.eq_vec_of_isPrg {P : Type u_1} [EuclidGeom.EuclideanPlane P] {prg : EuclidGeom.Parallelogram P} : EuclidGeom.Vec.mkPtPt prg.point₁ prg.point₂ = EuclidGeom.Vec.mkPtPt prg.point₄ prg.point₃

Vectors point₁ point₂ and point₄ point₃ in a parallelogram are equal.

theorem EuclidGeom.Parallelogram.eq_vec_of_isPrg' {P : Type u_1} [EuclidGeom.EuclideanPlane P] {prg : EuclidGeom.Parallelogram P} : EuclidGeom.Vec.mkPtPt prg.point₁ prg.point₄ = EuclidGeom.Vec.mkPtPt prg.point₂ prg.point₃

Vectors point₁ point₄ and point₂ point₃ in a parallelogram are equal.

theorem EuclidGeom.Parallelogram.parapara_of_gpos {P : Type u_1} [EuclidGeom.EuclideanPlane P] {prg : EuclidGeom.Parallelogram P} (InGPos : prg.InGPos) : prg.IsParaPara

A parallelogram which satisfies Prallelogram.InGPos satisfies IsParaPara.

theorem EuclidGeom.Parallelogram.cvx_of_gpos {P : Type u_1} [EuclidGeom.EuclideanPlane P] {prg : EuclidGeom.Parallelogram P} (InGPos : prg.InGPos) : prg.IsConvex

A parallelogram which satisfies Prallelogram.InGPos is convex.

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

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

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

We define parallelogram_nd as a structure.

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

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

A quadrilateral is parallelogram_nd if it is both convex and satisfies qualities of a parallelogram. This definition is in agreement with the structure above.

Equations

• qdr.IsPrgND = (qdr.IsConvex ∧ qdr.IsPrg)

def EuclidGeom.term_IsPrgND : Lean.TrailingParserDescr

Equations

• EuclidGeom.term_IsPrgND = Lean.ParserDescr.trailingNode `EuclidGeom.term_IsPrgND 50 50 (Lean.ParserDescr.symbol "IsPrgND")

theorem EuclidGeom.QuadrilateralND.parapara_iff_para_para {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : qdr_nd.IsParaPara ↔ EuclidGeom.Parallel qdr_nd.edgeND₁₂ qdr_nd.edgeND₃₄ ∧ EuclidGeom.Parallel qdr_nd.edgeND₄₁ qdr_nd.edgeND₂₃

theorem EuclidGeom.ParallelogramND.gpos_of_prgnd {P : Type u_1} [EuclidGeom.EuclideanPlane P] (prg_nd : EuclidGeom.ParallelogramND P) : prg_nd.InGPos

A parallelogram_nd satisfies InGPos.

theorem EuclidGeom.ParallelogramND.parapara_of_prgnd {P : Type u_1} [EuclidGeom.EuclideanPlane P] (prg_nd : EuclidGeom.ParallelogramND P) : prg_nd.IsParaPara

A parallelogram_nd satisfies IsParaPara.

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

Equations

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

def EuclidGeom.termPRG_nd : Lean.ParserDescr

Equations

• EuclidGeom.termPRG_nd = Lean.ParserDescr.node `EuclidGeom.termPRG_nd 1024 (Lean.ParserDescr.symbol "PRG_nd")

def EuclidGeom.ParallelogramND.mk_isPrgND {P : Type u_1} [EuclidGeom.EuclideanPlane P] {qdr : EuclidGeom.Quadrilateral P} (h : qdr.IsPrgND) : EuclidGeom.ParallelogramND P

Equations

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

def EuclidGeom.termPRG_nd' : Lean.ParserDescr

Equations

• EuclidGeom.termPRG_nd' = Lean.ParserDescr.node `EuclidGeom.termPRG_nd' 1024 (Lean.ParserDescr.symbol "PRG_nd'")

theorem EuclidGeom.qdr_isPrg_iff_perm_isPrg {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr : EuclidGeom.Quadrilateral P) : qdr.IsPrg ↔ EuclidGeom.Quadrilateral.perm.IsPrg

If a quadrilateral is a parallelogram, then its perm is also a parallelogram.

theorem EuclidGeom.prgND_iff_perm_prgND {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr : EuclidGeom.Quadrilateral P) : qdr.IsPrgND ↔ EuclidGeom.Quadrilateral.perm.IsPrgND

If a quadrilateral is a parallelogram_nd, then its perm is also a parallelogram_nd.

theorem EuclidGeom.para_iff_perm_para {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr : EuclidGeom.Quadrilateral P) : qdr.IsParaPara ↔ EuclidGeom.Quadrilateral.perm.IsParaPara

If a quadrilateral satisfies IsParaPara, then its perm also satisfies IsParaPara.

theorem EuclidGeom.qdrND_IsParaPara_iff_perm_IsParaPara {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : qdr_nd.IsParaPara ↔ qdr_nd.perm.IsParaPara

If a quadrilateral_nd satisfies IsParaPara, then its perm also satisfies IsParaPara.

theorem EuclidGeom.qdr_gpos_iff_perm_gpos {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr : EuclidGeom.Quadrilateral P) : qdr.InGPos ↔ EuclidGeom.Quadrilateral.perm.InGPos

If a quadrilateral satisfies IsParaPara, then its perm also satisfies IsParaPara.

theorem EuclidGeom.qdr_isPrg_iff_flip_isPrg {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr : EuclidGeom.Quadrilateral P) : qdr.IsPrg ↔ EuclidGeom.Quadrilateral.flip.IsPrg

If a quadrilateral is a parallelogram, then its flip is also a parallelogram.

theorem EuclidGeom.qdr_isPrgND_iff_qdr_isPrgND {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr : EuclidGeom.Quadrilateral P) : qdr.IsPrgND ↔ EuclidGeom.Quadrilateral.flip.IsPrgND

If a quadrilateral is a parallelogram_nd, then its flip is also a parallelogram_nd.

theorem EuclidGeom.qdr_IsParaPara_iff_flip_IsParaPara {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr : EuclidGeom.Quadrilateral P) : qdr.IsParaPara ↔ EuclidGeom.Quadrilateral.flip.IsParaPara

If a quadrilateral satisfies IsParaPara, then its flip also satisfies IsParaPara.

theorem EuclidGeom.qdrND_IsParaPara_iff_flip_IsParaPara {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) : qdr_nd.IsParaPara ↔ qdr_nd.flip.IsParaPara

If a quadrilateral_nd satisfies IsParaPara, then its flip also satisfies IsParaPara.

theorem EuclidGeom.qdr_gpos_iff_flip_gpos {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr : EuclidGeom.Quadrilateral P) : qdr.InGPos ↔ EuclidGeom.Quadrilateral.flip.InGPos

If a quadrilateral satisfies IsParaPara, then its flip also satisfies IsParaPara.

theorem EuclidGeom.isPrgND_of_prg_not_collinear₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (prg : EuclidGeom.Parallelogram P) (h : ¬EuclidGeom.Collinear prg.point₂ prg.point₃ prg.point₄) : prg.IsPrgND

If the 2nd, 3rd and 4th points of a parallelogram are not collinear, then it is a parallelogram_nd.

theorem EuclidGeom.isPrgND_of_prg_not_collinear₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (prg : EuclidGeom.Parallelogram P) (h : ¬EuclidGeom.Collinear prg.point₃ prg.point₄ prg.point₁) : prg.IsPrgND

If the 3rd, 4th and 1st points of a parallelogram are not collinear, then it is a parallelogram_nd.

theorem EuclidGeom.isPrgND_of_prg_not_collinear₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (prg : EuclidGeom.Parallelogram P) (h : ¬EuclidGeom.Collinear prg.point₄ prg.point₁ prg.point₂) : prg.IsPrgND

If the 4th, 1st and 2nd points of a parallelogram are not collinear, then it is a parallelogram_nd.

theorem EuclidGeom.isPrgND_of_prg_not_collinear₄ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (prg : EuclidGeom.Parallelogram P) (h : ¬EuclidGeom.Collinear prg.point₁ prg.point₂ prg.point₃) : prg.IsPrgND

If the 1st, 2nd and 3rd points of a parallelogram are not collinear, then it is a parallelogram_nd.

theorem EuclidGeom.prg_isPrgND_iff_not_collinear₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (prg : EuclidGeom.Parallelogram P) : prg.IsPrgND ↔ ¬EuclidGeom.Collinear prg.point₂ prg.point₃ prg.point₄

theorem EuclidGeom.prg_isPrgND_iff_not_collinear₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (prg : EuclidGeom.Parallelogram P) : prg.IsPrgND ↔ ¬EuclidGeom.Collinear prg.point₃ prg.point₄ prg.point₁

theorem EuclidGeom.prg_isPrgND_iff_not_collinear₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (prg : EuclidGeom.Parallelogram P) : prg.IsPrgND ↔ ¬EuclidGeom.Collinear prg.point₄ prg.point₁ prg.point₂

theorem EuclidGeom.prg_isPrgND_iff_not_collinear₄ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (prg : EuclidGeom.Parallelogram P) : prg.IsPrgND ↔ ¬EuclidGeom.Collinear prg.point₁ prg.point₂ prg.point₃

theorem EuclidGeom.qdrND_is_prgND_of_parapara_not_collinear₄ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) (h : qdr_nd.IsParaPara) (notcollinear : ¬EuclidGeom.Collinear qdr_nd.point₁ qdr_nd.point₂ qdr_nd.point₃) : qdr_nd.IsPrgND

If a QuadrilateralND satisfies IsParaPara and its 1st, 2nd and 3rd points are not collinear, then it is a parallelogram_nd.

theorem EuclidGeom.qdrND_is_prgND_of_parapara_not_collinear₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) (h : qdr_nd.IsParaPara) (notcollinear : ¬EuclidGeom.Collinear qdr_nd.point₂ qdr_nd.point₃ qdr_nd.point₄) : qdr_nd.IsPrgND

If a QuadrilateralND satisfies IsParaPara and its 2nd, 3rd and 4th points are not collinear, then it is a parallelogram_nd.

theorem EuclidGeom.qdrND_is_prgND_of_parapara_not_collinear₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) (h : qdr_nd.IsParaPara) (notcollinear : ¬EuclidGeom.Collinear qdr_nd.point₃ qdr_nd.point₄ qdr_nd.point₁) : qdr_nd.IsPrgND

If a QuadrilateralND satisfies IsParaPara and its 3rd, 4th and 1st points are not collinear, then it is a parallelogram_nd.

theorem EuclidGeom.qdrND_is_prgND_of_parapara_not_collinear₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) (h : qdr_nd.IsParaPara) (notcollinear : ¬EuclidGeom.Collinear qdr_nd.point₄ qdr_nd.point₁ qdr_nd.point₂) : qdr_nd.IsPrgND

If a QuadrilateralND satisfies IsParaPara and its 4th, 1st and 2nd points are not collinear, then it is a parallelogram_nd.

theorem EuclidGeom.qdrND_is_prgND_of_eq_angle_value_eq_angle_value_not_collinear₄ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) (h₁ : qdr_nd.angle₁.value = qdr_nd.angle₃.value) (h₂ : qdr_nd.angle₂.value = qdr_nd.angle₄.value) (notcollinear : ¬EuclidGeom.Collinear qdr_nd.point₁ qdr_nd.point₂ qdr_nd.point₃) : qdr_nd.IsPrgND

If the 1st, 3rd and 2nd, 4th angle of a QuadrilateralND are equal in value respectively, and its 1st, 2nd and 3rd points are not collinear, then it is a parallelogram_nd.

theorem EuclidGeom.qdrND_is_prgND_of_eq_angle_value_eq_angle_value_not_collinear₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) (h₁ : qdr_nd.angle₁.value = qdr_nd.angle₃.value) (h₂ : qdr_nd.angle₂.value = qdr_nd.angle₄.value) (notcollinear : ¬EuclidGeom.Collinear qdr_nd.point₂ qdr_nd.point₃ qdr_nd.point₄) : qdr_nd.IsPrgND

If the 1st, 3rd and 2nd, 4th angle of a QuadrilateralND are equal in value respectively, and its 2nd, 3rd and 4th points are not collinear, then it is a parallelogram_nd.

theorem EuclidGeom.qdrND_is_prgND_of_eq_angle_value_eq_angle_value_not_collinear₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) (h₁ : qdr_nd.angle₁.value = qdr_nd.angle₃.value) (h₂ : qdr_nd.angle₂.value = qdr_nd.angle₄.value) (notcollinear : ¬EuclidGeom.Collinear qdr_nd.point₃ qdr_nd.point₄ qdr_nd.point₁) : qdr_nd.IsPrgND

If the 1st, 3rd and 2nd, 4th angle of a QuadrilateralND are equal in value respectively, and its 3rd, 4th and 1st points are not collinear, then it is a parallelogram_nd.

theorem EuclidGeom.qdrND_is_prgND_of_eq_angle_value_eq_angle_value_not_collinear₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) (h₁ : qdr_nd.angle₁.value = qdr_nd.angle₃.value) (h₂ : qdr_nd.angle₂.value = qdr_nd.angle₄.value) (notcollinear : ¬EuclidGeom.Collinear qdr_nd.point₄ qdr_nd.point₁ qdr_nd.point₂) : qdr_nd.IsPrgND

If the 1st, 3rd and 2nd, 4th angle of a QuadrilateralND are equal in value respectively, and its 4th, 1st and 2nd points are not collinear, then it is a parallelogram_nd.

theorem EuclidGeom.qdrND_is_prgND_of_eq_length_eq_length_eq_angle_sign {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) (h₁ : EuclidGeom.SegND.length qdr_nd.edgeND₁₂ = EuclidGeom.SegND.length qdr_nd.edgeND₃₄) (h₂ : EuclidGeom.SegND.length qdr_nd.edgeND₄₁ = EuclidGeom.SegND.length qdr_nd.edgeND₂₃) (h : qdr_nd.angle₁.value.IsPos ∧ qdr_nd.angle₃.value.IsPos ∨ qdr_nd.angle₁.value.IsNeg ∧ qdr_nd.angle₃.value.IsNeg) : qdr_nd.IsPrgND

If edgeND₁₂, edgeND₃₄ and edgeND₁₄, edgeND₂₃ of a QuadrilateralND are equal in value respectively, and angle₁ and angle₃ are of the same sign, then it is a parallelogram_nd.

theorem EuclidGeom.qdrND_is_prgND_of_eq_length_eq_length_eq_angle_sign' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) (h₁ : EuclidGeom.SegND.length qdr_nd.edgeND₁₂ = EuclidGeom.SegND.length qdr_nd.edgeND₃₄) (h₂ : EuclidGeom.SegND.length qdr_nd.edgeND₄₁ = EuclidGeom.SegND.length qdr_nd.edgeND₂₃) (h : qdr_nd.angle₂.value.IsPos ∧ qdr_nd.angle₄.value.IsPos ∨ qdr_nd.angle₂.value.IsNeg ∧ qdr_nd.angle₄.value.IsNeg) : qdr_nd.IsPrgND

If edgeND₁₂, edgeND₃₄ and edgeND₁₄, edgeND₂₃ of a QuadrilateralND are equal in value respectively, and angle₂ and angle₄ are of the same sign, then it is a parallelogram_nd.

theorem EuclidGeom.qdrND_is_prg_of_parapara_eq_length_eq_length {P : Type u_2} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) (h : qdr_nd.IsParaPara) (h₂ : EuclidGeom.SegND.length qdr_nd.edgeND₁₂ = EuclidGeom.SegND.length qdr_nd.edgeND₃₄) (H₂ : EuclidGeom.SegND.length qdr_nd.edgeND₄₁ = EuclidGeom.SegND.length qdr_nd.edgeND₂₃) : qdr_nd.IsPrg

If edgeND₁₂ and edgeND₃₄ of a QuadrilateralND are equal in value and parallel, and so do edgeND₁₄ and edgeND₂₃, then it is a parallelogram.

theorem EuclidGeom.qdrND_is_prg_of_diag_inx_eq_midpt_eq_midpt {P : Type u_2} [EuclidGeom.EuclideanPlane P] (qdr_nd : EuclidGeom.QuadrilateralND P) (h' : EuclidGeom.Quadrilateral.diag₁₃.midpoint = EuclidGeom.Quadrilateral.diag₂₄.midpoint) : qdr_nd.IsPrg

If the midpoint of the two diags of a QuadrilateralND are exactly the same, then it is a parallelogram.

theorem EuclidGeom.qdrND_is_prg_of_diag_inx_eq_midpt_eq_midpt_variant {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {D : P} (nd : { point₁ := A, point₂ := B, point₃ := C, point₄ := D }.IsND) (h' : { source := A, target := C }.midpoint = { source := B, target := D }.midpoint) : (EuclidGeom.QuadrilateralND.mk_nd nd).IsPrg

If the midpoint of AC and BD are exactly the same, then QuadrilateralND A B C D is a parallelogram.

theorem EuclidGeom.qdrcvx_is_prgND_of_parapara {P : Type u_2} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) (h₁ : qdr_cvx.IsParaPara) : qdr_cvx.IsPrgND

If edgeND₁₂ and edgeND₃₄ of a quadrilateral_cvx are parallel, and so do edgeND₁₄ and edgeND₂₃, then it is a parallelogram_nd.

theorem EuclidGeom.qdrcvx_is_prgND_of_eq_length_eq_length {P : Type u_2} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) (h₁ : EuclidGeom.SegND.length qdr_cvx.edgeND₁₂ = EuclidGeom.SegND.length qdr_cvx.edgeND₃₄) (h₂ : EuclidGeom.SegND.length qdr_cvx.edgeND₄₁ = EuclidGeom.SegND.length qdr_cvx.edgeND₂₃) : qdr_cvx.IsPrgND

If edgeND₁₂ and edgeND₃₄ of a quadrilateral_cvx are equal in length, and so do edgeND₁₄ and edgeND₂₃, then it is a parallelogram_nd.

theorem EuclidGeom.qdrcvx_is_prgND_of_para_eq_length {P : Type u_2} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) (h₁ : EuclidGeom.Parallel qdr_cvx.edgeND₁₂ qdr_cvx.edgeND₃₄) (h₂ : EuclidGeom.SegND.length qdr_cvx.edgeND₁₂ = EuclidGeom.SegND.length qdr_cvx.edgeND₃₄) : qdr_cvx.IsPrgND

If edgeND₁₂ and edgeND₃₄ of a quadrilateral_cvx are not only equal in length but also parallel, then it is a parallelogram_nd.

theorem EuclidGeom.qdrcvx_is_prgND_of_para_eq_length' {P : Type u_2} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) (h₁ : EuclidGeom.Parallel qdr_cvx.edgeND₄₁ qdr_cvx.edgeND₂₃) (h₂ : EuclidGeom.SegND.length qdr_cvx.edgeND₄₁ = EuclidGeom.SegND.length qdr_cvx.edgeND₂₃) : qdr_cvx.IsPrgND

If edgeND₄₁ and edgeND₂₃ of a quadrilateral_cvx are not only equal in length but also parallel, then it is a parallelogram_nd.

theorem EuclidGeom.qdrcvx_is_prgND_of_eq_angle_value_eq_angle_value {P : Type u_2} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) (h₁ : qdr_cvx.angle₁.value = qdr_cvx.angle₃.value) (h₂ : qdr_cvx.angle₂.value = qdr_cvx.angle₄.value) : qdr_cvx.IsPrgND

If angle₁ and angle₃ of a quadrilateral_cvx are equal in value, and so do angle₂ and angle₄, then it is a parallelogram_nd.

theorem EuclidGeom.qdrcvx_is_prgND_of_diag_eq_midpt {P : Type u_2} [EuclidGeom.EuclideanPlane P] (qdr_cvx : EuclidGeom.Quadrilateral_cvx P) (h' : EuclidGeom.SegND.midpoint (EuclidGeom.Quadrilateral_cvx.diag_nd₁₃ qdr_cvx) = EuclidGeom.SegND.midpoint (EuclidGeom.Quadrilateral_cvx.diag_nd₂₄ qdr_cvx)) : qdr_cvx.IsPrgND

If the midpoint of the two diags of a quadrilateral_cvx are exactly the same, then it is a parallelogram_nd.

theorem EuclidGeom.qdrcvx_is_prgND_of_diag_eq_midpt_variant {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {D : P} (cvx : { point₁ := A, point₂ := B, point₃ := C, point₄ := D }.IsConvex) (h' : { source := A, target := C }.midpoint = { source := B, target := D }.midpoint) : (EuclidGeom.Quadrilateral_cvx.mk_cvx cvx).toQuadrilateralND.IsPrgND

Given four points ABCD and Quadrilateral ABCD IsConvex, and the midpoint of the diagonal AC and BD is the same, Quadrilateral ABCD is a Parallelogram_nd.

theorem EuclidGeom.eq_length_of_isPrg {P : Type u_3} [EuclidGeom.EuclideanPlane P] (prg : EuclidGeom.Parallelogram P) : EuclidGeom.Quadrilateral.edge₁₂.length = EuclidGeom.Quadrilateral.edge₃₄.length

The lengths of segments point₁ point₂ and point₃ point₄ in a parallelogram are equal.

theorem EuclidGeom.eq_length_of_isPrg_variant {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {D : P} (h : { point₁ := A, point₂ := B, point₃ := C, point₄ := D }.IsPrg) : { source := A, target := B }.length = { source := C, target := D }.length

theorem EuclidGeom.eq_length_of_isPrg' {P : Type u_3} [EuclidGeom.EuclideanPlane P] (prg : EuclidGeom.Parallelogram P) : EuclidGeom.Quadrilateral.edge₁₄.length = EuclidGeom.Quadrilateral.edge₂₃.length

The lengths of segments point₁ point₄ and point₂ point₃ in a parallelogram are equal.

theorem EuclidGeom.eq_length_of_isPrg'_variant {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {D : P} (h : { point₁ := A, point₂ := B, point₃ := C, point₄ := D }.IsPrg) : { source := A, target := D }.length = { source := B, target := C }.length

theorem EuclidGeom.eq_midpt_of_diag_of_isPrg {P : Type u_3} [EuclidGeom.EuclideanPlane P] (prg : EuclidGeom.Parallelogram P) : EuclidGeom.Quadrilateral.diag₁₃.midpoint = EuclidGeom.Quadrilateral.diag₂₄.midpoint

The midpoints of segments point₁ point₃ and point₂ point₄ in a parallelogram are exactly the same.

theorem EuclidGeom.parallelogram_law {P : Type u_3} [EuclidGeom.EuclideanPlane P] (prg : EuclidGeom.Parallelogram P) : 2 * EuclidGeom.Quadrilateral.edge₁₂.length ^ 2 + 2 * EuclidGeom.Quadrilateral.edge₂₃.length ^ 2 = EuclidGeom.Quadrilateral.diag₁₃.length ^ 2 + EuclidGeom.Quadrilateral.diag₂₄.length ^ 2

In a parallelogram the sum of the square of the sides is equal to that of the two diags.

theorem EuclidGeom.parallelogram_law_variant {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {D : P} (h : { point₁ := A, point₂ := B, point₃ := C, point₄ := D }.IsPrg) : 2 * { source := A, target := B }.length ^ 2 + 2 * { source := B, target := C }.length ^ 2 = { source := A, target := C }.length ^ 2 + { source := B, target := D }.length ^ 2

In a parallelogram A B C D the sum of the square of the sides is equal to that of the two diags, namely 2 * AB² + 2 * BC² = AC² + BD².

theorem EuclidGeom.para_of_isPrgND {P : Type u_3} [EuclidGeom.EuclideanPlane P] (prg_nd : EuclidGeom.ParallelogramND P) : EuclidGeom.Parallel prg_nd.edgeND₁₂ prg_nd.edgeND₃₄

In a parallelogram_nd, edgeND₁₂ and edge₃₄ are parallel.

theorem EuclidGeom.para_of_isPrgND' {P : Type u_3} [EuclidGeom.EuclideanPlane P] (prg_nd : EuclidGeom.ParallelogramND P) : EuclidGeom.Parallel prg_nd.edgeND₄₁ prg_nd.edgeND₂₃

In a parallelogram_nd, edgeND₁₄ and edge₂₃ are parallel.

theorem EuclidGeom.todir_eq_of_isPrgND {P : Type u_3} [EuclidGeom.EuclideanPlane P] (prg_nd : EuclidGeom.ParallelogramND P) : prg_nd.edgeND₁₂.toDir = -prg_nd.edgeND₃₄.toDir

The toDirs of edgeND₁₂ and edgeND₃₄ of a parallelogram_nd remain reverse.

theorem EuclidGeom.todir_eq_of_isPrgND' {P : Type u_3} [EuclidGeom.EuclideanPlane P] (prg_nd : EuclidGeom.ParallelogramND P) : prg_nd.edgeND₄₁.toDir = -prg_nd.edgeND₂₃.toDir

The toDirs of edgeND₁₄ and edgeND₂₃ of a parallelogram_nd remain the same.

theorem EuclidGeom.eq_angle_value_of_isPrgND {P : Type u_3} [EuclidGeom.EuclideanPlane P] (prg_nd : EuclidGeom.ParallelogramND P) : prg_nd.angle₂.value = prg_nd.angle₄.value

In a parallelogram_nd, angle₂ and angle₄ are equal.

theorem EuclidGeom.eq_angle_value_of_isPrgND' {P : Type u_3} [EuclidGeom.EuclideanPlane P] (prg_nd : EuclidGeom.ParallelogramND P) : prg_nd.angle₁.value = prg_nd.angle₃.value

In a parallelogram_nd, angle₁ and angle₃ are equal.

theorem EuclidGeom.eq_midpt_of_diag_inx_of_isPrgND {P : Type u_3} [EuclidGeom.EuclideanPlane P] (prg_nd : EuclidGeom.ParallelogramND P) : prg_nd.diag_inx = EuclidGeom.SegND.midpoint (EuclidGeom.Quadrilateral_cvx.diag_nd₁₃ prg_nd.toQuadrilateral_cvx)

In a parallelogram_nd the intersection of the two diags is the same as the midpoint of diag₁₃.

theorem EuclidGeom.eq_midpt_of_diag_inx_of_isPrgND' {P : Type u_3} [EuclidGeom.EuclideanPlane P] (prg_nd : EuclidGeom.ParallelogramND P) : prg_nd.diag_inx = EuclidGeom.SegND.midpoint (EuclidGeom.Quadrilateral_cvx.diag_nd₂₄ prg_nd.toQuadrilateral_cvx)

In a parallelogram_nd the intersection of the two diags is the same as the midpoint of diag₂₄.