English
Let p2 ∈ s. Then s.WSameSide x y ↔ y ∈ s ∨ ∃ p1 ∈ s, SameRay(x − p1, y − p2).
Русский
Пусть p2 ∈ s. Тогда s.WSameSide x y эквивалентно y ∈ s или существует p1 ∈ s, такое что SameRay(x − p1, y − p2).
LaTeX
$$$s.WSameSide x y\iff y\in s\lor \exists p_1\in s,\ SameRay(x - p_1, y - p_2).$$$
Lean4
theorem wOppSide_iff_exists_right {s : AffineSubspace R P} {x y p₂ : P} (h : p₂ ∈ s) :
s.WOppSide x y ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y) :=
by
rw [wOppSide_comm, wOppSide_iff_exists_left h]
constructor
· rintro (hy | ⟨p, hp, hr⟩)
· exact Or.inl hy
refine Or.inr ⟨p, hp, ?_⟩
rwa [SameRay.sameRay_comm, ← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev]
· rintro (hy | ⟨p, hp, hr⟩)
· exact Or.inl hy
refine Or.inr ⟨p, hp, ?_⟩
rwa [SameRay.sameRay_comm, ← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev]
