add_right — Mathlib

English

If x lies on the same ray as y, and x lies on the same ray as z, then x is on the same ray as y+z.

Русский

Если x на луче с y и x на луче с z, то x на луче с y+z.

LaTeX

$$$ \operatorname{SameRay}(R, x, y) \land \operatorname{SameRay}(R, x, z) \Rightarrow \operatorname{SameRay}(R, x, y+z). $$$

Lean4

/-- If `y` and `z` are on the same ray as `x`, then so is `y + z`. -/
theorem add_right (hy : SameRay R x y) (hz : SameRay R x z) : SameRay R x (y + z) :=
  (hy.symm.add_left hz.symm).symm

Похожие утверждения