English
If a Sbtw relation holds and x is not in s while y is in s, then s.SOppSide x z holds for any z with the appropriate conditions; this is a consequence of extending the betweenness by translation.
Русский
Если отношение Sbtw выполняется, и x не принадлежит s, а y принадлежит s, тогда для любого z выполнено s.SOppSide x z при подходящих условиях; это следует из продолжения междуности по смещению.
LaTeX
$$$$ Sbtw\ R\ x\ y\ z \to \neg x\in s \to y\in s \Rightarrow s.SOppSide x z. $$$$
Lean4
theorem _root_.Sbtw.sOppSide_of_notMem_of_mem {s : AffineSubspace R P} {x y z : P} (h : Sbtw R x y z) (hx : x ∉ s)
(hy : y ∈ s) : s.SOppSide x z :=
by
refine ⟨h.wbtw.wOppSide₁₃ hy, hx, fun hz => hx ?_⟩
rcases h with ⟨⟨t, ⟨ht0, ht1⟩, rfl⟩, hyx, hyz⟩
rw [lineMap_apply] at hy
have ht : t ≠ 1 := by
rintro rfl
simp [lineMap_apply] at hyz
have hy' := vsub_mem_direction hy hz
rw [vadd_vsub_assoc, ← neg_vsub_eq_vsub_rev z, ← neg_one_smul R (z -ᵥ x), ← add_smul, ← sub_eq_add_neg,
s.direction.smul_mem_iff (sub_ne_zero_of_ne ht)] at hy'
rwa [vadd_mem_iff_mem_of_mem_direction (Submodule.smul_mem _ _ hy')] at hy
