English
There exists the Wbtw relation along any point p ∈ s within the subspace s for the pair (x, y) under the WOppSide relation.
Русский
Существует отношение Wbtw между x и y через некоторую точку p ∈ s внутри подпространства s, если x и y связаны отношением WOppSide.
LaTeX
$$$$ \text{If } s.WOppSide(x,y) \text{ then } \exists p \in s\; Wbtw(R,x,p,y). $$$$
Lean4
theorem wOppSide_vadd_left_iff {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) :
s.WOppSide (v +ᵥ x) y ↔ s.WOppSide x y := by
constructor
· rintro ⟨p₁, hp₁, p₂, hp₂, h⟩
refine ⟨-v +ᵥ p₁, AffineSubspace.vadd_mem_of_mem_direction (Submodule.neg_mem _ hv) hp₁, p₂, hp₂, ?_⟩
rwa [vsub_vadd_eq_vsub_sub, sub_neg_eq_add, add_comm, ← vadd_vsub_assoc]
· rintro ⟨p₁, hp₁, p₂, hp₂, h⟩
refine ⟨v +ᵥ p₁, AffineSubspace.vadd_mem_of_mem_direction hv hp₁, p₂, hp₂, ?_⟩
rwa [vadd_vsub_vadd_cancel_left]
