def EuclidGeom.Seg.translate {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.Seg P) (v : EuclidGeom.Vec) : EuclidGeom.Seg P

Equations

• EuclidGeom.Seg.translate l v = { source := v +ᵥ l.source, target := v +ᵥ l.target }

theorem EuclidGeom.non_triv_of_trans_seg_non_triv {P : Type u_1} [EuclidGeom.EuclideanPlane P] (v : EuclidGeom.Vec) {l : EuclidGeom.Seg P} (nontriv : EuclidGeom.Seg.IsND l) : EuclidGeom.Seg.IsND (EuclidGeom.Seg.translate l v)

def EuclidGeom.SegND.translate {P : Type u_1} [EuclidGeom.EuclideanPlane P] (seg_nd : EuclidGeom.SegND P) (v : EuclidGeom.Vec) : EuclidGeom.SegND P

Equations

• EuclidGeom.SegND.translate seg_nd v = { val := EuclidGeom.Seg.translate (↑seg_nd) v, property := (_ : EuclidGeom.Seg.IsND (EuclidGeom.Seg.translate (↑seg_nd) v)) }

theorem EuclidGeom.reverse_of_trans_eq_trans_of_reverse_of_seg {P : Type u_1} [EuclidGeom.EuclideanPlane P] (v : EuclidGeom.Vec) (l : EuclidGeom.Seg P) : (EuclidGeom.Seg.translate l v).reverse = EuclidGeom.Seg.translate l.reverse v

theorem EuclidGeom.length_eq_length_of_translate_of_seg {P : Type u_1} [EuclidGeom.EuclideanPlane P] (v : EuclidGeom.Vec) (l : EuclidGeom.Seg P) : l.length = (EuclidGeom.Seg.translate l v).length

def EuclidGeom.Ray.translate {P : Type u_1} [EuclidGeom.EuclideanPlane P] (v : EuclidGeom.Vec) (l : EuclidGeom.Ray P) : EuclidGeom.Ray P

Equations

• EuclidGeom.Ray.translate v l = { source := v +ᵥ l.source, toDir := l.toDir }

theorem EuclidGeom.reverse_of_trans_eq_trans_of_reverse_of_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] (v : EuclidGeom.Vec) (l : EuclidGeom.Ray P) : (EuclidGeom.Ray.translate v l).reverse = EuclidGeom.Ray.translate v l.reverse

theorem EuclidGeom.trans_of_seg_of_nontriv_toRay {P : Type u_1} [EuclidGeom.EuclideanPlane P] (v : EuclidGeom.Vec) (seg_nd : EuclidGeom.SegND P) : EuclidGeom.Ray.translate v seg_nd.toRay = (EuclidGeom.SegND.translate seg_nd v).toRay