English
Let s be an affine subspace of P. If p1 and p2 lie in s and p3, p4 lie on the same side of s, then the signs of the oriented angles ∡p1 p4 p2 and ∡p1 p3 p2 are equal.
Русский
Пусть s — аффиново подпространство множества P. Если p1 и p2 принадлежат s, а p3, p4 лежат с одной стороны от s, то знаки ориентированных углов ∡p1 p4 p2 и ∡p1 p3 p2 равны.
LaTeX
$$$\operatorname{sign}(\angle p_1 p_4 p_2) = \operatorname{sign}(\angle p_1 p_3 p_2)$$$
Lean4
/-- Given two points in an affine subspace, the angles between those two points at two other
points on the same side of that subspace have the same sign. -/
theorem _root_.AffineSubspace.SSameSide.oangle_sign_eq {s : AffineSubspace ℝ P} {p₁ p₂ p₃ p₄ : P} (hp₁ : p₁ ∈ s)
(hp₂ : p₂ ∈ s) (hp₃p₄ : s.SSameSide p₃ p₄) : (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign :=
by
by_cases h : p₁ = p₂; · simp [h]
let sp : Set (P × P × P) := (fun p : P => (p₁, p, p₂)) '' {p | s.SSameSide p₃ p}
have hc : IsConnected sp := (isConnected_setOf_sSameSide hp₃p₄.2.1 hp₃p₄.nonempty).image _ (by fun_prop)
have hf : ContinuousOn (fun p : P × P × P => ∡ p.1 p.2.1 p.2.2) sp :=
by
refine continuousOn_of_forall_continuousAt fun p hp => continuousAt_oangle ?_ ?_
all_goals
simp_rw [sp, Set.mem_image, Set.mem_setOf] at hp
obtain ⟨p', hp', rfl⟩ := hp
dsimp only
rintro rfl
· exact hp'.2.2 hp₁
· exact hp'.2.2 hp₂
have hsp : ∀ p : P × P × P, p ∈ sp → ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ π :=
by
intro p hp
simp_rw [sp, Set.mem_image, Set.mem_setOf] at hp
obtain ⟨p', hp', rfl⟩ := hp
dsimp only
rw [oangle_ne_zero_and_ne_pi_iff_affineIndependent]
exact affineIndependent_of_ne_of_mem_of_notMem_of_mem h hp₁ hp'.2.2 hp₂
have hp₃ : (p₁, p₃, p₂) ∈ sp := Set.mem_image_of_mem _ (sSameSide_self_iff.2 ⟨hp₃p₄.nonempty, hp₃p₄.2.1⟩)
have hp₄ : (p₁, p₄, p₂) ∈ sp := Set.mem_image_of_mem _ hp₃p₄
convert Real.Angle.sign_eq_of_continuousOn hc hf hsp hp₃ hp₄
