two_zsmul_oangle_of_span_eq_of_span_eq

English

If the spans generated by w and x coincide and the spans generated by y and z coincide, then the doubled oriented angles satisfy 2·o.oangle(w,y) = 2·o.oangle(x,z).

Русский

Если пространства, порождённые w и x, совпадают, и пространства, порождённые y и z, совпадают, то удвоенные ориентированные углы равны: 2·o.oangle(w,y) = 2·o.oangle(x,z).

LaTeX

$$$(2)\cdot o.oangle(w,y) = (2)\cdot o.oangle(x,z)$$$

Lean4

/-- If the spans of two pairs of vectors are equal, twice angles between those vectors are
equal. -/
theorem two_zsmul_oangle_of_span_eq_of_span_eq {w x y z : V} (hwx : (ℝ ∙ w) = ℝ ∙ x) (hyz : (ℝ ∙ y) = ℝ ∙ z) :
    (2 : ℤ) • o.oangle w y = (2 : ℤ) • o.oangle x z := by
  rw [o.two_zsmul_oangle_left_of_span_eq y hwx, o.two_zsmul_oangle_right_of_span_eq x hyz]

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