English
Let V be a 2-dimensional real inner product space with orientation o. For any x, y in V and any real r, the angle o.oangle(x, r·x+y) is 0 or π if and only if o.oangle(x,y) is 0 or π.
Русский
Пусть V — двумерное вещественное пространство с ориентацией o. Для любых x,y ∈ V и любого r ∈ ℝ угол o.oangle(x, r·x+y) равен 0 или π тогда и только тогда, когда o.oangle(x,y) равен 0 или π.
LaTeX
$$$\\forall x,y\\in V,\\ r\\in\\mathbb{R},\\ o.oangle(x, r\\,x+y) \\in \\{0,\\pi\\} \\iff o.oangle(x,y) \\in \\{0,\\pi\\}$$$
Lean4
/-- Auxiliary lemma for the proof of `oangle_sign_smul_add_right`; not intended to be used
outside of that proof. -/
theorem oangle_smul_add_right_eq_zero_or_eq_pi_iff {x y : V} (r : ℝ) :
o.oangle x (r • x + y) = 0 ∨ o.oangle x (r • x + y) = π ↔ o.oangle x y = 0 ∨ o.oangle x y = π :=
by
simp_rw [oangle_eq_zero_or_eq_pi_iff_not_linearIndependent, Fintype.not_linearIndependent_iff, Fin.sum_univ_two,
Fin.exists_fin_two]
refine ⟨fun h => ?_, fun h => ?_⟩
· rcases h with ⟨m, h, hm⟩
change m 0 • x + m 1 • (r • x + y) = 0 at h
refine ⟨![m 0 + m 1 * r, m 1], ?_⟩
change (m 0 + m 1 * r) • x + m 1 • y = 0 ∧ (m 0 + m 1 * r ≠ 0 ∨ m 1 ≠ 0)
rw [smul_add, smul_smul, ← add_assoc, ← add_smul] at h
refine ⟨h, not_and_or.1 fun h0 => ?_⟩
obtain ⟨h0, h1⟩ := h0
rw [h1] at h0 hm
rw [zero_mul, add_zero] at h0
simp [h0] at hm
· rcases h with ⟨m, h, hm⟩
change m 0 • x + m 1 • y = 0 at h
refine ⟨![m 0 - m 1 * r, m 1], ?_⟩
change (m 0 - m 1 * r) • x + m 1 • (r • x + y) = 0 ∧ (m 0 - m 1 * r ≠ 0 ∨ m 1 ≠ 0)
rw [sub_smul, smul_add, smul_smul, ← add_assoc, sub_add_cancel]
refine ⟨h, not_and_or.1 fun h0 => ?_⟩
obtain ⟨h0, h1⟩ := h0
rw [h1] at h0 hm
rw [zero_mul, sub_zero] at h0
simp [h0] at hm
