English
Let p1 ∈ s. Then s.WSameSide x y is equivalent to x ∉ s ∧ y ∉ s ∧ ∃ p2 ∈ s with SameRay(x − p1, y − p2).
Русский
Пусть p1 ∈ s. Тогда s.WSameSide x y эквивалентно x ∉ s ∧ y ∉ s ∧ существует p2 ∈ s, такое что SameRay(x − p1, y − p2).
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 wSameSide_iff_exists_left {s : AffineSubspace R P} {x y p₁ : P} (h : p₁ ∈ s) :
s.WSameSide x y ↔ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂) :=
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 [vsub_vadd_eq_vsub_sub, smul_sub, ← hr, smul_smul, mul_div_cancel₀ _ hr₂.ne.symm, ← smul_sub,
vsub_sub_vsub_cancel_right]
· rintro (h' | ⟨h₁, h₂, h₃⟩)
· exact wSameSide_of_left_mem y h'
· exact ⟨p₁, h, h₁, h₂, h₃⟩
