English
If Wbtw x y z holds, then s.WOppSide (line through x and z with parameter 1/2) 1? Actually, this encodes a relation: there exists t with 0 < t < 1 such that lineMap relation holds; in particular, we can express a left version: WOppSide 13.
Русский
Если выполняется Wbtw x y z, то существует точка на прямой между x и z, которая лежит на противоположной стороне s по отношению к y.
LaTeX
$$$\forall s:\text{AffineSubspace } R P\ ,\forall x,y,z\in P\ (h:Wbtw\ R x y z)\Rightarrow s.WOppSide x z.$$$
Lean4
theorem _root_.Wbtw.wOppSide₁₃ {s : AffineSubspace R P} {x y z : P} (h : Wbtw R x y z) (hy : y ∈ s) : s.WOppSide x z :=
by
rcases h with ⟨t, ⟨ht0, ht1⟩, rfl⟩
refine ⟨_, hy, _, hy, ?_⟩
rcases ht1.lt_or_eq with (ht1' | rfl); swap
· simp
rcases ht0.lt_or_eq with (ht0' | rfl); swap
· simp
refine Or.inr (Or.inr ⟨1 - t, t, sub_pos.2 ht1', ht0', ?_⟩)
rw [lineMap_apply, vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, ← neg_vsub_eq_vsub_rev z, vsub_self]
module
