English
Let p1 ∈ s. Then s.WSameSide x y is equivalent to either x ∉ s and y ∉ s with ∃ p2 ∈ s and SameRay(x − p1, y − p2), or x ∈ s.
Русский
Пусть p1 ∈ s. Тогда s.WSameSide x y эквивалентно либо x ∉ s и y ∉ s с ∃ p2 ∈ s и SameRay(x − p1, y − p2), либо x ∈ s.
LaTeX
$$$s.WSameSide x y\iff x\notin s\land y\notin s\land \exists p_2\in s,\ SameRay(x - p_1, y - p_2)\,.$$$
Lean4
theorem wOppSide_iff_exists_left {s : AffineSubspace R P} {x y p₁ : P} (h : p₁ ∈ s) :
s.WOppSide x y ↔ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y) :=
by
constructor
· rintro ⟨p₁', hp₁', p₂', hp₂', h0 | h0 | ⟨r₁, r₂, hr₁, hr₂, hr⟩⟩
· rw [vsub_eq_zero_iff_eq] at h0
rw [h0]
exact Or.inl hp₁'
· refine Or.inr ⟨p₂', hp₂', ?_⟩
rw [h0]
exact SameRay.zero_right _
· refine
Or.inr
⟨(-r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂', s.smul_vsub_vadd_mem _ h hp₁' hp₂', Or.inr (Or.inr ⟨r₁, r₂, hr₁, hr₂, ?_⟩)⟩
rw [vadd_vsub_assoc, ← vsub_sub_vsub_cancel_right x p₁ p₁']
linear_combination (norm := match_scalars <;> field_simp <;> ring) hr
· rintro (h' | ⟨h₁, h₂, h₃⟩)
· exact wOppSide_of_left_mem y h'
· exact ⟨p₁, h, h₁, h₂, h₃⟩
