Euclidean Plane

This file defines the Euclidean Plane as an affine space, which admits an action of the standard inner product real vector space of dimension two.

Important definitions

• EuclideanPlane : the class of Euclidean Plane

Notation

• VEC A B : the vector B -ᵥ A in Vec

Implementation Notes

For simplicity, we use the standard inner product real vector space of dimension two as the underlying SeminormedAddCommGroup of the NormedAddTorsor in the definition of EuclideanPlane.

Thus we define EuclideanPlane P as NormedAddTorsor (ℝ × ℝ) P and present instances involving EuclideanPlane.

Further Works

The current definition is far from being general enough. Roughly speaking, it suffices to define the Euclidean Plane to be a NormedAddTorsor over any 2 dimensional normed real inner product spaces V with a choice of an orientation on V, rather than over the special ℝ × ℝ. All further generalizations in this file should be done together with Vector.lean.

class EuclidGeom.EuclideanPlane (P : Type u_1) extends MetricSpace , NormedAddTorsor : Type u_1

def EuclidGeom.Vec.mkPtPt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) : EuclidGeom.Vec

Equations

• EuclidGeom.Vec.mkPtPt A B = B -ᵥ A

def EuclidGeom.termVEC : Lean.ParserDescr

Equations

• EuclidGeom.termVEC = Lean.ParserDescr.node `EuclidGeom.termVEC 1024 (Lean.ParserDescr.symbol "VEC")

@[simp]

theorem EuclidGeom.start_vadd_vec_eq_end {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) : EuclidGeom.Vec.mkPtPt A B +ᵥ A = B

@[simp]

theorem EuclidGeom.vadd_eq_self_iff_vec_eq_zero {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {v : EuclidGeom.Vec} : v +ᵥ A = A ↔ v = 0

@[simp]

theorem EuclidGeom.vec_same_eq_zero {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) : EuclidGeom.Vec.mkPtPt A A = 0

@[simp]

theorem EuclidGeom.neg_vec {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) : -EuclidGeom.Vec.mkPtPt A B = EuclidGeom.Vec.mkPtPt B A

@[simp]

theorem EuclidGeom.neg_vec_norm_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) : ‖-EuclidGeom.Vec.mkPtPt A B‖ = ‖EuclidGeom.Vec.mkPtPt A B‖

theorem EuclidGeom.vec_norm_eq_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) : ‖EuclidGeom.Vec.mkPtPt A B‖ = ‖EuclidGeom.Vec.mkPtPt B A‖

theorem EuclidGeom.vec_norm_eq_dist {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) : ‖EuclidGeom.Vec.mkPtPt A B‖ = dist A B

theorem EuclidGeom.eq_iff_vec_eq_zero {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} : B = A ↔ EuclidGeom.Vec.mkPtPt A B = 0

theorem EuclidGeom.ne_iff_vec_ne_zero {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} : B ≠ A ↔ EuclidGeom.Vec.mkPtPt A B ≠ 0

@[simp]

theorem EuclidGeom.vec_add_vec {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) : EuclidGeom.Vec.mkPtPt A B + EuclidGeom.Vec.mkPtPt B C = EuclidGeom.Vec.mkPtPt A C

@[simp]

theorem EuclidGeom.vec_of_pt_vadd_pt_eq_vec {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (v : EuclidGeom.Vec) : EuclidGeom.Vec.mkPtPt A (v +ᵥ A) = v

@[simp]

theorem EuclidGeom.vec_of_vadd_pt_pt_eq_neg_vec {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (v : EuclidGeom.Vec) : EuclidGeom.Vec.mkPtPt (v +ᵥ A) A = -v

@[simp]

theorem EuclidGeom.vec_sub_vec {P : Type u_1} [EuclidGeom.EuclideanPlane P] (O : P) (A : P) (B : P) : EuclidGeom.Vec.mkPtPt O B - EuclidGeom.Vec.mkPtPt O A = EuclidGeom.Vec.mkPtPt A B

@[simp]

theorem EuclidGeom.vec_sub_vec' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (O : P) (A : P) (B : P) : EuclidGeom.Vec.mkPtPt A O - EuclidGeom.Vec.mkPtPt B O = EuclidGeom.Vec.mkPtPt A B

theorem EuclidGeom.pt_eq_pt_of_eq_smul_smul {P : Type u_1} [EuclidGeom.EuclideanPlane P] {O : P} {A : P} {B : P} {v : EuclidGeom.Vec} {tA : ℝ} {tB : ℝ} (h : tA = tB) (ha : EuclidGeom.Vec.mkPtPt O A = tA • v) (hb : EuclidGeom.Vec.mkPtPt O B = tB • v) : A = B

def EuclidGeom.VecND.mkPtPt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (h : B ≠ A) : EuclidGeom.VecND

Equations

• VEC_nd A B h = { val := EuclidGeom.Vec.mkPtPt A B, property := (_ : EuclidGeom.Vec.mkPtPt A B ≠ 0) }

def EuclidGeom.termVEC_nd______ : Lean.ParserDescr

Equations

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

def EuclidGeom.delabVecNDMkPtPt : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for VecND.mkPtPt

Equations

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

@[simp]

theorem EuclidGeom.VecND.coe_mkPtPt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) [_h : Fact (B ≠ A)] : ↑(VEC_nd A B) = EuclidGeom.Vec.mkPtPt A B

@[simp]

theorem EuclidGeom.VecND.neg_vecND {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) [_h : Fact (B ≠ A)] : -VEC_nd A B = VEC_nd B A (_ : A ≠ B)