def AP.Edge.translate (e : Edge) (offset : PointZ) : Edge

Equations

• e.translate offset = { dir := e.dir, offset := e.offset + if e.hor then offset.y else offset.x }

@[simp]

theorem AP.Edge.points_translate {e : Edge} {offset : PointZ} : (e.translate offset).points = ⇑(translate offset).ft '' e.points

@[simp]

theorem AP.Edge.dir_translate {e : Edge} {offset : PointZ} : (e.translate offset).dir = e.dir

@[simp]

theorem AP.Edge.offset_translate {e : Edge} {offset : PointZ} : (e.translate offset).offset = e.offset + if e.hor then offset.y else offset.x

@[simp]

theorem AP.Edge.dist_translate {e : Edge} {offset p : PointZ} : (e.translate offset).dist p = e.dist ((translate offset).ft' p)

@[simp]

theorem AP.Edge.getBorderPoint_translate_of_down {e : Edge} {dy : ℤ} {p : PointZ} {d : ℤ} [H : Fact (e.dir = Dir.down)] : (e.translate { x := 0, y := dy }).getBorderPoint p d = (translate { x := 0, y := dy }).ft (e.getBorderPoint ((translate { x := 0, y := dy }).ft' p) d)

@[simp]

theorem AP.Edge.getBorderPoint₀_translate_of_down {e : Edge} {dy : ℤ} {p : PointZ} [H : Fact (e.dir = Dir.down)] : (e.translate { x := 0, y := dy }).getBorderPoint₀ p = (translate { x := 0, y := dy }).ft (e.getBorderPoint₀ ((translate { x := 0, y := dy }).ft' p))

@[simp]

theorem AP.Edge.getBorderPoints_translate_of_down {e : Edge} {dy : ℤ} {p : PointZ} {d : ℕ} [H : Fact (e.dir = Dir.down)] : (e.translate { x := 0, y := dy }).getBorderPoints p d = List.map (⇑(translate { x := 0, y := dy }).ft) (e.getBorderPoints ((translate { x := 0, y := dy }).ft' p) d)

@[simp]

theorem AP.Edge.ptsArr_translate_of_down {e : Edge} {dy : ℤ} {s : State} [H : Fact (e.dir = Dir.down)] : (e.translate { x := 0, y := dy }).ptsArr s = e.ptsArr ((translate { x := 0, y := dy }).fs' s)

theorem AP.Edge.defense_translate_of_down {e : Edge} {dy : ℤ} [H : Fact (e.dir = Dir.down)] : (e.translate { x := 0, y := dy }).defense = e.defense.sym (translate { x := 0, y := dy })